Доказательство того, что SAT является NP-полным, является конструктивным доказательством, поэтому его можно реализовать в виде программы. Кто-нибудь сделал это?
Я ищу программу (компилятор), которая принимает на вход программу (которая возвращает true или false) и выводит формулу SAT.
Так, например, компилятор может взять на вход следующую программу (покажите в синтаксисе pythonic, но меня устраивает любой язык) и вывести формулу SAT. Подача формулы SAT в решатель SAT даст решение для параметра «сертификат». В этом случае решением будет [False, True, True, True, False], что указывает на то, что {-3, -2, 5} является решением.
def verify(certificate):
problem = [-7, -3, -2, 5, 8]
sum = 0
for (x, b) in zip(problem, certificate):
if b:
sum += x
return sum == 0
Очевидно, что выходная формула SAT будет иметь другие вспомогательные переменные, поэтому компилятору придется указать, какие переменные соответствуют сертификату.
Такие компиляторы уже существуют? Есть ли среди них открытый исходный код?
