问题标签 [sat-solvers]

什么是 SAT（布尔可满足性问题）求解器的好文档。我无法通过谷歌找到好的材料。我发现的文件要么是鸟瞰图，要么是太高级或损坏的 PDF 文件......

您推荐哪些论文/文档来了解现代实用 SAT 求解器中的算法？

我是 sat4j 求解器的新手..

它说应该给出一些cnf文件作为输入

是否有任何可能的方法将规则作为输入并获取它是否可以满足？

我的规则是这样的：

有人可以帮助我如何使用 sat4j 求解器解决这个问题吗？

我需要使用 sat 求解器来检查布尔表达式的可满足性..

我有这样的复杂布尔表达式

是否有任何自动 cnf 文件转换器，以便我可以直接将其提供给 sat 求解器？

我读了 cnf 格式文件.. 但是如何在 .cnf 文件中表达这个表达式？当括号内有连词以及如何表达 --> 和 <-> 时，我会感到困惑？请帮我

我在

http://code.google.com/p/aima-java/

我尝试了以下代码来使用 dpllsolver 解决表达式

输入是

CNF 变压器将其转换为

它不考虑逻辑的其他部分，只考虑第一项，如何使其正常工作？

如果其他卫星求解器可以做到，请建议我

我对 SMT Z3 使用（如 DbC）的实际示例感兴趣并寻找该工具的代码和开源替代品。所以，其实我对类似的Z3形式求解工具很感兴趣，但是：

• 它必须是开源的
• 提供低级（API）和高级（文本脚本）交互
• 支持 SMT-LIB
• 适用于（可用）工具/编写/用于 Java、python、ruby、Vala 等语言，而不是Haskell
• 有基于它的稳定（在实践中可用）工具，如按合同设计（DbC）、静态类型验证等。

根据 SMT-LIB 主页（详见 bit.ly bundle），2010 年 SMT 求解器列表为：“Alt-Ergo、Barcelogic、Beaver、Boolector、CVC3、DPT、MathSAT、OpenSMT、SatEEn、Spear、STP、SWORD、 UCLID、veriT、Yices、Z3。”

请就在实践中使用它们提供任何反馈（代码示例是最好的）？

最后，将它与 GHC 可能性进行比较的任何信息都是有用的，但前提是存在实现示例（不是语言“功能”）。

更多关于 Z3 的快速信息在这里http://bit.ly/bundles/ewiger/1

给定一个任意命题公式 PHI（对某些变量的线性约束），确定每个变量的（近似）上限和下限的最佳方法是什么？

有些变量可能是无界的。在这种情况下，算法应该得出结论，这些变量没有上限/下限。

例如，PHI = (x=3 AND y>=1)。x 的上限和下限均为 3。y 的下限为 1，并且 y 没有上限。

这是一个非常简单的例子，但有没有一般的解决方案（可能使用 SMT 求解器）？

我正在尝试使用 Z3 SMT Solver 证明以下内容：((x*x) + x) = ((~x * ~x) + ~x). 这是正确的，因为 c 编程语言中的溢出语义。

现在我编写了以下 smt-lib 代码：

z3 的输出是：

现在我的问题是：为什么结果“不满意”？我的代码中的简化命令表明可以获得有效的分配，以便 myfun1 和 myfun2 具有相同的结果。

我的代码有问题还是z3中的错误？

请任何人都可以帮助我。谢谢

是否有一个开源 java 解析工具可以通过方法枚举控制流路径并计算整数变量的范围约束？（Sat-solver 也会很棒）

- 编辑 -

这是引发这个问题的答案。

这是我正在考虑的工具的商业版本。

我的问题是 - 最接近的开源等价物是什么？

如维基百科中所述，我正在 C++ 中实现DPLL算法：

但表现糟糕。在这一步中：

目前我试图避免创建副本，Φ而是添加lornot(l)到一个且唯一的副本，并在 /if的 returnΦ时删除它们。这似乎破坏了给出错误结果的算法（即使集合是）。DPLL()falseUNSATISFIABLESATISFIABLE

有关如何在此步骤中避免显式复制的任何建议？

我需要一个 SAT 求解器库或程序，用 C++ 或 haskell 编写。我想知道您为什么会选择它，以及该库/程序的优缺点是什么。我需要它尽可能快，并且易于使用。

感谢您的回答！