theoretical computer science

Solving 2-MAXSAT in Polynomial Time: a Proof of =

arXiv:2304.12517

summary

The paper proposes a polynomial‑time algorithm for the NP‑complete 2‑MAXSAT problem by converting it to a DNF maximization task and using graph‑based (p*-graph) and trie‑like structures to find a maximum set of satisfied conjunctions.

Abstract

By the MAXSAT problem, we are given a set of variables and a collection of clauses over , i.e., a conjunctive normal form () formula. We will seek a truth assignment to maximize the number of satisfied clauses in . This problem is -complete even for its restricted version, the 2-maxsat problem, by which every clause contains at most 2 literals. In this paper, we discuss an efficient algorithm to solve this problem. Its main idea is to transform the 2-maxsat problem into a related problem of maximizing satisfied conjunctions of a formula in disjunctive normal form (). We then represent all those truth assignments for a conjunction as a graph (called a *-graph), under each of which evaluates to . In this way, our task becomes finding a maximum number of *-graphs, which have a same path. For this purpose, we organize all the *-graphs for the conjunctions in into a trie-like structure. By exploring the structure and recursively its substructures (with each corresponding to a subgraph dynamically built up by integrating some *-subgraphs), the algorithm can find a maximum set of satisfied conjunctions in in polynomial time. Its worst-case time complexity is bounded by O(). This provides in fact a proof of = .

Topics & keywords

#maxsat#2-sat#algorithm design#graph representation#complexity theory2-MAXSATp*-graphtrie structurepolynomial-time algorithmP=NP claim
Solving 2-MAXSAT in Polynomial Time: a Proof of $\textit{P}$ = $\textit{NP}$ · wovepaper