Многие документы используют SAT, но мало кто упоминал, как преобразовать дополнение в CNF.
Поскольку CNF допускает только операции И ИЛИ НЕ, описать операцию добавления сложно. Например,
x1 + x2 + x3 + ... +x1599 < 30, xi is binary.
- Преобразуйте эти уравнения в булеву схему.
- Примените преобразование Цейтина к схеме и преобразуйте его в формат DIMACS.
Но есть ли способ прочитать результаты? Я действительно думаю, что можно прочитать результаты, если все переменные определены самим собой, поэтому необходимо выяснить, как преобразовать линейное ограничение в задачу SAT.
Если есть 3 или 4 переменные, т.е. x1+ x2 + x3 <3, мы можем использовать таблицу истинности, чтобы решить это преобразование. Кроме того, прямой путь состоит в том, что 29 (любое число меньше 30) переменных из 1600 переменных равны 1, остальные - 0. Но существует слишком много возможностей, которые затрудняют решение этой проблемы. </p>
Я использовал STP, но он может дать только 1 ответ. По мере увеличения числа переменных и предложений запуск STP занимает много времени.
Поэтому я попытался использовать SAT для решения cnf, заданного STP, он может выдавать ответы за считанные минуты. Но результаты не могут быть прочитаны.
В конце я нашел несколько статей: 1. Кодирование линейных ограничений с импликационными цепями в CNF, 2. Методы на основе SAT для целочисленных линейных ограничений. Это может быть полезно.