×

zbMATH — the first resource for mathematics

New upper bounds for maximum satisfiability. (English) Zbl 0959.68049
Summary: The (unweighted) MAXimum SATisfiability problem (MAXSAT) is: Given a Boolean formula in conjunctive normal form, find a truth assignment that satisfies the largest number of clauses. This paper describes exact algorithms that provide new upper bounds for MAXSAT. We prove that MAXSAT can be solved in time \(O(|F|\cdot 1.3803^K)\), where \(|F|\) is the length of a formula \(F\) in conjunctive normal form and \(K\) is the number of clauses in \(F\). We also prove the time bounds \(O(|F|\cdot 1.3995^k)\), where \(k\) is the maximum number of satisfiable clauses, and \(O(1.1279^{|F|})\), for the same problem. For MAX2SAT this implies a bound of \(O(1.2722^K)\).

MSC:
68Q25 Analysis of algorithms and problem complexity
03D15 Complexity of computation (including implicit computational complexity)
Software:
MAX-2-SAT
PDF BibTeX XML Cite
Full Text: DOI