Document Open Access Logo

CNF Encodings of Binary Constraint Trees

Authors Ruiwei Wang, Roland H. C. Yap

PDF
Thumbnail PDF

File

LIPIcs.CP.2022.40.pdf
  • Filesize: 0.89 MB
  • 19 pages

Document Identifiers

Author Details

Ruiwei Wang
  • School of Computing, National University of Singapore, Singapore
Roland H. C. Yap
  • School of Computing, National University of Singapore, Singapore

Funding

This work was supported in part by the National Research Foundation Singapore under its AI Singapore Programme [AISG-RP-2018-005] and grant T1 251RES2024.

Cite As Get BibTex

Ruiwei Wang and Roland H. C. Yap. CNF Encodings of Binary Constraint Trees. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CP.2022.40

Abstract

Ordered Multi-valued Decision Diagrams (MDDs) have been shown to be useful to represent finite domain functions/relations. For example, various constraints can be modelled with MDD constraints. Recently, a new representation called Binary Constraint Tree (BCT), which is a (special) tree structure binary Constraint Satisfaction Problem, has been proposed to encode MDDs and shown to outperform existing MDD constraint propagators in Constraint Programming solvers. BCT is a compact representation, and it can be exponentially smaller than MDD for representing some constraints. Here, we also show that BCT is compact for representing non-deterministic finite state automaton (NFA) constraints. In this paper, we investigate how to encode BCT into CNF form, making it suitable for SAT solvers. We present and investigate five BCT CNF encodings. We compare the propagation strength of the BCT CNF encodings and experimentally evaluate the encodings on a range of existing benchmarks. We also compare with seven existing CNF encodings of MDD constraints. Experimental results show that the CNF encodings of BCT constraints can outperform those of MDD constraints on various benchmarks.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Artificial intelligence
  • Software and its engineering → Constraint and logic languages
Keywords
  • BCT
  • CNF
  • MDD
  • NFA / MDD constraint
  • propagation strength

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Ignasi Abío, Graeme Gange, Valentin Mayer-Eichberger, and Peter J Stuckey. On CNF encodings of decision diagrams. In International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pages 1-17. Springer, 2016. Google Scholar
  2. Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Valentin Mayer-Eichberger. A new look at BDDs for pseudo-boolean constraints. Journal of Artificial Intelligence Research, 45:443-480, 2012. Google Scholar
  3. Ignasi Abío and Peter J Stuckey. Encoding linear constraints into SAT. In International Conference on Principles and Practice of Constraint Programming, pages 75-91. Springer, 2014. Google Scholar
  4. Jérôme Amilhastre, Hélene Fargier, Alexandre Niveau, and Cédric Pralet. Compiling CSPs: A complexity map of (non-deterministic) multivalued decision diagrams. International Journal on Artificial Intelligence Tools, 23(04):1460015, 2014. Google Scholar
  5. Miquel Bofill, Jordi Coll, Josep Suy, and Mateu Villaret. Compact MDDs for pseudo-boolean constraints with at-most-one relations in resource-constrained scheduling problems. In International Joint Conference on Artificial Intelligence, pages 555-562, 2017. Google Scholar
  6. Lucas Bordeaux and Joao Marques-Silva. Knowledge compilation with empowerment. In International Conference on Current Trends in Theory and Practice of Computer Science, pages 612-624. Springer, 2012. Google Scholar
  7. Frédéric Boussemart, Fred Hemery, Christophe Lecoutre, and Lakhdar Sais. Boosting systematic search by weighting constraints. In European Conference on Artificial Intelligence, 2004. Google Scholar
  8. Sebastian Brand, Nina Narodytska, Claude-Guy Quimper, Peter Stuckey, and Toby Walsh. Encodings of the Sequence constraint. In International conference on principles and practice of constraint programming, pages 210-224. Springer, 2007. Google Scholar
  9. Kenil C.K. Cheng, Wei Xia, and Roland H.C. Yap. Space-time tradeoffs for the regular constraint. In International Conference on Principles and Practice of Constraint Programming, pages 223-237. Springer, 2012. Google Scholar
  10. Kenil C.K. Cheng and Roland H. C. Yap. An MDD-based generalized arc consistency algorithm for positive and negative table constraints and some global constraints. Constraints, 15(2):265-304, 2010. Google Scholar
  11. Kenil C.K. Cheng and Roland H.C. Yap. Applying ad-hoc global constraints with the case constraint to still-life. Constraints, 11(2-3):91-114, 2006. Google Scholar
  12. Kenil C.K. Cheng and Roland H.C. Yap. Maintaining generalized arc consistency on ad-hoc n-ary boolean constraints. In 17th European Conference on Artificial Intelligence, pages 78-82, 2006. Google Scholar
  13. Rina Dechter and Judea Pearl. Tree clustering for constraint networks. Artificial Intelligence, 38(3):353-366, 1989. Google Scholar
  14. Alvaro Del Val. Tractable databases: How to make propositional unit resolution complete through compilation. In International Conference on Principles of Knowledge Representation and Reasoning, pages 551-561. Elsevier, 1994. Google Scholar
  15. Jordan Demeulenaere, Renaud Hartert, Christophe Lecoutre, Guillaume Perez, Laurent Perron, Jean-Charles Régin, and Pierre Schaus. Compact-Table: efficiently filtering table constraints with reversible sparse bit-sets. In International Conference on Principles and Practice of Constraint Programming, pages 207-223, 2016. Google Scholar
  16. Elizabeth D Dolan and Jorge J Moré. Benchmarking optimization software with performance profiles. Mathematical programming, 91(2):201-213, 2002. Google Scholar
  17. Armin Biere Katalin Fazekas Mathias Fleury and Maximilian Heisinger. CaDiCaL, KISSAT, PARACOOBA, PLINGELING and TREENGELING entering the SAT competition 2020. SAT COMPETITION, 2020:50, 2020. Google Scholar
  18. Graeme Gange, Peter J Stuckey, and Radoslaw Szymanek. MDD propagators with explanation. Constraints, 16(4):407, 2011. Google Scholar
  19. Ian P Gent. Arc consistency in SAT. In European Conference on Artificial Intelligence, pages 121-125, 2002. Google Scholar
  20. Ian P Gent and Peter Nightingale. A new encoding of AllDifferent into SAT. In International Workshop on Modelling and Reformulating Constraint Satisfaction, pages 95-110, 2004. Google Scholar
  21. Rebecca Gentzel, Laurent Michel, and Willem Jan van Hoeve. Haddock: A language and architecture for decision diagram compilation. In nternational Conference on Principles and Practice of Constraint Programming, pages 531-547. Springer, 2020. Google Scholar
  22. Willem-Jan van Hoeve, Gilles Pesant, Louis-Martin Rousseau, and Ashish Sabharwal. Revisiting the sequence constraint. In International conference on principles and practice of constraint programming, pages 620-634. Springer, 2006. Google Scholar
  23. Kazuo Iwama and Shuichi Miyazaki. SAT-variable complexity of hard combinatorial problems. In IFIP World Computer Congress, 1994. Google Scholar
  24. Simon Kasif. On the parallel complexity of discrete relaxation in constraint satisfaction networks. Artificial Intelligence, 45(3):275-286, 1990. Google Scholar
  25. Petr Kucera and Petr Savický. Propagation complete encodings of smooth DNNF theories. CoRR, abs/1909.06673, 2019. URL: http://arxiv.org/abs/1909.06673.
  26. Petr Kučera and Petr Savickỳ. Bounds on the size of PC and URC formulas. Journal of Artificial Intelligence Research, 69:1395-1420, 2020. Google Scholar
  27. Mikael Zayenz Lagerkvist. Techniques for efficient constraint propagation. PhD thesis, KTH, 2008. Google Scholar
  28. Christophe Lecoutre. STR2: optimized simple tabular reduction for table constraints. Constraints, 16(4):341-371, 2011. Google Scholar
  29. Sylvain Merchez, Christophe Lecoutre, and Frédéric Boussemart. Abscon: A prototype to solve CSPs with abstraction. In International Conference on Principles and Practice of Constraint Programming, pages 730-744. Springer, 2001. Google Scholar
  30. Laurent Michel and Pascal Van Hentenryck. Activity-based search for black-box constraint programming solvers. In International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming, 2012. Google Scholar
  31. Guillaume Perez and Jean-Charles Régin. Improving GAC-4 for table and MDD constraints. In International Conference on Principles and Practice of Constraint Programming, pages 606-621. Springer, 2014. Google Scholar
  32. Gilles Pesant. A regular language membership constraint for finite sequences of variables. In International conference on principles and practice of constraint programming, pages 482-495. Springer, 2004. Google Scholar
  33. Claude-Guy Quimper and Toby Walsh. Global grammar constraints. In International conference on principles and practice of constraint programming, pages 751-755, 2006. Google Scholar
  34. Philippe Refalo. Impact-based search strategies for constraint programming. In International Conference on Principles and Practice of Constraint Programming, 2004. Google Scholar
  35. Jean-Charles Régin. A filtering algorithm for constraints of difference in CSPs. In National Conference on Artificial Intelligence, 1994. Google Scholar
  36. Jean-Charles Régin. Generalized arc consistency for global cardinality constraint. National Conference on Artificial Intelligence, pages 209-215, 1996. Google Scholar
  37. Francesca Rossi, Charles J. Petrie, and Vasant Dhar. On the equivalence of constraint satisfaction problems. In European Conference on Artificial Intelligence, pages 550-556, 1990. Google Scholar
  38. Barbara M Smith and Stuart A Grant. Trying harder to fail first. In European Conference on Artificial Intelligence, 1998. Google Scholar
  39. Arvind Srinivasan, Timothy Ham, Sharad Malik, and Robert K Brayton. Algorithms for discrete function manipulation. In IEEE/ACM International Conference on Computer-Aided Design, pages 92-95, 1990. Google Scholar
  40. Kostas Stergiou and Toby Walsh. Encodings of non-binary constraint satisfaction problems. In AAAI Conference on Artificial Intelligence, pages 163-168, 1999. Google Scholar
  41. Allen Van Gelder. Another look at graph coloring via propositional satisfiability. Discrete Applied Mathematics, 156(2):230-243, 2008. Google Scholar
  42. Hélene Verhaeghe, Christophe Lecoutre, and Pierre Schaus. Compact-MDD: Efficiently filtering (s)MDD constraints with reversible sparse bit-sets. In International Joint Conference on Artificial Intelligence, pages 1383-1389, 2018. Google Scholar
  43. Hélène Verhaeghe, Christophe Lecoutre, and Pierre Schaus. Extending Compact-Diagram to basic smart multi-valued variable diagrams. In International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 581-598. Springer, 2019. Google Scholar
  44. Toby Walsh. SAT v CSP. In International Conference on Principles and Practice of Constraint Programming, pages 441-456, 2000. Google Scholar
  45. Ruiwei Wang, Wei Xia, Roland H. C. Yap, and Zhanshan Li. Optimizing simple tabular reduction with a bitwise representation. In International Joint Conference on Artificial Intelligence, pages 787-795, 2016. Google Scholar
  46. Ruiwei Wang and Roland H. C. Yap. Arc consistency revisited. In International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 599-615, 2019. Google Scholar
  47. Ruiwei Wang and Roland H. C. Yap. Bipartite encoding: A new binary encoding for solving non-binary csps. In International Joint Conference on Artificial Intelligence, pages 1184-1191, 2020. Google Scholar
  48. Ruiwei Wang and Roland H. C. Yap. Encoding multi-valued decision diagram constraints as binary constraint trees. In AAAI Conference on Artificial Intelligence, 2022. Google Scholar
  49. Wei Xia and Roland H. C. Yap. Optimizing STR algorithms with tuple compression. In International Conference on Principles and Practice of Constraint Programming, pages 724-732, 2013. Google Scholar
  50. Roland H. C. Yap, Wei Xia, and Ruiwei Wang. Generalized arc consistency algorithms for table constraints: A summary of algorithmic ideas. In AAAI Conference on Artificial Intelligence, pages 13590-13597, 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact