An Efficient Algorithm for Solving the 2-MAXSAT Problem

技术摘要：一种求解 2-MAXSAT 问题的有效算法

问题定义
本文研究了 2-MAXSAT 问题，这是最大可满足性（MAXSAT）问题的一个受限版本。给定一组包含 $m$ 个布尔变量 $V$ 的集合，以及一个由合取范式（CNF）组成的 $n$ 个子句集合 $C$，其中每个子句最多包含两个文字。目标是找到一个真值指派，以最大化被满足的子句数量。研究表明，即使在这种限制条件下，该问题也是 NP 完全的。

方法论
所提出的算法通过将问题转化为正规析取范式（DNF）最大化任务并利用专门的基于图的搜索结构，脱离了传统的分支限界法或近似方法。该方法分为三个主要阶段：

1. 向 DNF 转换：
   算法从原始 CNF 公式 $C$ 构建一个新的 DNF 公式 $D$。对于 $C$ 中的每一个子句 $C_i = l_{i1} \lor l_{i2}$，算法引入一个新的辅助变量 $x_i$ 并生成两个合取式：$D_{i1} = l_{i1} \land x_i$ 和 $D_{i2} = l_{i2} \land \neg x_i$。生成的公式 $D$ 由 $2n$ 个合取式组成。论文中的命题 1 证明，当且仅当在 $V \cup \{x_1, \dots, x_n\}$ 的真值指派下，$D$ 至少有 $n^*$ 个可满足的合取式时，$C$ 至少有 $n^*$ 个可满足的子句。

2. 图表示（p-图与 Trie 树）：*
   为了高效表示满足 $D$ 中合取式的真值指派，论文引入了 p-图*。

   • 变量序列： 每个合取式根据变量出现的全局频率转换为排序后的变量序列。负文字通过引入特殊符号 $(c, *)$ 来处理，表示变量 $c$ 可以为真或假（或被跳过），而不影响合取式的真值。
   • p-图： 一个表示单个合取式的有向图，其节点对应于序列中的变量。“跨度”（skip 变量的边）代表了 $(c, *)$ 选项。
   • p-图：* p-图的一种精化形式，其中“重叠跨度”（连续的可选变量）通过传递闭包进行合并。这确保了图能够正确表示特定合取式的所有有效真值指派。
   • 类 Trie 结构 ($G$)： 所有 p*-图被整合进一个单一的类 Trie 图 $G$ 中。该结构通过聚类共同的变量序列来避免冗余检查。图中包含“分支节点”，即路径发生分歧的地方。

3. 递归自底向上搜索：
   核心算法 SEARCH(G) 以自底向上（后序遍历）的方式探索图 $G$，以寻找最大可满足合取式子集。

   • 可达子集 (RS)： 对于分支节点 $v$，算法计算通过祖先节点的跨度（spans）可达到的节点的可达子集。这些子集代表了可以通过绕过某些变量而同时被满足的合取式组。
   • 上界 (upBounds)： 基于 RS，算法识别“上边界”——允许合并子图的节点集合。
   • 递归构建： 当遇到分支节点时，算法构造一个新的、更小的类 Trie 子图，该子图以上边界中的节点为根。添加一个虚拟根（原始分支节点）以保持连通性。算法在这些子图上递归调用 SEARCH。
   • 优化： 为了防止冗余计算，算法采用了两项改进措施：(1) 将 RS 计算限制在当前分支节点与其最低祖先分支节点之间的段内；(2) 使用哈希数组缓存已访问子图的结果，从而抑制重复的递归调用。

主要贡献

• 转换技术： 将 2-MAXSAT 问题多项式时间归约为 DNF 中的最大可满足合取式问题。
• p-图结构：* 定义了 p*-图及其针对包含可选变量的合取式的传递闭包，以准确且紧凑地表示真值指派。
• 递归 Trie 搜索： 一种新型递归算法，它动态地构建并搜索类 Trie 图结构，利用“可达子集”和“上边界”来高效合并解空间。
• 复杂度分析： 论文提供了详细的分析，声称该算法在多项式时间界限内运行。

结果与复杂度
论文断言，所提算法的最坏情况时间复杂度被限制在 $O(n^2 m^4)$，其中 $n$ 是子句数量，$m$ 是变量数量。

• 构建初始 Trie 和 p*-图的时间为 $O(nm^2)$。
• 递归搜索涉及至多 $O(nm)$ 个分支节点。
• 由于每步过程中图高度的降低，每个分支节点最多参与 $O(m)$ 次递归调用。
• 每次调用中构造子图的代价为 $O(nm^2)$。
• 综合这些因素，得出 $O(n^2 m^4)$ 的界限。

意义与主张
论文结论指出，由于 2-MAXSAT 问题已知是 NP 完全的，因此存在求解该问题的多项式时间算法意味着证明了 P = NP。作者表示，这一结果提供了 P = NP 的证明，从根本上改变了对可满足性问题计算复杂性的理解。该工作作为一篇会议论文的修改与扩展进行展示，并由加拿大 NSERC 提供支持。