Solving MAX-SAT and Weighted MAX-SAT Problems Using Branch-and-Cut

Download the paper, postscript or pdf.
Steve Joy
Mathematics Department,
Rensselaer Polytechnic Institute,
Troy, NY 12180.
email:joys@rpi.edu

John E. Mitchell
Mathematics Department,
Rensselaer Polytechnic Institute,
Troy, NY 12180.
email:mitchj@rpi.edu

Brian Borchers
Mathematics Department,
New Mexico Tech, 
Socorro, NM 87801.
email:borchers@nmt.edu

February 28, 1998.

Abstract: We describe a branch and cut algorithm for both MAX-SAT and weighted MAX-SAT. This algorithm uses the GSAT procedure as a primal heuristic. At each node we solve a linear programming (LP) relaxation of the problem. Two styles of separating cuts are added: resolution cuts and odd cycle inequalities. We compare our algorithm to an extension of the Davis Putnam Loveland (EDPL) algorithm and a Semi-Definite Programming (SDP) approach. Our algorithm is more effective than EDPL on some problems, notably MAX-2-SAT. EDPL and SDP are more effective on some other classes of problems.

Download the paper, postscript or pdf.

Return to my list of papers.