2-SAT 问题,寻找变量的值
我正在使用这个 solution寻找给定公式的可满足性。 (通过检查 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) .
所以实际上只有规则 (1)。这导致类似于拓扑排序的线性时间算法。
如果我们要将图中的每个 SCC 折叠成一个顶点,结果将是非循环的。图中必须至少有一个 SCC,因此,它没有外向影响。
所以:
- 将选定的赋值初始化为空;
- 选择一个没有外向影响的 SCC。如果它与当前作业中的任何内容都不矛盾,则将其所有术语添加到当前作业中。否则,添加其所有条款的否定,并为每个直接暗示它的 SCC 添加至少一个矛盾。
- 从图中删除选定的 SCC,然后返回 (2),直到图中为空。
重复直到图表为空。该过程将始终终止,因为删除 SCC 不会引入循环。
步骤 (2) 确保,在我们从图中删除 SCC 之前,当前分配会确定与其有关联的所有内容的真假。
如果问题实例是可满足的,那么您将为问题中提到的每个变量留下一个令人满意的分配。
关于algorithm - 2-SAT变量值,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/55783720/