Maximum Satisfiability Using Core-Guided MaxSAT Resolution


  • Nina Narodytska University of Toronto and University of New South Wales
  • Fahiem Bacchus University of Toronto



Maximum Satisfiability, MAXSAT resolution


Core-guided approaches to solving MAXSAT have proved to be effective on industrial problems. These approaches solve a MAXSAT formula by building a sequence of SAT formulas, where in each formula a greater weight of soft clauses can be relaxed. The soft clauses are relaxed via the addition of blocking variables, and the total weight of soft clauses that can be relaxed is limited by placing constraints on the blocking variables. In this work we propose an alternative approach. Our approach also builds a sequence of new SAT formulas. However, these formulas are constructed using MAXSAT resolution, a sound rule of inference for MAXSAT. MAXSAT resolution can in the worst case cause a quadratic blowup in the formula, so we propose a new compressed version of MAXSAT resolution. Using compressed MAXSAT resolution our new core-guided solver improves the state-of-theart, solving significantly more problems than other state-ofthe-art solvers on the industrial benchmarks used in the 2013 MAXSAT Solver Evaluation.




How to Cite

Narodytska, N., & Bacchus, F. (2014). Maximum Satisfiability Using Core-Guided MaxSAT Resolution. Proceedings of the AAAI Conference on Artificial Intelligence, 28(1).



Main Track: Search and Constraint Satisfaction