问Z3 SAT求解器的XOR子句
EN

Stack Overflow用户

提问于 2013-01-20 08:31:56

回答 1查看 1.8K关注 0票数 1

我正在使用Z3来解决可满足性问题，包括数百个XOR子句，每个子句有22个输入。为了在DIMACS表单中编写XOR子句，我使用了Tseitin编码。我的转换将XOR分解为更小的CNF子句，每个子句最多包含5个字面量。到目前为止，Z3还不能设计出一个SAT解决方案。

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

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

xor

conjunctive-normal-form

回答 1

Stack Overflow用户

发布于 2013-01-20 09:09:09

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)

也就是说，使用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求解器(由上面的例子调用)有一些用于检测和传播xors (等价)的数据结构。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/14420486

复制

相似问题

问Z3 SAT求解器的XOR子句
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Z3 SAT求解器的XOR子句EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Z3 SAT求解器的XOR子句
EN