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

There are no files associated with this record.

Title Exploiting Inference Rules to Compute Lower Bounds for MAX-SAT Solving
Author Lin, Han; Su, Kaile
Publication Title IJCAI-07
Editor Manuela M. Veloso
Year Published 2007
Abstract 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 MAX-2-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.
Peer Reviewed Yes
Published Yes
Publisher URI http://www.ijcai-07.org/
Alternative URI http://dli.iiit.ac.in/ijcai/IJCAI-2007/PDF/IJCAI07-376.pdf
Conference name 20th International Joint Conference on Artificial Intelligence
Location India
Date From 2007-01-06
Date To 2008-01-12
URI http://hdl.handle.net/10072/18937
Date Accessioned 2008-03-06
Language en_AU
Faculty Faculty of Science, Environment, Engineering and Technology
Subject Other Artificial Intelligence
Publication Type Conference Publications (Full Written Paper - Refereed)
Publication Type Code e1

Show simple item record

Griffith University copyright notice