Partial Max-SAT solvers with clause learning

We describe three original exact solvers for Partial Max-SAT: PMS, PMS-hard, and PMS-learning. PMS is a branch and bound solver which incorporates efficient data structures, a dynamic variable selection heuristic, inference rules which exploit the fact that some clauses are hard, and a good quality lower bound based on unit propagation. PMS-hard is built on top of PMS and incorporates clause learning only for hard clauses; this learning is similar to the learning incorporated into modern SAT solvers. PMS-learning is built on top of PMS-hard and incorporates learning on both hard and soft clauses; the learning on soft clauses is quite different from the learning on SAT since it has to use Max-SAT resolution instead of SAT resolution. Finally, we report on the experimental investigation in which we compare the state-of-the-art solvers Toolbar and ChaffBS with PMS, PMS-hard, and PMS-learning. The results obtained provide empirical evidence that Partial Max-SAT is a suitable formalism for representing and solving over-constrained problems, and that the learning techniques we have defined in this paper can give rise to substantial performance improvements.