问题标签 [2-satisfiability]

我有一个问题是 2-SAT 问题的扩展。在标准的 2-SAT 问题中，我们可以找到任何取决于我们选择的顶点顺序的真值分配。我想检查是否存在一个且只有一个真值赋值（即只有一个组合），表达式可以满足。文字的数量可以是 100000。一种方法是找到所有可能的真值分配，然后比较它们是否不同。但问题是对于每次比较，我将不得不比较 100000 个值（没有文字）。有什么有效的方法吗？

我想为 100000 个文字实现 2-SAT 问题。所以会有200000个顶点。所以我坚持拥有一个来自每个顶点的所有可到达顶点的数组，其空间复杂度 O(200000^2)是不可行的所以请为此提出一个解决方案。并请对 2-SAT 问题的有效实施有所了解。

我已经为 2-satisfiability 问题编写了一个 SAT 求解器，有人请给我一个测试用例，比如 10000 个文字，它只有一个可满足的分配，即只有一个解决方案

我一直在寻找一段时间，但我似乎无法找到 2-Sat 算法的任何实现。

我在 c++ 中使用 boost 库（它有一个强连接的组件模块），需要一些指导来创建一个高效的 2-Sat 程序或找到一个现有的库供我通过 c++ 使用。

每当我搜索 2-Sat 的算法时，我都会返回问题决策形式的算法：是否存在满足所有子句的合法值集。但是，这并不能让我轻松找到一组令人满意的布尔值。

如何有效地找到一组满足 2-Sat 实例的合法值？

我正在使用 boost 库在 c++ 中工作，并且希望能够轻松集成代码。

提前致谢

我目前正在为考试研究 2SAT 问题，但我真的不明白如何使用蛮力检查解决方案是否存在。我知道这看起来有点奇怪，但我了解如何更好地实现蕴含图，但我不太确定如何实现蛮力策略。

有人可以分享一些见解吗？也许在伪代码或java中。

谢谢

我正在使用以下代码：

输出为：在此处在线运行此示例

在此示例中，矩阵 M 将 2-SAT 实例定义为 CNF（参考）。在这个例子中，矩阵 M 是手动引入的。请让我知道如何自动引入矩阵 M ( matrix )。非常感谢。

我知道在有向图中应用强连通分量，如果问题可以在多项式时间内解决，我们可以检查2-SAT 布尔可满足性。

让我们假设问题是可以满足的。

问题：是否有通用算法来计算依赖于 2-SAT 的解决方案？

蕴涵图是一个有向图，其中每个节点都被指定为真或假，并且任何边都u -> v暗示if u is true then v is true。

我知道一种简单的O(n^2)算法，可以在一般蕴涵图中找到分配以及O(n)某些特殊情况的算法（例如由2-SAT问题引起的蕴涵图）。

所以我想知道是否有O(n)算法找到任何暗示图的分配？

我阅读了许多用于查找 2-SAT 问题的算法，即给定的表达式是否可满足，可以在多项式时间内求解。示例（算法）。
对于Krom 的过程（维基百科），我构建了一个图，从中我可以轻松地验证它在多项式时间内的可满足性。
现在，我想找到这个表达式的解决方案是令人满意的。
我是这样想的（验证它）：首先我取任何形成强连通分量的表达式文字，比如 x，并将值赋值为 0。然后根据算法，存在边（x！-> y）。因此 y 不能为 0。（因为 1 -> 0 为假）并且如果可能，类似地继续。
否则取 x=0，然后只能选择 y=1，然后类似地继续获取任何 1 个可满足的实例。

现在，是否有任何可行的解决方案可以在多项式时间内找到其中任何一个

• 给出表达式可满足的所有可能解。
• 或者这个表达式对于总 k 字面量 = 1 的输入是否可以满足。
• 或者有多少最小数量的文字具有值 1 才能满足表达式。

对于这类问题，我没有得到任何多项式算法。