2-SAT问题，寻找变量值
我用这个来寻找给定公式的可满足性。（通过检查SCC）如果公式是可满足的，有没有有效的方法（在我的例子中，有效的方法不比多项式时间差）来找到每个变量的值？
它不必是C++，我只是使用相同的算法。
最佳答案
如链接答案中所述，可以将2-SAT问题转化为蕴涵图，因为（x y）（~x=>y）&（~y=>x）
为了做出一个令人满意的赋值，我们需要为每个变量x选择x或~x，以便：
如果我们选择了一个术语x，那么我们也选择了x在蕴涵图的传递闭包中所暗示的一切，同样对于~x；和
如果我们选择x，那么我们也选择了蕴涵图的传递闭包中蕴涵~x的所有事物的否定。
由于我们构造蕴涵图的方式，规则（2）已经被规则（1）覆盖。如果（a=>~x）在图中，那么（x=>~a）也在图中如果（a=>b）&（b=>~x），那么我们有（x=>~b）&（~b=>~a）。
所以实际上只有一条规则。这就产生了一种类似于拓扑排序的线性时间算法。
如果我们将图中的每个SCC折叠成一个顶点，结果将是非循环的因此，图中必须至少有一个scc，它没有传出含义。
所以：
将所选分配初始化为空；
选择没有传出含义的SCC。如果它与当前工作分配中的任何内容都不矛盾，则将其所有术语添加到当前工作分配中。否则，添加对其所有术语的否定，并为每个直接暗示它的scc添加至少一个矛盾。
从图中删除选定的SCC，然后返回（2）直到图为空。
重复此操作，直到图形为空。进程将始终终止，因为删除SCC不会引入周期。
步骤（2）确保在我们从图中删除SCC之前，当前赋值确定了对它有影响的所有内容的真假。
如果问题实例是可满足的，那么您将为问题中提到的每个变量留下一个令人满意的赋值。