z3 - Z3 SAT 求解器的 XOR 子句

Question

我正在使用 Z3 解决可满足性问题，包括数百个 XOR 子句，每个子句有 22 个输入。为了以 DIMACS 形式编码 XOR 子句，我使用了 Tseitin 编码。我的转换将 XOR 分解为更小的 CNF 子句，每个子句最多五个字面值。到目前为止，Z3 无法设计 SAT 解决方案。

我可以/应该做些什么来改进我的编码？

我看过高斯消元法，但这可能没有帮助，因为 XOR 表达式没有相同的输入变量。

Answer 1

Z3 有两个 SAT 求解器引擎，您可以使用策略框架启用更高效的引擎。例如，参见教程Z3 - 策略

有一节说明了位向量公式的策略的使用：

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

也就是说，使用 XOR 为基于 CDCL 的 SAT 求解器生成硬实例相对容易。例如：

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

Z3 更高效的 sat 求解器（由上面的示例调用）具有一些数据结构，用于检测和传播 xor（等价）。