XOR Clauses for Z3 SAT Solver

Question

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.

Answer 1

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).