问题标签 [sat]

我必须解决一个SAT问题。该问题有 2 个基数约束，第一个是：每天最多 6 个“同一阶段的班级”，“大学”每天“开放”12 小时，因此您必须生成约束以将它们应用于 SAT 求解器。

第二个基数约束是：每个受试者每周必须至少有 X 小时。

我一直在阅读，第一个最好的方法可能是“排序网络算法”，我不知道第二个虽然我不知道如何实现，甚至都没有开始在 prolog 中实现它。

我在 Z3 中有一堆布尔变量，比如ai,bj和ck, 来制定我的 SAT 问题。但是，在我的问题中，需要考虑三个算术约束：

如何在不更改变量类型的情况下使用 Z3 API 制定这三个算术约束（即，默认情况下都是布尔值）？

我正在研究研究工具的一个组成部分；我有兴趣检索（用于 QF_LRA）

-多个（最小或其他）UNSAT核心和
-多个SAT分配

我在论坛上查看了有关此主题的早期讨论，例如， 如何在逻辑 QF_LRA 上使用 z3 时获得不同的未饱和内核

他们指的是 z3 Python 教程，例如http://rise4fun.com/Z3Py/tutorial/musmss

目前似乎处于离线状态。我尝试了 github 等的其他建议来找到提到的教程，但没有运气。

我正在使用 z3 Java API；但很高兴转向替代品。

有没有办法使用 SMTLIB2 语法检索所有令人满意的分配？

我使用的求解器是 Z3 和 CVC4。

我对 sat4j 求解器和研究布尔可满足问题是全新的；我被卡住了。我想制作一个程序来解决布尔公式中的整数变量，例如；

x1 < x2 + x3 用户输入该公式，我的程序满足该公式（返回真），如 x1 = 5 ，x2 = 3，x3 = 4。所以公式返回真，用户得到满足公式的整数值。是可以在 sat4j 中实现它，因为我使用 java 在 eclipse 中工作。

很抱歉重新发布这个问题， 如何让 z3 返回多个 unsat 核心，多个令人满意的分配

为了完整起见，上面链接中的原始问题是：

我有兴趣检索（用于 QF_LRA）

-多个（最小或其他）UNSAT核心和-多个SAT分配

我在论坛上查看了有关此主题的早期讨论，例如，如何在逻辑 QF_LRA 上使用 z3 时获得不同的未饱和内核。这些是指 z3 Python 教程，例如 http://rise4fun.com/Z3Py/tutorial/musmss，目前似乎已离线。我尝试了 github 等的其他建议来找到提到的教程，但没有运气。

感谢 Nikolaj Bjorner 发布了我之前问题的答案。但是，我不确定答案中发布的代码片段是否完整？有人可以对此发表评论吗？

我查看了引用的论文和 Mark Liffiton 的网页，在我原来的问题的答案中提到。如果可以重新发布或澄清完整的代码片段，那将是最有帮助的。

非常感谢

让我们从这里开始：据说所有的NP问题都可以简化为SAT（布尔可满足性问题）。更准确地说是Circuit SAT，因为像 NP 这样的所有决策问题都应该以Yes或No的答案结束。

但是现在，如果我有一个随机 NP 问题，如何构建一个布尔电路来测试，如何对我的输入进行分组，什么样的门（AND、NOT、OR 等）应该连接这些输入。所以基本上，我的问题是如何设计给出答案TRUE 或 FALSE的布尔电路。

最后一件事，这个答案是什么意思。我理解 TRUE，因为这个 NP 问题可以在多项式时间内解决，而 FALSE 不能，对吗？

我脑子里一片混乱，如果我在解释我的问题时犯了逻辑错误，请不要太离谱:)我希望你能理解。

兴奋地等待答案。

我正在寻找有关如何将数学方程编码为 cnf-sat 形式的想法，以便它们可以通过像 MiniSat 这样的开源 SAT 求解器来求解。

那么，我该如何转换：

3x + 4y - z = 14

-2x - 4z <= -6

x - 3y + z >= 15

成一个命题方程，可以使用 SAT Solvers 求解。

有什么建议，因为我很难过？？

我正在尝试编写一个算法来天真地寻找布尔公式（NNF，但不是 CNF）的模型。

我拥有的代码可以检查现有模型，但是当被要求查找模型时它会失败（或无法完成），似乎是因为它生成了无限多member(X, Y)的解决方案[X|_], [_,X|_], [_,_,X|_]...

我到目前为止是这样的：

是否有更好的数据结构F或其他方式可以切断部分实例化的列表？

编辑：添加定义和示例。

z3 -smt2 <filename>只输出“sat”或“unsat”。如果满足约束，我希望 Z3 输出模型，如果不满足，则输出 unsat 核心。我应该使用 Z3 的哪些选项？