New Inference Rules for Max-SAT

Details New Inference Rules for Max-SAT New Inference Rules for Max-SAT

2011-10-31

arxiv.org/abs/1111.0040v1

Journal Of Artificial Intelligence Research, Volume 30, pages 321-359, 2007

Computer Science

Artificial Intelligence

Scientific paper

10.1613/jair.2215

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, Max-Cut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.

Affiliated with

Also associated with

No associations

Rating

New Inference Rules for Max-SAT does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with New Inference Rules for Max-SAT, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and New Inference Rules for Max-SAT will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-466654