English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/161611
logo share SHARE logo core CORE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Exportar a otros formatos:


Resolution-based lower bounds in MaxSAT

AuthorsLi, Chumin; Manyà, Felip ; Mohamedou, Nouredine O.; Planes, Jordi
KeywordsLower bound
Issue Date2010
CitationConstraints 15: 456- 484 (2010)
AbstractThe lower bound (LB) implemented in branch and bound MaxSAT solvers is decisive for obtaining a competitive solver. In modern solvers like MaxSatz and MiniMaxSat, the LB relies on the cooperation of the underestimation and inference components. Actually, the underestimation component of some solvers guides the application of the inference component when a conflict is reached and certain structures are found. In this paper we analyze algorithmic and logical aspects of the underestimation components that have been implemented in MaxSatz during its evolution. From an algorithmic point of view, we define novel strategies for selecting unit clauses in UP (the underestimation of LB in UP is the number of independent inconsistent subformulas detected using unit propagation), the extension of UP with failed literal detection, and a clever heuristic for guiding the application of MaxSAT resolution when UP augmented with failed literal detection is applied in the presence of cycles structures. From a logical point of view, we prove that the inconsistent subformulas detected by UP are minimally unsatisfiable, but this property does not hold if failed literal detection is added. In the presence of cycle structures in conflicts detected by UP augmented with failed literal detection, we prove that the application of MaxSAT resolution produces smaller inconsistent subformulas and, besides, generates additional clauses that may be used to improve the LB. The conducted empirical investigation indicates that the LB techniques described in this paper lead to better quality LBs. © 2010 Springer Science+Business Media, LLC.
Identifiersdoi: 10.1007/s10601-010-9097-9
issn: 1383-7133
Appears in Collections:(IIIA) Artículos
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,38 kBAdobe PDFThumbnail
Show full item record
Review this work

Related articles:

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.