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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Codish, M., Miller, A., Prosser, P., Stuckey, P.J.: Breaking symmetries in graph representation. In: Rossi, F. (ed.) IJCAI. IJCAI/AAAI (2013)
EĆ©n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.Ā 3569, pp. 61ā75. Springer, Heidelberg (2005)
Garnick, D.K., Kwong, Y.H.H., Lazebnik, F.: Extremal graphs without three-cycles or four-cycles. Journal of Graph TheoryĀ 17(5), 633ā645 (1993)
Heule, M.J.H., JƤrvisalo, M., Biere, A.: Efficient CNF simplification based on binary implication graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.Ā 6695, pp. 201ā215. Springer, Heidelberg (2011)
Heule, M., van Maaren, H.: Aligning CNF- and equivalence-reasoning. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.Ā 3542, pp. 145ā156. Springer, Heidelberg (2005)
Janota, M.: SAT Solving in Interactive Configuration. PhD thesis, University College Dublin (November 2010)
Kilby, P., Slaney, J.K., ThiĆ©baux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: Veloso, M.M., Kambhampati, S. (eds.) AAAI, pp. 1368ā1373. AAAI Press / The MIT Press (2005)
Kirkpatrick, S., Toulouse, G.: Configuration space analysis of traveling salesman problems. J. Phys. (France)Ā 46, 1277ā1292 (1985)
Li, C.-M.: Equivalent literal propagation in the DLL procedure. Discrete Applied MathematicsĀ 130(2), 251ā276 (2003)
Manolios, P., Papavasileiou, V.: Pseudo-boolean solving by incremental translation to SAT. In: Bjesse, P., SlobodovĆ”, A. (eds.) FMCAD, pp. 41ā45. FMCAD Inc. (2011)
Manthey, N.: Coprocessor 2.0 - a flexible CNF simplifier - (tool presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.Ā 7317, pp. 436ā441. Springer, Heidelberg (2012)
Marques-Silva, J., Janota, M., Lynce, I.: On computing backbones of propositional theories. In: Coelho, H., Studer, R., Wooldridge, M. (eds.) ECAI. Frontiers in Artificial Intelligence and Applications, vol.Ā 215, pp. 15ā20. IOS Press (2010), Extended version: http://sat.inesc-id.pt/~mikolas/bb-aicom-preprint.pdf
Metodi, A., Codish, M.: Compiling finite domain constraints to SAT with BEE. TPLPĀ 12(4-5), 465ā483 (2012)
Metodi, A., Codish, M., Lagoon, V., Stuckey, P.J.: Boolean equi-propagation for optimized SAT encoding. In: Lee, J. (ed.) CP 2011. LNCS, vol.Ā 6876, pp. 621ā636. Springer, Heidelberg (2011)
Metodi, A., Codish, M., Stuckey, P.J.: Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems. J. Artif. Intell. Res. (JAIR)Ā 46, 303ā341 (2013)
Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity for characteristic phase transitions. NatureĀ 400, 133ā137 (1998)
Schneider, J.J.: Searching for backbones ā an efficient parallel algorithm for the traveling salesman problem. Comput. Phys. Commun. (1996)
Sheeran, M., StĆ„lmarck, G.: A tutorial on stĆ„lmarckās proof procedure for propositional logic. Formal Methods in System DesignĀ 16(1), 23ā58 (2000)
StƄlmark, G.: A system for determining propositional logic theorem by applying values and rules to triplets that are generated from a formula. US Patent 5,276,897; Canadian Patent 2,018,828; European Patent 0403 545; Swedish Patent 467 076 (1994)
Zhang, W.: Phase transitions and backbones of the asymmetric traveling salesman problem. J. Artif. Intell. Res. (JAIR)Ā 21, 471ā497 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
Ā© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Codish, M., Fekete, Y., Metodi, A. (2013). Backbones for Equality. In: Bertacco, V., Legay, A. (eds) Hardware and Software: Verification and Testing. HVC 2013. Lecture Notes in Computer Science, vol 8244. Springer, Cham. https://doi.org/10.1007/978-3-319-03077-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-03077-7_1
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03076-0
Online ISBN: 978-3-319-03077-7
eBook Packages: Computer ScienceComputer Science (R0)