问题标签 [satisfiability]

有人可以以最简单的方式向我解释，如何减少3-SAT到Vertex Cover？我正在按照这里的解释（滚动到第 4 页底部）。我了解拥有两个“小工具”的基本设置：2 节点变量小工具和 3 节点子句小工具。我也将公式理解k = variables + 2 clauses为覆盖所有边缘所需的最小节点数。我不明白的是，这种设置如何证明如果存在 a k-covering，则 CNF 中的布尔表达式是可满足的。具有可满足和不可满足表达式的示例会有所帮助。此外，一旦3-SAT问题转换为 a k-covering，它是否提供了一种方法来识别哪个值（true或false) 应该分配给每个变量以满足布尔表达式？谢谢你的帮助。

我有一个 .cnf 文件，其中包含作为连接范式的数字。

我需要读取它们并将它们存储在数据结构（矩阵或列表）中，以便能够将它们用作索引。（我需要这个来解决 3-SAT 问题。）

如何在 Java 中读取和存储它们？

我在高尔夫球手问题中有一组集合（每周应该有一组，这样没有两个玩家一起玩超过一次，并且每个人每周都玩一次）：

我的限制如下（我不确定一切是否正常）：

我的问题在于约束编号 5。我不能在“var set of int: x”上使用 min，我应该在“set of int: x”上使用它。不幸的是，我不明白这两者之间的区别（从我读过的内容来看，这可能与定义每组的大小有关，但我不确定）。

有人可以向我解释这个问题并提出解决方案吗？我将非常感激。谢谢！

我在想出伪代码来解决布尔可满足性问题时遇到了麻烦，使用最少数量的变量设置为真。

我有一个可满足的 number(H) 方法，我可以调用它来获取需要设置为 true 的变量的最小数量，以便布尔公式可以满足。

}

这是我目前的逻辑。如果我走在正确的轨道上，请告诉我。

我有一个 ANTLR 表达式解析器，它可以使用生成的访问者评估表单 ( A & ( B | C ) ) 的表达式。A 、 B 和 C 可以采用 2 个值中的任何一个true或false。但是，我面临着找到表达式为真的 A、B 和 C 的所有组合的挑战。我试图通过以下方法解决这个问题。

1. 评估 3 个变量的表达式，每个变量取真假
2. 这是 8 种组合，因为 2 ^ 3 是 8
3. 我评估将 000, 001, 010 .... 111 之类的值赋予变量并使用访问者进行评估

虽然这可行，但随着变量数量的增加，这种方法变得计算密集。因此，对于具有 20 个变量的表达式，需要进行 1048576 次计算。如何优化这种复杂性以便获得所有真实的表达式？我希望这属于布尔可满足性问题

假设变量数 N 和子句数 K 相等。找到一种算法，该算法返回满足子句的不同方式的数量。

我读到SAT与独立集有关。

假设我有一个带有 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 添加单元子句）。但是如果我有多个假设呢？这可能吗？

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

例如，我有这些条款：

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

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

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

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

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

我找不到从 3 Sat 到 Set Cover 的“简单”且可以理解的减少。

明天我有考试，这可能是一个问题。

谁能给我解释一下？

感谢所有阅读到这里的人