A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems. (English) Zbl 0954.90026

Borchers, Brian; Furman, Judith

J. Comb. Optim. 2, No. 4, 299-306 (1999).

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.

MSC:

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

Keywords:

MAX-SAT and weighted MAX-SAT problems; heuristic; integer programming; branch-and-cut algorithm

Software:

MINTO