如何将 SMT（包含布尔和有界 int 变量）约束转换为 CNF答案

【问题标题】：How to convert SMT(containing boolean and bounded int variables) constraints to CNF如何将 SMT（包含布尔和有界 int 变量）约束转换为 CNF
【发布时间】：2014-05-09 15:09:07
【问题描述】：

我的申请者原本是 SAT 问题。现在，我正在尝试做一些需要使用一些 int 变量的扩展。所以问题就变成了SMT问题。但是我在使用z3解决的时候遇到了性能问题。由于 int 变量是有界的（小于 100），因此可以将其转换为纯 SAT 问题。

有谁知道如何在 z3 c++ 接口中应用这种策略？或者我可以先使用 z3 将 SMT 约束转换为 SAT 公式，然后再转换尝试其他 SAT 求解器？
提前致谢。

【问题讨论】：

标签： z3

【解决方案1】：

如果您用位向量公式表示您的问题，例如QF_ABV，它将被自动展平为命题公式，并使用 SAT 求解器求解。例如，您可以将少于 100 个整数变量表示为 7 位的位向量。

除了位向量，从 SMT 到 SAT 的转换不会提高您的性能（否则 SMT 将不存在）。因为 SAT 求解器只擅长案例分析和特定理论的决策程序，例如基于单纯形的线性算术算法，在约束求解方面效率更高。

【讨论】：

感谢您的建议！使用 bv 变量替换 int 变量后，性能肯定有所提升。
您知道任何工具可以将包含布尔变量和位向量变量的约束集转换为纯 SAT 问题吗？
AFAIK，转换为 CNF 是位向量的最新技术，但我不知道有任何工具可以将转换后的 CNF 输出到文件中。也许你可以破解 stp 求解器来做到这一点。 sites.google.com/site/stpfastprover 。另请查看其论文dl.acm.org/citation.cfm?id=1770421

【解决方案2】：

如果使用位向量，yices SMT 求解器支持从 SMT 约束转换为 SAT。在 SMT 问题表中使用 (export-to-dimacs "myfile.cnf") 并使用 --logic=QF_BV option 运行 yices。

【讨论】：

据我所知这是行不通的。 yices 与 yices-smt2 不同，它使用 yices 语言而不是 smtlib。我错过了什么吗？