Maximum satisfiability using core-guided MAXSAT resolution

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