将（数学）问题转换为SAT实例

Question

我想做的是将我遇到的数学问题变成布尔值满意度问题（SAT），然后使用SAT求解器解决它。我想知道某人是否知道手册，指南或任何可以帮助我将问题转换为SAT实例的东西。

另外，我想在比指数时间更好的时间内解决这个问题。我希望SAT求解器能帮助我。

Answer 1

SAT手册的第2章（史蒂文·普雷斯特维奇（Steven Prestwich）） 涵盖了如何将离散的决策问题转化为CNF。 （不幸的是，我认为没有在线草稿版本 - 最好咨询您当地的图书馆。）MagnusBjörk的古怪概述中引用的其他一些参考文献 成功的SAT编码技术 也很有用。

如果您的问题是连续的，或者您对不平等系统特别感兴趣，那么其他类型的求解器更有可能有用。正如凯尔（Kyle）指出的那样，SMT求解器（例如 Z3, YICES, ， 或者 Opensmt）可能很有用，尽管传统上SMT理论倾向于专注于计算机软件的验证，因此SMT求解器通常对涉及整数间隔的表达方式有很大的支持，但在注射率约束方面的表现较差。对于自然表达为不平等系统的问题， cplex 是要击败的人（过去可以免费提供学术用途，而且可能仍然是）。对于某些组合决策问题（例如查找 矩形包装到广场上），诸如 奴才 表现优于SAT求解器，通常更易于使用。

Answer 2

除非您将数学问题转化为学习练习，否则您的时间将花在学习上。 令人满意的模型理论. 。 SMT将使您比布尔SAT实例更自然地表达方程式和其他约束。一些SMT求解器支持存在和通用的量化器，使您可以超越NP并表达Pspace问题。

除了表现力之外，SMT求解器的速度更快。不是p = np更快，但更有效的是，良好的SMT求解器不会丢弃特定于理论的结构信息，从而帮助指导求解器穿越搜索空间。直接将KARP减少到SAT实例上，迫使SAT求解器通常以指数成本重新学习所有结构。例如，在基于DPLL和基于本地搜索的SAT求解器上丢失了添加性能的事实；求解器根本不知道它正在处理数字！为了避免尝试X+Y+Z = 10的所有排列，SAT求解器需要对称的代码，这需要图形自动形态检测。当前最佳的图形自动形态识别算法需要在最坏情况下的顶点数量的时间指数，因此可能会花费指数时间来重新学习一个简单的算术规则。

Answer 3

将高级语言转换为SMT或CNF的两个工具。

CVC 语法靠近CAS。

CBMC 它将C程序转换为CNF，允许断言。断言要么始终为真，要么是错误的反例输入。 CBMC展开循环，因此某些C程序具有指数较大的CNF/SMT。