Pycos SAT with pycosat

Question

pycosat 라이브러리를 사용하여 SAT를 테스트하는 함수를 작성해야하는 클래스 할당이 있습니다. 라이브러리에서 "UNSAT"를 반환하는 매개 변수 집합을 파악하는 데 어려움을 겪고 있습니다. 누군가가 "해결할 수없는"매개 변수 세트를 찾도록 도와 줄 수 있습니까? 라이브러리에 대한 단위 테스트를 살펴보면 찾을 수있는 유일한 인스턴스는 [[1], [-1]]

** 할당은 훨씬 더 복잡하며 SAT 해결 자만 이해하려고합니다. 그것은 내 과제를 테스트하는 데 사용됩니다.

Answer 1

내 자신의 질문에 대답하려면 : 모순을 만들어야합니다. 3 개의 변수 (A, B, C)를 만듭니다. 해결할 수없는 계산을 만들려면 해결할 수없는 부울 연산을 만들어야합니다.

(A 또는 B) 및 (아니하거나하지 B) 및 (B 또는 C) 및 (B 없거나 C)

진리표 보여 것이라고 A, B 또는 C의 값들의 조합하지 위의 계산이 참이 될 수 있습니다. 이것을 다음과 같이 표현하면 다음과 같습니다.

[[1, 2], [2, 3], [-2,3]]