내가 생각한 내용에 대한 답변을 quite interesting question에 적었습니다.하지만 불행히도 질문을 게시자가 삭제하기 전에 삭제되었습니다. 다른 사람에게 유용 할 수 있으므로 질문과 대답의 요약을 다시 게시합니다.SAT 해결사를 사용하여 모든 솔루션을 찾을 수 있습니까?
결합 표준 형식의 부울 수식이 주어지면 솔루션 (수식을 만족하는 변수 할당) 또는 문제가 만족스럽지 않다는 정보를 반환하는 SAT 해결사가 있다고 가정합니다.
이 해답을 사용하여 을 찾을 수 있습니까? 솔루션을 모두 찾을 수 있습니까?
SAT 문제의 모든 해결책을 찾기 위해 설명한 SAT 해결사를 사용하는 방법이 있지만 가장 효율적인 방법은 아닙니다.
솔버를 사용하여 원래 문제에 대한 해결책을 찾고, 방금 찾은 해결책을 제외하고 아무 것도하지 않는 절을 추가하고, 해결자를 사용하여 새로운 문제에 대한 해결책을 찾는 등의 작업을 수행하십시오. 만족스럽지 않은 문제가 발생할 때까지 계속하십시오.
예를 들어 (X or Y) and (X or Z)을 만족 시키려고한다고 가정합니다. 사실 X, Y 및 Z 임의의로
네 : 다섯 가지 해결책이 있습니다.
하나는 X이고, 하나는 Y이고, 다른 하나는 Z입니다.
그러면 해결사를 실행하고 해결책이 (X, Y, Z) = (T, F, F)이라고 가정 해 봅시다. 당신은이 제약이 절 그래서
(not X) or Y or Z
지금 당신이에 당신의 해결사를 실행할 수로 다시 쓸 수있는 제약
not (X and (not Y) and (not Z))
로 ---이 솔루션 --- 만이 솔루션을 배제 할 수 새로운 문제
등등.
내가 말했듯이, 이것은 당신이 원하는대로 할 수있는 방법이지만, 아마도 가장 효율적인 방법은 아닙니다. SAT 솔버가 솔루션을 찾고있을 때 문제에 대해 많은 것을 알게되지만 모든 정보를 반환하지는 않습니다. 단지 찾은 솔루션 만 제공합니다. 솔버를 다시 실행할 때, 버려진 모든 정보를 다시 학습해야합니다.
물론 가능합니다.MiniSat [1] 솔루션을 발견하면
s SATISFIABLE
v 1 2 -3 0
(솔루션 = True 1 = True 2, 3 = False) 다음은이 솔루션을 금지 원래 CNF [2] 절에 추가해야한다
-1 -2 3 0
(즉, 1 또는 2는 False이거나 3은 True이어야합니다.) 그럼 다시 풀어. 해석기가 UNSAT를 반환 할 때까지 즉, 문제에 대한 해결책이 더 이상 없을 때까지이 작업을 수행합니다. 반복 할 때마다 하나의 절을 삽입하고 각 절의 형식이 모두 거꾸로되어 끝 부분에 0이 있습니다.
이렇게하면 MiniSat의 C++ 인터페이스를 사용하는 것이 훨씬 빠릅니다. 그러면 중간 데이터를 저장할 수 있고 반복 작업이 빨라집니다.
[2] http://fairmut3x.wordpress.com/2011/07/29/cnf-conjunctive-normal-form-dimacs-format-explained/
하십시오을 downvoted 사람이 이유를 설명 할 수 있습니까? 이 블로그 항목 (http://blog.stackoverflow.com/2011/07/its-ok-to-ask-and-answer-your-own-questions/)을 읽은 후, 나는 여기서 한 것은 "단지 OK "하지만"명시 적으로 권장합니다. " – Vectornaut
괜찮습니다. 좋은 대답, btw. –