Abstract
Nogood learning is a critical component of Boolean satisfiability (SAT) solvers, and increasingly popular in the context of integer programming and constraint programming. We present a generic method to learn valid clauses from exact or approximate binary decision diagrams (BDDs) and resolution in the context of SAT solving. We show that any clause learned from SAT conflict analysis can also be generated using our method, while, in addition, we can generate stronger clauses that cannot be derived from one application of conflict analysis. Importantly, since SAT instances are often too large for an exact BDD representation, we focus on BDD relaxations of polynomial size and show how they can still be used to generated useful clauses. Our experimental results show that when this method is used as a preprocessing step and the generated clauses are appended to the original instance, the size of the search tree for a SAT solver can be significantly reduced.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Achterberg, T.: Conflict analysis in mixed integer programming. Discrete Optimization 4(1), 4–20 (2007)
Andersen, H.R., Hadzic, T., Hooker, J.N., Tiedemann, P.: A constraint store based on multivalued decision diagrams. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 118–132. Springer, Heidelberg (2007)
Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. Journal of Artificial Intelligence Research 40, 353–373 (2011)
Beame, P., Kautz, H., Sabharwal, A.: Understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research 22, 319–351 (2004)
Behle, M.: On threshold BDDs and the optimal variable ordering problem. Journal of Combinatorial Optimization 16, 107–118 (2008)
Bergman, B., Cire, A., van Hoeve, W.-J., Hooker, J.: Optimization bounds from binary decision diagrams. INFORMS Journal on Computing 26(2), 253–268 (2014)
Bergman, D., Cire, A.A., van Hoeve, W.-J., Yunes, T.: BDD-based heuristics for binary optimization. Journal of Heuristics 20(2), 211–234 (2014)
Bergman, D., van Hoeve, W.-J., Hooker, J.N.: Manipulating MDD relaxations for combinatorial optimization. In: Achterberg, T., Beck, J.C. (eds.) CPAIOR 2011. LNCS, vol. 6697, pp. 20–35. Springer, Heidelberg (2011)
Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Transactions on Computers 45(9), 993–1002 (1996)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Cire, A., van Hoeve, W.-J.: Multivalued decision diagrams for sequencing problems. Operations Research 61(6), 1411–1428 (2013)
Downing, N., Feydy, T., Stuckey, P.: Explaining flow-based propagation. In: Beldiceanu, N., Jussien, N., Pinson, É. (eds.) CPAIOR 2012. LNCS, vol. 7298, pp. 146–162. Springer, Heidelberg (2012)
Hadzic, T., Hooker, J., O’Sullivan, B., Tiedemann, P.: Approximate compilation of constraints into multivalued decision diagrams. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 448–462. Springer, Heidelberg (2008)
Hoda, S., van Hoeve, W.-J., Hooker, J.: A systematic approach to MDD-based constraint programming. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 266–280. Springer, Heidelberg (2010)
Katsirelos, G.: Nogood Processing in CSPs. PhD thesis, University of Toronto (2008)
Kell, B., van Hoeve, W.-J.: An MDD approach to multidimensional bin packing. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 128–143. Springer, Heidelberg (2013)
Kilinç-Karzan, F., Nemhauser, G., Savelsbergh, M.: Information-based branching schemes for binary linear mixed integer problems. Mathematical Programming Computation 1(4), 249–293 (2009)
Knuth, D.E.: The Art of Computer Programming, vol. 4, fascicle 1: Bitwise Tricks & Techniques; Binary Decision Diagrams. Addison-Wesley (2009)
Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell System Technical Journal 38(4), 985–999 (1959)
Marques-Silva, J.P., Lynce, I., Malik, S.: CDCL solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T., (eds.), Handbook of Satisfiability, chapter 4, pp. 131–154. IOS Press (2009)
Ohrimenko, O., Stuckey, P., Codish, M.: Propagation via lazy clause generation. Constraints 14, 357–391 (2009)
Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence 175(2), 512–525 (2011)
SAT Challenge 2012. SAT Challenge 2012: Downloads, November 23, 2014. http://baldur.iti.kit.edu/SAT-Challenge-2012/downloads.html
Stuckey, P.: Lazy clause generation: combining the power of SAT and CP (and MIP?) solving. In: Lodi, A., Milano, M., Toth, P. (eds.) CPAIOR 2010. LNCS, vol. 6140, pp. 5–9. Springer, Heidelberg (2010)
Wegener, I.: Branching Programs and Binary Decision Diagrams: Theory and Applications. SIAM Monographs on Discrete Mathematics and Applications. SIAM, Philadelphia (2000)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Kell, B., Sabharwal, A., van Hoeve, WJ. (2015). BDD-Guided Clause Generation. In: Michel, L. (eds) Integration of AI and OR Techniques in Constraint Programming. CPAIOR 2015. Lecture Notes in Computer Science(), vol 9075. Springer, Cham. https://doi.org/10.1007/978-3-319-18008-3_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-18008-3_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-18007-6
Online ISBN: 978-3-319-18008-3
eBook Packages: Computer ScienceComputer Science (R0)