2-SAT变量值

Question

2-SAT problem, finding value for variables

我正在使用这个solution来寻找给定公式的可满足性。 （通过检查SCC）。有没有任何有效的方法（有效的方法不比我的情况下的多项式时间更差）如果公式是可满足的，如何找到每个变量的值？

它不一定是在C ++中，我只是使用相同的算法。

Answer 1

如链接答案中所述，您可以将2-SAT问题转换为蕴涵图，因为（x | y）<=>（~x => y）＆（~y => x）

为了做出令人满意的赋值，我们需要为每个变量x选择x或~x，这样：

1. 如果我们选择一个术语x，那么我们也会在蕴涵图的传递闭包中选择x暗示的所有内容，对于~x同样如此;和
2. 如果我们选择x，那么我们也选择在蕴涵图的传递闭包中暗示~x的所有内容的否定。

由于我们构建蕴涵图的方式，规则（1）已经涵盖了规则（1）。如果（a => ~x）在图中，那么（x => ~a）也在图中。如果（a => b）＆（b => ~x），那么我们有（x => ~b）＆（~b => ~a）。

所以真的只有规则（1）。这导致线性时间算法类似于拓扑排序。

如果我们将图中的每个SCC折叠成单个顶点，结果将是非循环的。因此，图中必须至少有一个SCC，没有外向影响。

所以：

1. 将所选分配初始化为空;
2. 选择没有传出含义的SCC。如果它与当前分配中的任何内容都不矛盾，则将其所有术语添加到当前分配中。否则，添加其所有术语的否定，并为每个直接暗示它的SCC添加至少一个矛盾。
3. 从图中删除选定的SCC，然后返回（2）直到图表为空。

重复，直到图表为空。该过程将始终终止，因为删除SCC不会引入循环。

步骤（2）确保在我们从图中移除SCC之前，当前的分配确定了对其有意义的所有事物的真实性或错误性。

如果问题实例是可满足的，那么您将为问题中提到的每个变量留下令人满意的赋值。