C. M. Li, F. Manya, J. Planes. New Inference Rules for Max-sat

Natural Sciences / Computer Science / Analysis of algorithms

Submitted on: Aug 20, 2012, 20:25:34

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 Library of Congress (USA) reference page : http://lccn.loc.gov/cn2013300046.

To read the article posted on Intellectual Archive web site please click the link below.


© Shiny World Corp., 2011-2023. All rights reserved. To reach us please send an e-mail to support@IntellectualArchive.com