Z3 Z3을 SAT 솔버로 사용하는 극성

Question

Z3을 사용하여 12000+ 부울 변수로 SAT 문제를 풀려고합니다. 대부분의 변수는 솔루션에서 false로 평가 될 것으로 예상됩니다. Z3을 "극성 거짓"을 먼저 시도하는 SAT 해결사로 안내하거나 알려주는 방법이 있습니까? 나는 cryptominisat 2로 시도해 봤는데 좋은 결과를 얻었습니다.

Answer 1

Z3은 해독기와 전 처리기 모음입니다. 우리는 일부 해결사에 대한 힌트를 제공 할 수 있습니다. (check-sat) 명령을 사용하면 Z3이 자동으로 솔버를 선택합니다. 솔버를 직접 선택하려면 (check-sat-using <strategy>)해야합니다. 예를 들어, 다음 명령은 Z3에 부울 SAT 해결자를 사용하도록 지시합니다.

(check-sat-using sat) 

우리는 항상 사용하여 첫 번째 "거짓 극성을"시도를 강제 할 수

(check-sat-using (with sat :phase always-false)) 

우리는 또한 전처리 단계를 제어 할 수 있습니다. 우리가 sat를 호출하기 전에 CNF 수식을 넣고 싶은 경우에, 우리는 사용한다 :

(check-sat-using (then tseitin-cnf (with sat :phase always-false))) 

편집을 : 당신이 DIMACS 입력 형식과 Z3의 v4.3.1를 사용하는 경우, 다음 매개 변수를 설정할 수 없습니다 명령 줄을 사용하여 사용 가능한 모든 해결사. 다음 릴리스에서는이 제한 사항을 해결합니다. 그 사이에

git clone https://git01.codeplex.com/z3 -b unstable 

을 사용하여 작업중인 지점을 다운로드하고 Z3을 컴파일 할 수 있습니다. 그런 다음, 극성 거짓을 강제로, 우리는이 모듈에 사용할 수있는 모든 옵션을 표시합니다 명령 줄 옵션

sat.phase=always_false 

명령 z3 -pm:sat을 사용합니다. 스택 오버플로

(declare-const p Bool) 
(declare-const q Bool) 
(declare-const r Bool) 
(declare-const s Bool) 

(assert (or (not p) (not q) (not r))) 
(assert (or r s)) 
(assert (or r (not s))) 
(assert (or r (and p q))) 

(echo "With always false") 
(check-sat-using (then tseitin-cnf (with sat :phase always-false))) 
(get-model) 
(echo "With always true") 
(check-sat-using (then tseitin-cnf (with sat :phase always-true))) 
(get-model)