I am using Z3 to solve satisfiability problems including several hundred XOR clauses with 22 inputs each. To code the XOR clauses in DIMACS form, I am using Tseitin encoding. My conversion breaks the XORs down to smaller CNF clauses with up to five literals each. Z3 so far is not able to devise a SAT solution.
What could/should I do to improve my encoding?
I have looked at Gaussian elimination, but this probably does not help, because the XOR expressions do not have the same input variables.
Z3 has two SAT solver engines, you can enable the more efficient engine using the strategy framework. For example, see the tutorial Z3 - strategies
There is a section the illustrates the use of strategies for bit-vector formulas:
(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)
That said, it is relatively easy to generate hard instances for CDCL based SAT solvers using XOR. For example:
Randal E. Bryant: A View from the Engine Room: Computational Support for Symbolic Model Checking. 25 Years of Model Checking 2008: 145-149
Z3's more efficient sat solver (called by the example above) have some data-structures for detecting and propagating with xors (equivalences).
