问题标签 [sat]

我正在使用 python 和 Sympy。

我有以下格式的规则：Or(x,And(y,z)). 不幸的是，Sympysubs和xreplace函数没有提供足够快的实现来验证 x=False、y=True 和 z=True 是否满足上述规则。

我怎样才能有效地将这个表达式转换为给定 x、y、z 和规则的其他库，无论这个分配是否满足规则，我都会得到 True/False？

我正在使用 Python 和 Sympy。

我有以下内容：

我在 Sympy 中寻找一个可以返回的True函数rule.eval(doc)？

编辑：目前我正在使用rule.subs，rule.xreplace两者都执行缓慢，每次调用大约 0.0003 秒。这使得它不切实际。

假设我有一个带有 variables 的 CNF 表达式(a,b,c,d,e,f,g)。我将如何使用 SAT 求解器来找到(d,e,f)给定的分配{a,b,c,g} = {1,0,0,1}和{a,b,c,g} = {1,1,1,1}？如果这是一个假设，那么调用 sat 求解器来查找分配{d,e,f}将是直截了当的（例如，通过向 CNF 添加单元子句）。但是如果我有多个假设呢？这可能吗？

我正在为Z3 定理证明器(Z3Py) 使用 Python 绑定。我有 N 个布尔变量，x1,..,xN。我想表达一个约束，即其中 N 个中的 K 个应该为真。在 Z3Py 中我该怎么做？是否有任何内置支持？我查看了在线文档，但Z3Py 文档没有提及任何 API。

对于 N 中取一的约束，我知道我可以分别表示至少一个为真（断言 Or(x1,..,xN)）和至多一个为真（断言 Not(And(xi,xj )) 对于所有 i,j)。我还知道其他手动表达 1-of-N 和 K-out-of-N 约束的方法。但是我的印象是，当求解器内置支持此约束时，它有时会比手动表达更有效。

我需要从用 Scala 编写的应用程序中调用通用 SAT 求解器。我正在研究 SAT4J，因为它可以很容易地作为 jar 文件导入，但是我发现它很难实际使用。有没有办法可以触发 SAT4j jar 文件来从我的 Scala 代码中计算我的 SAT 问题？

如果 SAT4J 不是正确的方法，是否有任何 SAT 库我可以直接使用而不是启动外部 SAT 求解器？

我试图在实际编码之前了解 DPLL 程序。

例如，我有这些条款：

现在我将决策变量设为 d = 0, b = 0。子句现在看起来像这样。

单元传播和纯文字规则如何在这里发挥作用？

此外，在C3 : {1, !a}- 当我服用 时a = 1，这变成了{1, 0}。该子句的最终值应该是多少？应该是{1}吗？

如果任何子句具有 value {!b}，即对文字的否定，在应用决策变量之后，那么如何进行？

最近，我开始研究形式化验证技术。在文献中，模型检查器和求解器以某种方式互换使用。但是，模型检查器和求解器如何相互连接？

ps 如果建议一些论文或链接，我将不胜感激。

这两个 NP 完全问题之间到底有什么区别？在我看来，他们都在询问是否可以满足布尔公式（即输出 1），但一个是在电路的上下文中，另一个只是一个公式。但是，不能从布尔电路中写出一个布尔公式吗？

使用合金 4.2，以下合金模型...

... 执行以下输出：

如果您只是将签名重命名D为H（真正的单字符更改），则基础 SAT 问题的变量和子句的数量会发生变化：

为什么？这种行为什么时候出现？有没有办法命名签名以确保获得尽可能少的变量和子句？

更多细节：

我确信这与签名名称的字母顺序有关。如果您选择任何低于 的名称E，您将获得 486 个变量，如果选择任何高于您的名称，H您将获得 494 个变量。

在我寻找一个最小示例的过程中（从我相当大的模型开始），我目睹了一些情况，其中选择三个不同的名称会产生三个不同数量的变量。我在这个过程中丢失了这些例子，但我记得涉及到字母顺序。

对于小尺寸，这可能看起来没什么，但如果你run {} for 12不是3，变量的数量变为 17415 和 19439，因此差异超过 10%。我也见证了我的实际模型的巨大差异（有更多的签名，但不是更大的范围）。

谢谢，

一个简单的运动规划问题可以改造成一个SAT 求解问题。谁能解释这怎么可能？

在这个问题中，我们必须找到一条从起点到终点的无碰撞路径。