5
SAT가 NP 완전하다는 증거는 건설적인 증거이므로 프로그램으로 구현할 수 있어야합니다. 아무도이 짓을 한거야?검증 알고리즘을 SAT 문제로 변환하는 컴파일러
나는 (true 또는 false를 반환하는) 프로그램으로 입력하고 SAT 수식을 출력하는 프로그램 (컴파일러)을 찾고있다.
예를 들어, 컴파일러는 다음 프로그램을 사용할 수 있습니다 (pythonic 구문으로 표시하지만 모든 언어는 저와 동일합니다). 입력으로 SAT 수식을 출력합니다. SAT 공식을 SAT 해석기에 공급하면 "인증서"매개 변수에 대한 해답을 얻을 수 있습니다. 이 경우, 해는 {-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 공식에는 다른 보조 변수가 있으므로 컴파일러는 어떤 변수가 인증서에 해당하는지 표시해야합니다.
이러한 컴파일러가 이미 있습니까? 그들 중 누구도 오픈 소스입니까?