Efficient strategies for (weighted) maximum satisfiability

It is well known that the Davis-Putnam-Logemann-Loveland (DPLL) algorithm for satisfiability (SAT) can be extended to an algorithm for maximum SAT (max-SAT). In this paper, we propose a number of strategies to significantly improve this max-SAT method. The first strategy is a set of unit propagation rules; the second is an effective lookahead heuristic based on linear programming; and the third strategy is a dynamic variable ordering that exploits problem constrainedness during search. We integrate these strategies in an efficient complete solver for both max-SAT and weighted max-SAT. Our experimental results on random problem instances and many instances from SATLIB demonstrate the efficacy of these strategies and show that the new solver is able to significantly outperform most of the existing complete max-SAT solvers, with a few orders of magnitude of improvement in running time in many cases.