Exact Algorithms for MAX-SAT
Issue date
2003Author
Zhang, Hantao
Shen, Haiou
Manyà Serres, Felip
Suggested citation
Zhang, Hantao;
Shen, Haiou;
Manyà Serres, Felip;
.
(2003)
.
Exact Algorithms for MAX-SAT.
Electronic Notes in Theoretical Computer Science, 2003, vol. 86, núm. 1, p. 190-203.
https://doi.org/10.1016/S1571-0661(04)80663-7.
Metadata
Show full item recordAbstract
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 distinct 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.
Is part of
Electronic Notes in Theoretical Computer Science, 2003, vol. 86, núm. 1, p. 190-203European research projects
Collections
The following license files are associated with this item: