Z3 SAT 솔버를위한 XOR 절

Question

나는 각각 22 개의 입력을 갖는 수백 개의 XOR 절을 포함하여 만족 가능성 문제를 해결하기 위해 Z3을 사용하고있다. DIMACS 형식의 XOR 절을 코딩하려면 Tseitin 인코딩을 사용하고 있습니다. 내 변환은 XOR을 각각 최대 5 자 리터럴의 작은 CNF 절로 나눕니다. Z3은 지금까지 SAT 솔루션을 고안 할 수 없습니다.

인코딩을 개선하려면 어떻게해야합니까?

가우스 제거를 살펴 보았지만, XOR 표현식에 동일한 입력 변수가 없으므로 아마도 도움이되지 않습니다.

Answer 1

Z3에는 2 개의 SAT 해결 엔진이 있으므로 전략 프레임 워크를 사용하여보다 효율적인 엔진을 사용할 수 있습니다. 예를 들어, 자습서를 참조 Z3 - strategies (가) 비트 벡터 식 전략의 사용을 설명하는 부분이 있습니다

: 말했다

(declare-const x (_ BitVec 16)) 
(declare-const y (_ BitVec 16)) 
(assert (= (bvor x y) (_ bv13 16))) 
(assert (bvslt x y)) 
(check-sat-using (then simplify solve-eqs bit-blast sat)) 
(get-model) 

,을 CDCl3 기반 SAT 하드 인스턴스를 생성 비교적 쉽게 솔버는 XOR을 사용합니다. 예 :

Randal E. Bryant: A View from the Engine Room: Computational Support for Symbolic Model Checking. 25 Years of Model Checking 2008: 145-149 

Z3의 더 솔버 (위의 예에서 호출) 토 효율적인 검출 및 배타적 논리합을 연산하여 (동등성)로 전파 일부 데이터 구조를 갖는다.