실제 SAT 인스턴스

Question

SAT 해결사를 설계하고 구현하고 있습니다. 모든 조항은 내가 실제로 원래의 실제 문제에 덜 효율적 표현이 될 것이라고 생각이다 형태 문헌에

a AND b = c 
a OR b = c 
a XOR b = c 
a = NOT b 

그들이 사용하는 CNF의 형태의 경우는 특히 좋은 것입니다. 기존 SAT 해결자가 CNF를보다 잘 처리 할 수 ​​있기 때문에 이러한 작업을 수행 할 수 있습니다. 그러나 이것은 내 SAT 해결사에게 적용되지 않을 것이며, 이는 내게 불공정 한 불이익을 초래할 것입니다. 위의 형식으로 실제 인스턴스를 알고있는 사람이 있습니까?

Answer 1

유효한 점수를 올립니다. Peter Stuckey는 SAT Conference 2013에 "CNF 문제가 없습니다"라는 프레젠테이션을했습니다. 슬라이드 here을 찾으실 수 있습니다.

실제 응용 프로그램의 경우 Stuckey의 MiniZinc과 같은 상위 수준의 문제 설명 언어를 사용하는 것이 좋습니다. CNF의 문제를 인코딩하는 일은 너무 지루하고 오류가 발생하기 쉽습니다.

은 귀하의 질문에 대답하려면 :
예, 대부분의 실제 문제가 부울 또는 수학적 표현으로서가 아닌 CNF로 설명되어 있습니다. 인코딩 단계는 일부 솔버가 해결하도록하기 위해 필요합니다.

문제가있는 인코딩을 덜 문제화하기 위해 과학 시장에 많은 "학교"솔버가 있습니다. 예를 들어 Gringo/Clasp과 CSP (Constraint Programming Solvers) 같은 답변 세트 프로그래밍 (ASP)은 MiniZinc입니다.

다른 옵션은 CNF-SAT 대신 "Circuit-SAT"를 사용하는 것입니다. "회로"는 논리 게이트 및 이들 사이의 연결에 의해 설명됩니다. 이것은 부울 표현식의 일종의 중첩 시스템입니다. 회로를 CNF로 번역하는 가장 좋은 도구는 bc2cnf입니다.

CNF에 대해 언급하는 몇 가지 좋은 점이있다 :

1. CNF (DIMACS 형식)
2. CNF 오히려 컴팩트 한 많은 도구에 의해 처리 될 수
CNF 아주 쉽게 구문 분석 할 수

Answer 2

SAT 솔버의 이론 및 적용은 CNF 표현과 매우 밀접하게 결합되어 있습니다. 솔버가 CNF 대신 부울 수식을 사용하는 경우 솔버를 "SAT 솔버"가 아니라 "수량 한정 프리 1 차 로직을 제외한 이론을 지원하지 않는 SMT 솔버"라고 생각할 수 있습니다.

많은 SMT 솔버는 입력 언어로 SMT-LIBv2를 지원합니다. SMT-LIB에서 솔버의 피쳐 세트는 set-logic 문을 사용하여 "로직"을 설정하여 구성됩니다. QF_UF 논리는 기본 양수 기호가없는 부울 수식 만 지원하므로 원하는 것과 동등해야합니다. 예 : SMT-LIB 구문에 예 절 일 : SMT 해결사로 전달 될 때

(set-logic QF_UF) 
(declare-fun a() Bool) 
(declare-fun b() Bool) 
(declare-fun c() Bool) 
(assert (= (and a b) c)) 
(assert (= (or a b) c)) 
(assert (= (xor a b) c)) 
(assert (= a (not b))) 
(check-sat) 
(exit) 

unsat를 인쇄 할 수있다.

SMT-LIB QF_UF 벤치 마크는이 fomat에 문제의 큰 컬렉션을 포함 (6647 "조작"3 "산업") :

• http://www.cs.nyu.edu/~barrett/smtlib/QF_UF_Hierarchy.zip

SMT 대회가 나누어집니다 논리 부. 따라서 QF_UF 만 지원하는 경쟁에서 솔버를 입력 할 수 있습니다. (사실, OpenSMT2 솔버는 QF_UF을 지원하고 SMT-COMP 2014에 참여했다.)