如何获取 2-Sat 值

Question

每当我搜索 2-Sat 的算法时，我都会得到问题决策形式的算法：是否存在满足所有条款的合法值集。然而，这不允许我轻松找到一组令人满意的布尔值。

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

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

提前致谢

Answer 1

如果您有用于检测是否存在有效的分配到2-SAT的决定算法，你可以用它来真正找出实际的分配。

首先对整个表达运行2-SAT决定算法。假设它说，有一个有效的分配。

现在如果X_1是文字，分配X_1为0。现在计算2-SAT用于将所得的表达（你将不得不分配因为这样一些其它的文字，例如，如果X_1 OR X_3出现，还需要到集X_3为1）。

如果所得expresion是2-满足的，则可以采取X_1为0，否则取X_1为1。

现在，你可以发现这一点对每个文字。

有关更有效的算法，我建议你尝试使用蕴涵图方法。

您可以在这里找到更多的信息： http://en.wikipedia.org/wiki/ 2-可满足

在相关部分：

  

2满足性实例是   解当且仅当每一个变量   实例的属于不同的   强连通分量的   蕴涵图比的否定   相同的变量。由于强烈   连接的组件可参见   基于由算法线性时间   深度优先搜索，相同的线性   约束时间，适用于好   2-满足性。

在各强连通分量的文字或者是全零或全1。

Answer 2

至少有一种算法列出了 2-sat 问题的所有解决方案，作者：Tomas Feder： http://www.springerlink.com/content/j582276p06276l12/