Show simple item record

dc.contributor.authorLi, Chu-Min
dc.contributor.authorManyà Serres, Felip
dc.contributor.authorPlanes Cid, Jordi
dc.date.accessioned2016-07-11T09:02:12Z
dc.date.issued2007
dc.identifier.issn1076-9757
dc.identifier.urihttp://hdl.handle.net/10459.1/57413
dc.description.abstractExact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving the Max-SAT problem for the simplified formula is not equivalent to solving it for the original formula. In this paper, we define a number of original inference rules that, besides being applied efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution adapted to Max-SAT, are proved in a novel and simple way via an integer programming transformation. With the aim of finding out how powerful the inference rules are in practice, we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules, and performed an experimental investigation. The results provide empirical evidence that MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, MaxCut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.ca_ES
dc.description.sponsorshipResearch partially supported by projects TIN2004-07933-C03-03 and TIN2006-15662-C02- 02 funded by the Ministerio de Educación y Ciencia. The first author was partially supported by National 973 Program of China under Grant No. 2005CB321900. The second author was supported by a grant Ramón y Cajal.ca_ES
dc.language.isoengca_ES
dc.publisherAssociation for the Advancement of Artificial Intelligenceca_ES
dc.relationMIECI/PN2004-2007/TIN2004-07933-C03-03ca_ES
dc.relationMIECI/PN2004-2007/TIN2006-15662-C02-02ca_ES
dc.relation.isformatofReproducció del document publicat a https://doi.org/10.1613/jair.2215ca_ES
dc.relation.ispartofJournal of Artificial Intelligence Research, 2007, vol. 30, p. 321-359ca_ES
dc.rights(c) AI Access Foundation, 2007ca_ES
dc.titleNew Inference Rules for Max-SATca_ES
dc.typearticleca_ES
dc.identifier.idgrec012470
dc.type.versionpublishedVersionca_ES
dc.rights.accessRightsinfo:eu-repo/semantics/restrictedAccessca_ES
dc.identifier.doihttps://doi.org/10.1613/jair.2215
dc.date.embargoEndDate10000-01-01


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record