Exact algorithms for MAX-SAT

Citations of this article
Mendeley users who have this article in their library.


The maximum satisfiability problem (MAX-SAT) is stated as follows: Given a boolean formula in CNF, find a truth assignment that satisfies the maximum possible number of its clauses. MAX-SAT is MAX-SNP-complete and received much attention recently. One of the challenges posed by Alber, Gramm and Niedermeier in a recent survey paper asks: Can MAX-SAT be solved in less than 2n "steps"? Here, n is the number of different variables in the formula and a step may take polynomial time of the input. We answered this challenge positively by showing that a popular algorithm based on branch-and-bound is bounded by O(2n) in time, where n is the maximum number of occurrences of any variable in the input. When the input formula is in 2-CNF, that is, each clause has at most two literals, MAX-SAT becomes MAX-2-SAT and the decision version of MAX-2-SAT is still NP-complete. The best bound of the known algorithms for MAX-2-SAT is O(m2m/5), where m is the number of clauses. We propose an efficient decision algorithm for MAX-2-SAT whose time complexity is bound by O(n2n). This result is substantially better than the previously known results. Experimental results also show that our algorithm outperforms any algorithm we know on MAX-2-SAT. ©2003 Published by Elsevier Science B. V.




Zhang, H., Shen, H., & Manyà, F. (2003). Exact algorithms for MAX-SAT. In Electronic Notes in Theoretical Computer Science (Vol. 86, pp. 190–203). Elsevier. https://doi.org/10.1016/S1571-0661(04)80663-7

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free