An Efficient Algorithm for Solving the 2-MAXSAT Problem

Technical Summary: An Efficient Algorithm for Solving the 2-MAXSAT Problem

Problem Definition
The paper addresses the 2-MAXSAT problem, a restricted version of the Maximum Satisfiability (MAXSAT) problem. Given a set $V$ of $m$ Boolean variables and a collection $C$ of $n$ clauses in Conjunctive Normal Form (CNF), where each clause contains at most two literals, the objective is to find a truth assignment that maximizes the number of satisfied clauses. The problem is established as NP-complete, even under this restriction.

Methodology
The proposed algorithm departs from traditional branch-and-bound or approximation methods by transforming the problem into a Disjunctive Normal Form (DNF) maximization task and utilizing a specialized graph-based search structure. The methodology proceeds in three main stages:

1. Transformation to DNF:
   The algorithm constructs a new formula $D$ in DNF from the original CNF formula $C$. For every clause $C_i = l_{i1} \lor l_{i2}$ in $C$, the algorithm introduces a new auxiliary variable $x_i$ and generates two conjunctions: $D_{i1} = l_{i1} \land x_i$ and $D_{i2} = l_{i2} \land \neg x_i$. The resulting formula $D$ consists of $2n$ conjunctions. Proposition 1 in the paper establishes that $C$ has at least $n^*$ satisfiable clauses if and only if $D$ has at least $n^*$ satisfiable conjunctions under a truth assignment for $V \cup \{x_1, \dots, x_n\}$.

2. Graph Representation (p-graphs and Tries):*
   To efficiently represent the truth assignments that satisfy the conjunctions in $D$, the paper introduces the p-graph*.

   • Variable Sequences: Each conjunction is converted into a sorted variable sequence based on the global frequency of variable appearances. Negative literals are handled by introducing a special notation $(c, *)$, representing that variable $c$ can be either true or false (or skipped) without affecting the truth of the conjunction.
   • p-graphs: A directed graph representing a single conjunction where nodes correspond to variables in the sequence. "Spans" (edges skipping variables) represent the $(c, *)$ options.
   • p-graphs:* A refinement of p-graphs where "overlapped spans" (consecutive optional variables) are merged via transitive closure. This ensures that the graph correctly represents all valid truth assignments for a specific conjunction.
   • Trie-like Structure ($G$): All p*-graphs are integrated into a single trie-like graph $G$. This structure clusters common variable sequences to avoid redundant checks. The graph includes "branching nodes" where paths diverge.

3. Recursive Bottom-Up Search:
   The core algorithm, SEARCH(G), explores the graph $G$ in a bottom-up (post-order) manner to find the maximum subset of satisfiable conjunctions.

   • Reachable Subsets (RS): For a branching node $v$, the algorithm calculates "reachable subsets" of nodes reachable via spans from ancestors. These subsets represent groups of conjunctions that can be satisfied simultaneously by bypassing certain variables.
   • Upper Boundaries (upBounds): Based on RSs, the algorithm identifies "upper boundaries"—sets of nodes that allow for the merging of subgraphs.
   • Recursive Construction: When a branching node is encountered, the algorithm constructs a new, smaller trie-like subgraph rooted at the nodes in the upper boundary. A virtual root (the original branching node) is added to maintain connectivity. The algorithm recursively calls SEARCH on these subgraphs.
   • Optimization: To prevent redundant computation, the algorithm employs two improvements: (1) limiting RS calculations to the segment between the current branching node and its lowest ancestor branching node, and (2) using a hash array to cache results of previously visited subgraphs, suppressing repeated recursive calls.

Key Contributions

• Transformation Technique: A polynomial-time reduction of the 2-MAXSAT problem to a maximum satisfiable conjunction problem in DNF.
• p-graph Structure:* The definition of p*-graphs and their transitive closure to accurately and compactly represent truth assignments for conjunctions containing optional variables.
• Recursive Trie Search: A novel recursive algorithm that dynamically builds and searches a trie-like graph structure, utilizing "reachable subsets" and "upper boundaries" to merge solution spaces efficiently.
• Complexity Analysis: The paper provides a detailed analysis claiming the algorithm operates within polynomial time bounds.

Results and Complexity
The paper asserts that the worst-case time complexity of the proposed algorithm is bounded by $O(n^2 m^4)$, where $n$ is the number of clauses and $m$ is the number of variables.

• The construction of the initial trie and p*-graphs takes $O(nm^2)$.
• The recursive search involves at most $O(nm)$ branching nodes.
• Each branching node is involved in at most $O(m)$ recursive calls due to the reduction in graph height at each step.
• The cost to construct a subgraph per call is $O(nm^2)$.
• Combining these factors yields the $O(n^2 m^4)$ bound.

Significance and Claims
The paper concludes that since the 2-MAXSAT problem is known to be NP-complete, the existence of a polynomial-time algorithm to solve it constitutes a proof that P = NP. The authors state that this result provides a proof of P = NP, fundamentally altering the understanding of computational complexity for satisfiability problems. The work is presented as a modification and extension of a conference paper, supported by NSERC, Canada.