Z3 SAT 求解器的 XOR 子句答案

【问题标题】：XOR Clauses for Z3 SAT SolverZ3 SAT 求解器的 XOR 子句
【发布时间】：2013-01-20 00:31:56
【问题描述】：

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

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

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

【问题讨论】：

标签： z3 xor conjunctive-normal-form

【解决方案1】：

Z3 有两个 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)

也就是说，生成hard比较容易使用 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 求解器（由上面的示例调用）有一些用于检测和传播异或（等价）的数据结构。

【讨论】：

使用 SMT2 输入格式和位向量通常/可能比使用 DIMACS/CNF 作为 Z3 输入更有效？
快速注释：1- 高效 SAT 求解器默认用于仅包含位向量的问题，因此无需使用check-sat-using。 2- Z3 不支持 CryptoMinisat 等异或子句。以 SMT2 输入格式对问题进行编码将无济于事。对 Xor 子句的支持并不难实现。但是，它不在我们的 TODO 列表中。如果您有兴趣，我可以展示在 Z3 中实施 Crytominisat 方法需要做些什么。