algorithm - 2-SAT 变量值

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 之前，当前分配确定了对其有影响的所有内容的真假。

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