Proceedings

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

Han Lin, Kaile Su

Download BibTeX Cite

Proceedings of the Twentieth International Joint Conference on Artificial Intelligence. Pages 2334-2338.

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 new rules, which are not equivalent but $Lambda$-equivalent, are proposed, and we show that $Lambda$-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.

Han Lin, and Kaile Su. 2007. Exploiting Inference Rules to Compute Lower Bounds for MAX-SAT Solving. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, IJCAI-07. IJCAI, 2334–2338. https://ijcai.org/proceedings/2007/376
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards