Show simple item record

dc.contributor.authorMorgado, Antonio
dc.contributor.authorHeras, Federico
dc.contributor.authorLiffiton, Mark
dc.contributor.authorPlanes Cid, Jordi
dc.contributor.authorMarques-Silva, Joao
dc.date.accessioned2016-06-15T11:40:18Z
dc.date.issued2013
dc.identifier.issn1383-7133
dc.identifier.urihttp://hdl.handle.net/10459.1/57209
dc.description.abstractMaximum Satisfiability (MaxSAT) is an optimization version of SAT, and many real world applications can be naturally encoded as such. Solving MaxSAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in developing efficient algorithms and several families of algorithms have been proposed. This paper overviews recent approaches to handle MaxSAT and presents a survey of MaxSAT algorithms based on iteratively calling a SAT solver which are particularly effective to solve problems arising in industrial settings. First, classic algorithms based on iteratively calling a SAT solver and updating a bound are overviewed. Such algorithms are referred to as iterative MaxSAT algorithms. Then, more sophisticated algorithms that additionally take advantage of unsatisfiable cores are described, which are referred to as core-guided MaxSAT algorithms. Core-guided MaxSAT algorithms use the information provided by unsatisfiable cores to relax clauses on demand and to create simpler constraints. Finally, a comprehensive empirical study on non-random benchmarks is conducted, including not only the surveyed algorithms, but also other state-of-the-art MaxSAT solvers. The results indicate that (i) core-guided MaxSAT algorithms in general abort in less instances than classic solvers based on iteratively calling a SAT solver and that (ii) core-guided MaxSAT algorithms are fairly competitive compared to other approaches.ca_ES
dc.language.isoengca_ES
dc.publisherSpringer Verlagca_ES
dc.relation.isformatofReproducció del document publicat a https://doi.org/10.1007/s10601-013-9146-2ca_ES
dc.relation.ispartofConstraints, 2013, vol. 18, núm. 4, p. 478-534ca_ES
dc.rights(c) Springer Science+Business Media New York, 2013ca_ES
dc.subjectMaxSATca_ES
dc.subjectMaxSMTca_ES
dc.subjectBoolean optimizationca_ES
dc.subjectOptimization problemsca_ES
dc.titleIterative and core-guided MaxSAT solving: A survey and assessmentca_ES
dc.typearticleca_ES
dc.identifier.idgrec019818
dc.type.versionpublishedVersionca_ES
dc.rights.accessRightsinfo:eu-repo/semantics/restrictedAccessca_ES
dc.identifier.doihttps://doi.org/10.1007/s10601-013-9146-2
dc.date.embargoEndDate2025-01-01


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record