| dc.contributor.author | Li, Chu-Min | |
| dc.contributor.author | Manyà Serres, Felip | |
| dc.contributor.author | Planes Cid, Jordi | |
| dc.date.accessioned | 2016-07-11T09:02:12Z | |
| dc.date.issued | 2007 | |
| dc.identifier.issn | 1076-9757 | |
| dc.identifier.uri | http://hdl.handle.net/10459.1/57413 | |
| dc.description.abstract | Exact 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.sponsorship | Research 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.iso | eng | ca_ES |
| dc.publisher | Association for the Advancement of Artificial Intelligence | ca_ES |
| dc.relation | MIECI/PN2004-2007/TIN2004-07933-C03-03 | ca_ES |
| dc.relation | MIECI/PN2004-2007/TIN2006-15662-C02-02 | ca_ES |
| dc.relation.isformatof | Reproducció del document publicat a https://doi.org/10.1613/jair.2215 | ca_ES |
| dc.relation.ispartof | Journal of Artificial Intelligence Research, 2007, vol. 30, p. 321-359 | ca_ES |
| dc.rights | (c) AI Access Foundation, 2007 | ca_ES |
| dc.title | New Inference Rules for Max-SAT | ca_ES |
| dc.type | article | ca_ES |
| dc.identifier.idgrec | 012470 | |
| dc.type.version | publishedVersion | ca_ES |
| dc.rights.accessRights | info:eu-repo/semantics/restrictedAccess | ca_ES |
| dc.identifier.doi | https://doi.org/10.1613/jair.2215 | |
| dc.date.embargoEndDate | 10000-01-01 | |
