New Inference Rules for Efficient Max-SAT Solving

Proceedings of the AAAI Conference on Artificial Intelligence, 21

Volume

Technical Papers

Constraint Satisfaction and Satisfiability

In this paper we augment a Max-SAT solver with three new inference rules. The three of them are special cases of Max-SAT resolution with which better lower bounds and more value pruning is achieved. Our experimental results on several domains show that the resulting algorithm can be orders of magnitude faster than state-of-the-art Max-SAT solvers and the best Weighted CSP solver.