Abstract
Decisions diagrams such as Binary Decision Diagrams (BDDs), Multi-valued Decision Diagrams (MDDs) and Negation Normal Forms (NNFs) provide succinct ways of representing Boolean and other finite functions. Hence they provide a powerful tool for modelling complex constraints in discrete satisfaction and optimization problems. Generic propagators for these global constraints exist, but they are complex and hard to implement. An alternative approach to making use of them for solving is to encode them to CNF, using SAT style solving technology to implement them efficiently. This may also have advantages since it is naturally incremental and exposes intermediate literals which may well be useful as search decisions for solving the problem.
In this paper we explore different ways that we can map these constraints to CNF, and the different properties these mappings maintain. Surprisingly the most used encoding of BDDs does not maintain domain consistency in arbitrary BDDs. We also consider the strength of propagation with respect to the intermediate literals. We give experiments which compare the performance of the different encodings.
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
Similar content being viewed by others
Notes
- 1.
A longer version of this paper including proofs of all Theorems can be found at http://people.eng.unimelb.edu.au/pstuckey/mddenc.pdf.
- 2.
Notice, however, that every result in this paper holds for non-reduced MDDs without long edges, and with some modifications of the rules the results also extend to non-reduced MDDs with long edges.
- 3.
Benchmarks are available from http://people.eng.unimelb.edu.au/pstuckey/mddenc.tar.gz.
References
Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Stuckey, P.J.: To encode or to propagate? The best choice for each constraint in SAT. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 97–106. Springer, Heidelberg (2013)
Abío, I., Stuckey, P.J.: Encoding linear constraints into SAT. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 75–91. Springer, Heidelberg (2014)
Ansótegui, C., Manyà, F.: Mapping problems with finite-domain variables into problems with boolean variables. In: SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, Vancouver, BC, Canada, Online Proceedings, 10–13 May 2004
Bacchus, F.: GAC via unit propagation. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 133–147. Springer, Heidelberg (2007)
Bessiere, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit complexity and decompositions of global constraints. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, Pasadena, California, USA, 11–17 July 2009, pp. 412–418 (2009)
Bordeaux, L., Marques-Silva, J.: Knowledge compilation with empowerment. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 612–624. Springer, Heidelberg (2012)
Chen, J.: A new SAT encoding of the at-most-one constraint. In: Proceedings of the Tenth International Workshop of Constraint Modelling and Reformulation (2010)
Cheng, K.C.K., Yap, R.H.C.: Maintaining generalized arc consistency on Ad Hoc r-Ary constraints. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 509–523. Springer, Heidelberg (2008)
Chu, G.: Chuffed. https://github.com/geoffchu/chuffed
Chu, G.G.: Improving combinatorial optimization. Ph.D. thesis, The University of Melbourne (2011)
Darwiche, A.: On the tractable counting of theory models and its application to truth maintenance and belief revision. J. Appl. Non-class. Logics 11(1–2), 11–34 (2001)
Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: IJCAI, pp. 819–826 (2011)
Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. JSAT 2(1–4), 1–26 (2006)
Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.: Solving non-boolean satisfiability problems with stochastic local search: a comparison of encodings. J. Autom. Reason. 35(1–3), 143–179 (2005)
Gange, G., Stuckey, P.J., Van Hentenryck, P.: Explaining propagators for edge-valued decision diagrams. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 340–355. Springer, Heidelberg (2013)
Gange, G., Stuckey, P.J., Lagoon, V.: Fast set bounds propagation using a BDD-SAT hybrid. J. Artif. Intell. Res. (JAIR) 38, 307–338 (2010)
Gange, G., Stuckey, P.J., Szymanek, R.: MDD propagators with explanation. Constraints 16(4), 407–429 (2011)
Gent, I.P.: Arc consistency in SAT. In: Proceedings of the 15th Eureopean Conference on Artificial Intelligence, ECAI 2002, Lyon, France, pp. 121–125, July 2002
Gwynne, M., Kullmann, O.: A framework for good SAT translations, with applications to CNF representations of XOR constraints. CoRR abs/1406.7398 (2014). http://arxiv.org/abs/1406.7398
Jung, J.C., Barahona, P., Katsirelos, G., Walsh, T.: Two encodings of DNNF theories. In: ECAI 2008 Workshop on Inference Methods Based on Graphical Structures of Knowledge (2008)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract davis-putnam-logemann-loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)
Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986)
Quimper, C.-G., Walsh, T.: Decomposing global grammar constraints. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 590–604. Springer, Heidelberg (2007)
Srinivasan, A., Ham, T., Malik, S., Brayton, R.: Algorithms for discrete function manipulation. In: 1990 IEEE International Conference on Computer-Aided Design, ICCAD-90, Digest of Technical Papers, pp. 92–95 (1990)
Tseytin, G.: On the complexity of derivation in propositional calculus. Stud. Constr. Math. Math. Logic Part 2, 115–125 (1968)
del Val, A.: Tractable databases: how to make propositional unit resolution complete through compilation. In: Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR 1994), Bonn, Germany, 24–27 May 1994, pp. 551–561 (1994)
Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 441–456. Springer, Heidelberg (2000)
Acknowledgement
NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Abío, I., Gange, G., Mayer-Eichberger, V., Stuckey, P.J. (2016). On CNF Encodings of Decision Diagrams. In: Quimper, CG. (eds) Integration of AI and OR Techniques in Constraint Programming. CPAIOR 2016. Lecture Notes in Computer Science(), vol 9676. Springer, Cham. https://doi.org/10.1007/978-3-319-33954-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-33954-2_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-33953-5
Online ISBN: 978-3-319-33954-2
eBook Packages: Computer ScienceComputer Science (R0)