A Characterization of Efficiently Compilable Constraint Languages

Authors Christoph Berkholz , Stefan Mengel , Hermann Wilhelm



PDF
Thumbnail PDF

File

LIPIcs.STACS.2024.11.pdf
  • Filesize: 0.8 MB
  • 19 pages

Document Identifiers

Author Details

Christoph Berkholz
  • Technische Universität Ilmenau, Germany
Stefan Mengel
  • Univ. Artois, CNRS, Centre de Recherche en Informatique de Lens (CRIL), France
Hermann Wilhelm
  • Technische Universität Ilmenau, Germany

Cite AsGet BibTex

Christoph Berkholz, Stefan Mengel, and Hermann Wilhelm. A Characterization of Efficiently Compilable Constraint Languages. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.STACS.2024.11

Abstract

A central task in knowledge compilation is to compile a CNF-SAT instance into a succinct representation format that allows efficient operations such as testing satisfiability, counting, or enumerating all solutions. Useful representation formats studied in this area range from ordered binary decision diagrams (OBDDs) to circuits in decomposable negation normal form (DNNFs). While it is known that there exist CNF formulas that require exponential size representations, the situation is less well studied for other types of constraints than Boolean disjunctive clauses. The constraint satisfaction problem (CSP) is a powerful framework that generalizes CNF-SAT by allowing arbitrary sets of constraints over any finite domain. The main goal of our work is to understand for which type of constraints (also called the constraint language) it is possible to efficiently compute representations of polynomial size. We answer this question completely and prove two tight characterizations of efficiently compilable constraint languages, depending on whether target format is structured. We first identify the combinatorial property of "strong blockwise decomposability" and show that if a constraint language has this property, we can compute DNNF representations of linear size. For all other constraint languages we construct families of CSP-instances that provably require DNNFs of exponential size. For a subclass of "strong uniformly blockwise decomposable" constraint languages we obtain a similar dichotomy for structured DNNFs. In fact, strong (uniform) blockwise decomposability even allows efficient compilation into multi-valued analogs of OBDDs and FBDDs, respectively. Thus, we get complete characterizations for all knowledge compilation classes between O(B)DDs and DNNFs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Theory of computation → Complexity theory and logic
Keywords
  • constraint satisfaction
  • knowledge compilation
  • dichotomy
  • DNNF

Metrics

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

References

  1. Noga Alon, Mrinal Kumar, and Ben Lee Volk. Unbalancing sets and an almost quadratic lower bound for syntactically multilinear arithmetic circuits. Comb., 40(2):149-178, 2020. URL: https://doi.org/10.1007/s00493-019-4009-0.
  2. Antoine Amarilli, Pierre Bourhis, Louis Jachiet, and Stefan Mengel. A circuit-based approach to efficient enumeration. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 111:1-111:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.111.
  3. Antoine Amarilli, Florent Capelli, Mikaël Monet, and Pierre Senellart. Connecting knowledge compilation classes and width parameters. Theory Comput. Syst., 64(5):861-914, 2020. URL: https://doi.org/10.1007/s00224-019-09930-2.
  4. Jérôme Amilhastre, Hélène Fargier, Alexandre Niveau, and Cédric Pralet. Compiling CSPs: A complexity map of (non-deterministic) multivalued decision diagrams. Int. J. Artif. Intell. Tools, 23(4), 2014. URL: https://doi.org/10.1142/S021821301460015X.
  5. Christoph Berkholz, Stefan Mengel, and Hermann Wilhelm. A characterization of efficiently compilable constraint languages. CoRR, abs/2311.10040, 2023. URL: https://doi.org/10.48550/ARXIV.2311.10040.
  6. Christoph Berkholz and Harry Vinall-Smeeth. A dichotomy for succinct representations of homomorphisms. In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany, volume 261 of LIPIcs, pages 113:1-113:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.113.
  7. Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. Expander CNFs have exponential DNNF size. CoRR, abs/1411.1995, 2014. URL: https://arxiv.org/abs/1411.1995.
  8. Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. Knowledge compilation meets communication complexity. In Subbarao Kambhampati, editor, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pages 1008-1014. IJCAI/AAAI Press, 2016. URL: http://www.ijcai.org/Abstract/16/147.
  9. Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986. URL: https://doi.org/10.1109/TC.1986.1676819.
  10. Andrei A. Bulatov. The complexity of the counting constraint satisfaction problem. J. ACM, 60(5):34:1-34:41, 2013. URL: https://doi.org/10.1145/2528400.
  11. Andrei A. Bulatov. A dichotomy theorem for nonuniform CSPs. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 319-330. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.37.
  12. Andrei A. Bulatov, Víctor Dalmau, Martin Grohe, and Dániel Marx. Enumerating homomorphisms. J. Comput. Syst. Sci., 78(2):638-650, 2012. URL: https://doi.org/10.1016/J.JCSS.2011.09.006.
  13. Jin-Yi Cai and Xi Chen. Complexity of counting CSP with complex weights. J. ACM, 64(3):19:1-19:39, 2017. URL: https://doi.org/10.1145/2822891.
  14. Florent Capelli. Understanding the complexity of #SAT using knowledge compilation. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-10. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005121.
  15. Florent Capelli and Stefan Mengel. Tractable QBF by Knowledge Compilation. In Rolf Niedermeier and Christophe Paul, editors, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019), volume 126 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:16, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2019.18.
  16. Clément Carbonnel, Miguel Romero, and Stanislav Zivný. The complexity of general-valued constraint satisfaction problems seen from the other side. SIAM J. Comput., 51(1):19-69, 2022. URL: https://doi.org/10.1137/19M1250121.
  17. Arthur Choi and Adnan Darwiche. Dynamic minimization of sentential decision diagrams. In Marie desJardins and Michael L. Littman, editors, Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, July 14-18, 2013, Bellevue, Washington, USA, pages 187-194. AAAI Press, 2013. URL: https://doi.org/10.1609/aaai.v27i1.8690.
  18. Nadia Creignou. A dichotomy theorem for maximum generalized satisfiability problems. J. Comput. Syst. Sci., 51(3):511-522, 1995. URL: https://doi.org/10.1006/jcss.1995.1087.
  19. Nadia Creignou and Miki Hermann. Complexity of generalized satisfiability counting problems. Inf. Comput., 125(1):1-12, 1996. URL: https://doi.org/10.1006/inco.1996.0016.
  20. Nadia Creignou, Sanjeev Khanna, and Madhu Sudan. Complexity classifications of boolean constraint satisfaction problems. SIAM, 2001. Google Scholar
  21. Nadia Creignou, Frédéric Olive, and Johannes Schmidt. Enumerating all solutions of a boolean CSP by non-decreasing weight. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, volume 6695 of Lecture Notes in Computer Science, pages 120-133. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_11.
  22. Víctor Dalmau and Peter Jonsson. The complexity of counting homomorphisms seen from the other side. Theor. Comput. Sci., 329(1-3):315-323, 2004. URL: https://doi.org/10.1016/j.tcs.2004.08.008.
  23. Adnan Darwiche. Decomposable negation normal form. J. ACM, 48(4):608-647, 2001. URL: https://doi.org/10.1145/502090.502091.
  24. Adnan Darwiche. New advances in compiling CNF into decomposable negation normal form. In Ramón López de Mántaras and Lorenza Saitta, editors, Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI'2004, including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, Spain, August 22-27, 2004, pages 328-332. IOS Press, 2004. Google Scholar
  25. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. J. Artif. Intell. Res., 17:229-264, 2002. URL: https://doi.org/10.1613/jair.989.
  26. Guy Van den Broeck and Dan Suciu. Query processing on probabilistic data: A survey. Found. Trends Databases, 7(3-4):197-341, 2017. URL: https://doi.org/10.1561/1900000052.
  27. Martin E. Dyer and David Richerby. An effective dichotomy for the counting constraint satisfaction problem. SIAM J. Comput., 42(3):1245-1274, 2013. URL: https://doi.org/10.1137/100811258.
  28. Hélène Fargier and Pierre Marquis. On the use of partially ordered decision graphs in knowledge compilation and quantified boolean formulae. In Proceedings, The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16-20, 2006, Boston, Massachusetts, USA, pages 42-47. AAAI Press, 2006. URL: http://www.aaai.org/Library/AAAI/2006/aaai06-007.php.
  29. Martin Grohe. The complexity of homomorphism and constraint satisfaction problems seen from the other side. J. ACM, 54(1), March 2007. URL: https://doi.org/10.1145/1206035.1206036.
  30. Sanjeev Khanna, Madhu Sudan, Luca Trevisan, and David P. Williamson. The approximability of constraint satisfaction problems. SIAM J. Comput., 30(6):1863-1920, 2000. URL: https://doi.org/10.1137/S0097539799349948.
  31. Frédéric Koriche, Jean-Marie Lagniez, Pierre Marquis, and Samuel Thomas. Compiling constraint networks into multivalued decomposable decision graphs. In Qiang Yang and Michael Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 332-338. AAAI Press, 2015. URL: http://ijcai.org/papers15/Abstracts/IJCAI15-053.html.
  32. Eyal Kushilevitz and Noam Nisan. Communication complexity. Cambridge University Press, 1997. Google Scholar
  33. Jean-Marie Lagniez and Pierre Marquis. An improved decision-dnnf compiler. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 667-673. ijcai.org, 2017. URL: https://doi.org/10.24963/ijcai.2017/93.
  34. Robert Mateescu and Rina Dechter. Compiling constraint networks into AND/OR multi-valued decision diagrams (aomdds). In Frédéric Benhamou, editor, Principles and Practice of Constraint Programming - CP 2006, 12th International Conference, CP 2006, Nantes, France, September 25-29, 2006, Proceedings, volume 4204 of Lecture Notes in Computer Science, pages 329-343. Springer, 2006. URL: https://doi.org/10.1007/11889205_25.
  35. Robert Mateescu, Rina Dechter, and Radu Marinescu. AND/OR multi-valued decision diagrams (aomdds) for graphical models. J. Artif. Intell. Res., 33:465-519, 2008. URL: https://doi.org/10.1613/jair.2605.
  36. Christian J. Muise, Sheila A. McIlraith, J. Christopher Beck, and Eric I. Hsu. Dsharp: Fast d-dnnf compilation with sharpSAT. In Leila Kosseim and Diana Inkpen, editors, Advances in Artificial Intelligence - 25th Canadian Conference on Artificial Intelligence, Canadian AI 2012, Toronto, ON, Canada, May 28-30, 2012. Proceedings, volume 7310 of Lecture Notes in Computer Science, pages 356-361. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-30353-1_36.
  37. Dan Olteanu. Factorized databases: A knowledge compilation perspective. In Adnan Darwiche, editor, Beyond NP, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 12, 2016, volume WS-16-05 of AAAI Technical Report. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/WS/AAAIW16/paper/view/12638.
  38. Dan Olteanu and Jakub Závodný. Size bounds for factorised representations of query results. ACM Trans. Database Syst., 40(1):2:1-2:44, 2015. URL: https://doi.org/10.1145/2656335.
  39. Umut Oztok and Adnan Darwiche. A top-down compiler for sentential decision diagrams. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 3141-3148. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/443.
  40. Knot Pipatsrisawat and Adnan Darwiche. New compilation languages based on structured decomposability. In Dieter Fox and Carla P. Gomes, editors, Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008, pages 517-522. AAAI Press, 2008. URL: http://www.aaai.org/Library/AAAI/2008/aaai08-082.php.
  41. Ran Raz, Amir Shpilka, and Amir Yehudayoff. A lower bound for the size of syntactically multilinear arithmetic circuits. SIAM J. Comput., 38(4):1624-1647, 2008. URL: https://doi.org/10.1137/070707932.
  42. Thomas J. Schaefer. The complexity of satisfiability problems. In Richard J. Lipton, Walter A. Burkhard, Walter J. Savitch, Emily P. Friedman, and Alfred V. Aho, editors, Proceedings of the 10th Annual ACM Symposium on Theory of Computing, May 1-3, 1978, San Diego, California, USA, pages 216-226. ACM, 1978. URL: https://doi.org/10.1145/800133.804350.
  43. Johan Thapper and Stanislav Zivný. The complexity of finite-valued csps. J. ACM, 63(4):37:1-37:33, 2016. URL: https://doi.org/10.1145/2974019.
  44. Ingo Wegener. Branching Programs and Binary Decision Diagrams. SIAM, 2000. URL: http://ls2-www.cs.uni-dortmund.de/monographs/bdd/.
  45. Dmitriy Zhuk. A proof of CSP dichotomy conjecture. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 331-342. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.38.
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