Dowód, że SAT jest NP-complete jest dowodem konstrukcyjnym, więc powinno być możliwe jego wdrożenie jako programu. Czy ktoś to zrobił?Kompilatory tłumaczące algorytmy weryfikacji na problemy SAT
Szukam programu (kompilatora), który pobiera jako dane wejściowe program (który zwraca wartość true lub false) i wysyła formułę SAT.
Na przykład, kompilator może przyjąć następujący program (pokaż w składni pythonic, ale każdy język jest w porządku ze mną), jako dane wejściowe i wypisać formułę SAT. Podanie formuły SAT do solver SAT dałoby rozwiązanie do parametru "certyfikat". W takim przypadku rozwiązaniem byłoby [False, True, True, True, False], wskazując, że {-3, -2, 5} jest rozwiązaniem.
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
Oczywiście wyjście SAT wzór miałyby inne zmienne pomocnicze, tak kompilator musi wskazać zmiennych odpowiadają certyfikatu.
Czy takie kompilatory już istnieją? Czy któryś z nich jest open source?