
Backbones for EqualityMichael Codish, Yoav Fekete and Amit Metodi
Proceedings of the Ninth Haifa Verification Conference;
2013
Abstract:This paper generalizes the notion of the backbone of a CNF formula to capture also equations between literals. Each such equation applies to remove a variable from the original formula thus simplifying the formula without changing its satisfiability, or the number of its satisfying assignments. We prove that for a formula with n variables, the generalized backbone is computed with at most n+1 satisfiable calls and exactly one unsatisfiable call to the SAT solver. We illustrate the integration of generalized backbone computation to facilitate the encoding of finite domain constraints to SAT. In this context generalized backbones are computed for small groups of constraints and then propagated to simplify the entire constraint model. A preliminary experimental evaluation is provided.Available: bibtex entry pdf Michael Codish The Department of Computer Science BenGurion University of the Negev PoB 653, BeerSheva, 84105, Israel mcodish@cs.bgu.ac.il
