2023/04/25 by Yangjun Chen, Chen, Yangjun · 3 voices
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Natural Language Processing Techniques #cs.CC
paper · pdf · doi:10.48550/arxiv.2304.12517
openalex publication_date 2023/04/25 · openalex created_date 2023/04/27 · openalex updated_date 2026/07/28
By the MAXSAT problem, we are given a set V of m variables and a collection C of n clauses over V, i.e., a conjunctive normal form (CNF) formula. We will seek a truth assignment to maximize the number of satisfied clauses in C. This problem is NP-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 D in disjunctive normal form (DNF). We then represent all those truth assignments for a conjunction d as a graph (called a p*-graph), under each of which d evaluates to true. In this way, our task becomes finding a maximum number of p*-graphs, which have a same root-to-leaf path. For this purpose, we organize all the p*-graphs for the conjunctions in D 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 p*-subgraphs), the algorithm can find a maximum set of satisfied conjunctions in D in polynomial time. Its worst-case time complexity is bounded by O(n2m4). This provides in fact a proof of P = NP.