Maximum Satisfiability Using Core-Guided MaxSAT Resolution

By Nina Narodytska, Fahiem Bacchus. 2014

167 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Computer Networks and Communications

Citations in the corpus

Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT (2015, methodology): “Eva: the best-performing solver in the weighted partial industrial category of MaxSAT Evaluation 2014 [Narodytska and Bacchus, 2014].”
MaxSMT-Based Type Inference for Python 3 (2018, methodology): “Typpete relies on Z3 [7] and the MaxRes [18] algorithm for solving the generated type constraints.”
Core-Boosted Linear Search for Incomplete MaxSAT (2019, methodology): “For related work from the ﬁeld of complete MaxSAT solving, the Primal-Dual MaxSAT algorithm [18] extends PMRES with a second instance reformulation used to rule out solutions that falsify the same clauses as an intermediate so-lution obtained during search.”