Show simple item record

dc.contributor.authorLi, Chu-Min
dc.contributor.authorManyà Serres, Felip
dc.contributor.authorPlanes Cid, Jordi
dc.date.accessioned2016-07-13T08:30:14Z
dc.date.issued2005
dc.identifier.issn0302-9743
dc.identifier.urihttp://hdl.handle.net/10459.1/57574
dc.description.abstractOne of the main differences between complete SAT solvers and exact Max-SAT solvers is that the former make an intensive use of unit propagation at each node of the proof tree while the latter, in order to ensure optimality, can only apply unit propagation to a restricted number of nodes. In this paper, we describe a branch and bound MaxSAT solver that applies unit propagation at each node of the proof tree to compute the lower bound instead of applying unit propagation to simplify the formula. The new lower bound captures the lower bound based on inconsistency counts that apply most of the state-of-the-art Max-SAT solvers as well as other improvements, like the start rule, that have been defined to get a lower bound of better quality. Moreover, our solver incorporates the Jeroslow-Wang variable selection heuristic, the pure literal and dominating unit clause rules, and novel preprocessing techniques. The experimental investigation we conducted to compare our solver with the most modern Max-SAT solvers provides experimental evidence that our solver is very competitive.ca_ES
dc.description.sponsorshipResearch partially supported by projects TIN2004-07933-C03-03 and TIC2003-00950 funded by the Ministerio de Educación y Ciencia. The second author is supported by a grant Ramón y Cajal.ca_ES
dc.language.isoengca_ES
dc.publisherSpringer Verlagca_ES
dc.relationMIECI/PN2004-2007/TIN2004-07933-C03-03ca_ES
dc.relationMICYT/PN2000-2003/TIC2003-00950ca_ES
dc.relation.isformatofReproducció del document publicat a https://doi.org/10.1007/11564751_31ca_ES
dc.relation.ispartofLecture Notes in Computer Science, 2005, vol. 3709, p. 403-414ca_ES
dc.rights(c) Springer-Verlag Berlin Heidelberg, 2005ca_ES
dc.titleExploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solversca_ES
dc.typearticleca_ES
dc.identifier.idgrec007814
dc.type.versionpublishedVersionca_ES
dc.rights.accessRightsinfo:eu-repo/semantics/restrictedAccessca_ES
dc.identifier.doihttps://doi.org/10.1007/11564751_31
dc.date.embargoEndDate10000-01-01


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record