algorithm - 2-SAT变量值

Question

2-SAT 问题，寻找变量的值

我正在使用这个 solution寻找给定公式的可满足性。 (通过检查 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 之前，当前分配会确定与其有关联的所有内容的真假。

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