A branch and cut algorithm for MAX-SAT and weighted MAX-SAT
Steve Joy, John E. Mitchell, Brian Borchers · DIMACS series in discrete mathematics and theoretical computer science · 1997
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 nodewe 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. Our algorithm is more e ective than EDPL on some problems, notably MAX-2-SAT. EDPL is more e ective on some other classes of problems.