A Two-Phase Exact Algorithm for MAX-SAT and Weighted MAX-SAT Problems

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.