C. M. Li, F. Manya, J. Planes. New Inference Rules for Max-sat
Submitted on: Aug 20, 2012, 20:25:34
Natural Sciences / Computer Science / Analysis of algorithms
Description: 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 abstract of this article will be published in the August 2012 issue of "Intellectual Archive Bulletin", ISSN 1929-1329.
The Library and Archives Canada reference page: collectionscanada.gc.ca/ourl/res.php?url_ver=Z39.88......
To read the article posted on Intellectual Archive web site please click the link below.