data-structures - 2-可满足性问题中的实现问题

Question

我想为 100000 个文字实现 2-SAT 问题。所以会有200000个顶点。所以我坚持拥有一个来自每个顶点的所有可到达顶点的数组，其空间复杂度 O(200000^2)是不可行的所以请为此提出一个解决方案。并请对 2-SAT 问题的有效实施有所了解。

Answer 1

来自维基百科：

... 2-可满足性可以在多项式时间内求解。Aspvall , Plass & Tarjan (1979)观察到，一个 2-satisfiability 实例是可解的，当且仅当实例的每个变量都属于暗示图的不同强连通分量而不是同一变量的否定。由于基于深度优先搜索的算法可以在线性时间内找到强连通分量，因此相同的线性时间界限也适用于 2-可满足性。

我不会假装理解那段的大部分内容，但似乎有一种算法可用于解决 2-SAT 问题，并且在该参考文档中进行了描述（A linear-time algorithm for testing the某些量化布尔公式的真实性）。它显然可以在网上以大约 20 美元的价格购买。我不确定这是否有帮助，但确实有！

更新：可以在此处找到同一文档的免费 PDF 。归功于 liori的发现。

Answer 2

这整个线程有点混乱。是的，一个人可以在线性时间内解决 2-sat，但不——你不能解决那么多变量。求解 2-sat 的时间与蕴涵的数量呈线性关系，对于 200 000 个变量，蕴涵的数量可能达到 (200000*199999)/2，此外，如果您使用此解决方案，您将需要大约相同数量的内存. 还有另一种解决方案（不使用速度较慢但不需要那么多内存的强连接组件）。