algorithm - 2-可满足性和强连通分量

Question

我知道在有向图中应用强连通分量，如果问题可以在多项式时间内解决，我们可以检查2-SAT 布尔可满足性。

让我们假设问题是可以满足的。

问题：是否有通用算法来计算依赖于 2-SAT 的解决方案？

Answer 1

假设我正确理解了您的问题，是的，有一个通用算法可以通过使用可满足性问题的算法来找到解决方案（即令人满意的分配）。

假设我为变量 x _i分配值“true”（因此文字 x _i为真，~x _i为假）以从原始创建一个新的 2-CNF。如果我要对其运行可满足性（即使用带有 SCC 的东西来查找新的 CNF 是否可满足）：

1. 如果生成的 CNF 现在不能满足，它会告诉您关于原始 CNF 中令人满意的分配的什么？
2. 如果生成的 CNF仍然可以满足，它会告诉您关于原始 CNF 中令人满意的分配的什么？

该算法背后的想法是，如果您遇到案例 1，则使变量为“假”，如果您遇到案例 2，则为“真”，并循环遍历每个变量（保留您对已经查看过的变量所做的分配） . 一旦你能回答我提出的问题，你就会理解它背后的概念。