SAT-based MaxSAT algorithms
MetadataShow full item record
Many industrial optimization problems can be translated to MaxSAT. Although the general problem is NP hard, like SAT, many practical problems may be solved using modern MaxSAT solvers. In this paper we present several algorithms specially designed to deal with industrial or real problems. All of
them are based on the idea of solving MaxSAT through successive calls to a SAT solver. We show that this SAT-based technique is efficient in solving industrial problems. In fact, all state-of-the-art MaxSAT solvers that perform well in industrial instances are based on this technique. In particular, our solvers won the 2009 partial MaxSAT and the 2011 weighted partial MaxSAT industrial categories of the MaxSAT evaluation. We prove the correctness of all our algorithms. We also present a complete experimental study comparing the performance of our algorithms with latest MaxSAT solvers.
Is part ofArtificial Intelligence, 2013, vol. 196, p. 77-105
Showing items related by title, author, creator and subject.
Ansótegui Gil, Carlos José; Bonet, Maria Luisa; Giráldez-Cru, Jesús; Levy, Jordi (Springer Verlag, 2014)Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is believed that these techniques exploit ...
Marques-Silva, Joao; Argelich Romà, Josep; Graça, Ana; Lynce, Inês (Springer Verlag, 2011)Multi-Objective Combinatorial Optimization (MOCO) problems find a wide range of practical application problems, some of which involving Boolean variables and constraints. This paper develops and evaluates algorithms for ...
Sabharwal, Ashish; Ansótegui Gil, Carlos José; Gomes, Carla; Hart, Justin W.; Selman, Bart (Springer Verlag, 2006)Quantified Boolean Formulas (QBFs) present the next big challenge for automated propositional reasoning. Not surprisingly, most of the present day QBF solvers are extensions of successful propositional satisfiability ...