2-SAT variable values

Question

>2-SAT 问题，查找变量的值

我正在使用此解决方案来查找给定公式的满意度。(通过检查 SCC)。如果公式满足，是否有任何有效的方法(在我的情况下，有效意味着不比多项式时间差)如何为每个变量找到值？

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

Answer 1

如链接答案中所述，您可以将 2-SAT 问题转换为暗示图，因为 (x|y) <=> (~x =>y) & (~y => x)

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

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

由于我们构建含义图的方式，规则(2)已经包含在规则(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 之前，当前赋值确定对其有影响的所有内容的真假。

如果问题实例是可以满足的，那么对于问题中提到的每个变量，您将得到一个令人满意的赋值。