zbMATH — the first resource for mathematics

A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems. (English) Zbl 0954.90026
Summary: We describe a two-phase algorithm for MAX-SAT and weighted MAX-SAT problems. In the first phase, we use the GSAT heuristic to find a good solution to the problem. In the second phase, we use an enumeration procedure based on the Davis-Putnam-Loveland algorithm, to find a provably optimal solution. The first heuristic stage improves the performance of the algorithm by obtaining an upper bound on the minimum number of unsatisfied clauses that can be used in pruning branches of the search tree.
We compare our algorithm with an integer programming branch-and-cut algorithm. Our implementation of the two-phase algorithm is faster than the integer programming approach on many problems. However, the integer programming approach is more effective than the two-phase algorithm on some classes of problems, including MAX-2-SAT problems.

90C10 Integer programming
90C57 Polyhedral combinatorics, branch-and-bound, branch-and-cut
90C59 Approximation methods and heuristics in mathematical programming
Full Text: DOI