Sciweavers

Share
IJCAI
2007

Exploiting Inference Rules to Compute Lower Bounds for MAX-SAT Solving

8 years 8 months ago
Exploiting Inference Rules to Compute Lower Bounds for MAX-SAT Solving
In this paper we present a general logical framework for (weighted) MAX-SAT problem, and study properties of inference rules for branch and bound MAX-SAT solver. Several rules, which are not equivalent but Λ-equivalent, are proposed, and we show that Λ-equivalent rules are also sound. As an example, we show how to exploit inference rules to achieve a new lower bound function for a MAX2-SAT solver. Our new function is admissible and consistently better than the well-known lower bound function. Based on the study of inference rules, we implement an efficient solver and the experimental results demonstrate that our solver outperforms the most efficient solver that has been implemented very recently [Heras and Larrosa, 2006], especially for large instances.
Han Lin, Kaile Su
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2007
Where IJCAI
Authors Han Lin, Kaile Su
Comments (0)
books