问题标签 [sat-solvers]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
computer-science - SAT学习资料(布尔可满足性问题)
什么是 SAT(布尔可满足性问题)求解器的好文档。我无法通过谷歌找到好的材料。我发现的文件要么是鸟瞰图,要么是太高级或损坏的 PDF 文件......
您推荐哪些论文/文档来了解现代实用 SAT 求解器中的算法?
java - SAT4J 求解器的输入 CNF
我是 sat4j 求解器的新手..
它说应该给出一些cnf文件作为输入
是否有任何可能的方法将规则作为输入并获取它是否可以满足?
我的规则是这样的:
有人可以帮助我如何使用 sat4j 求解器解决这个问题吗?
java - 如何将布尔表达式转换为 cnf 文件?
我需要使用 sat 求解器来检查布尔表达式的可满足性..
我有这样的复杂布尔表达式
是否有任何自动 cnf 文件转换器,以便我可以直接将其提供给 sat 求解器?
我读了 cnf 格式文件.. 但是如何在 .cnf 文件中表达这个表达式?当括号内有连词以及如何表达 --> 和 <-> 时,我会感到困惑?请帮我
java - 使用 DPLL sat 求解器求解
我在
http://code.google.com/p/aima-java/
我尝试了以下代码来使用 dpllsolver 解决表达式
输入是
CNF 变压器将其转换为
它不考虑逻辑的其他部分,只考虑第一项,如何使其正常工作?
如果其他卫星求解器可以做到,请建议我
.net - 寻找 SMT Z3 用例(如 DbC)和 Z3 的开源替代品的实际示例?
我对 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
z3 - 确定任意命题公式中变量的上限/下限
给定一个任意命题公式 PHI(对某些变量的线性约束),确定每个变量的(近似)上限和下限的最佳方法是什么?
有些变量可能是无界的。在这种情况下,算法应该得出结论,这些变量没有上限/下限。
例如,PHI = (x=3 AND y>=1)。x 的上限和下限均为 3。y 的下限为 1,并且 y 没有上限。
这是一个非常简单的例子,但有没有一般的解决方案(可能使用 SMT 求解器)?
optimization - z3的错误结果
我正在尝试使用 Z3 SMT Solver 证明以下内容:((x*x) + x) = ((~x * ~x) + ~x)
. 这是正确的,因为 c 编程语言中的溢出语义。
现在我编写了以下 smt-lib 代码:
z3 的输出是:
现在我的问题是:为什么结果“不满意”?我的代码中的简化命令表明可以获得有效的分配,以便 myfun1 和 myfun2 具有相同的结果。
我的代码有问题还是z3中的错误?
请任何人都可以帮助我。谢谢
c++ - 提高 dpll 算法的性能
如维基百科中所述,我正在 C++ 中实现DPLL算法:
但表现糟糕。在这一步中:
目前我试图避免创建副本,Φ
而是添加l
ornot(l)
到一个且唯一的副本,并在 /if的 returnΦ
时删除它们。这似乎破坏了给出错误结果的算法(即使集合是)。DPLL()
false
UNSATISFIABLE
SATISFIABLE
有关如何在此步骤中避免显式复制的任何建议?
c++ - 用 C++ 或 haskell 编写的 SAT Solver 的建议。优点和缺点
我需要一个 SAT 求解器库或程序,用 C++ 或 haskell 编写。我想知道您为什么会选择它,以及该库/程序的优缺点是什么。我需要它尽可能快,并且易于使用。
感谢您的回答!