Separating Incremental and Non-Incremental Bottom-Up Compilation

Author Alexis de Colnet



PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.7.pdf
  • Filesize: 0.78 MB
  • 20 pages

Document Identifiers

Author Details

Alexis de Colnet
  • Algorithms and Complexity Group, TU Wien, Austria

Cite As Get BibTex

Alexis de Colnet. Separating Incremental and Non-Incremental Bottom-Up Compilation. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.SAT.2023.7

Abstract

The aim of a compiler is, given a function represented in some language, to generate an equivalent representation in a target language L. In bottom-up (BU) compilation of functions given as CNF formulas, constructing the new representation requires compiling several subformulas in L. The compiler starts by compiling the clauses in L and iteratively constructs representations for new subformulas using an "Apply" operator that performs conjunction in L, until all clauses are combined into one representation. In principle, BU compilation can generate representations for any subformulas and conjoin them in any way. But an attractive strategy from a practical point of view is to augment one main representation - which we call the core - by conjoining to it the clauses one at a time. We refer to this strategy as incremental BU compilation. We prove that, for known relevant languages L for BU compilation, there is a class of CNF formulas that admit BU compilations to L that generate only polynomial-size intermediate representations, while their incremental BU compilations all generate an exponential-size core.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
Keywords
  • Knowledge Compilation
  • Bottom-up Compilation
  • DNNF
  • OBDD

Metrics

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

References

  1. Albert Atserias, Phokion G. Kolaitis, and Moshe Y. Vardi. Constraint Propagation as a Proof System. In Mark Wallace, editor, Principles and Practice of Constraint Programming - CP 2004, 10th International Conference, CP 2004, Toronto, Canada, September 27 - October 1, 2004, Proceedings, volume 3258 of Lecture Notes in Computer Science, pages 77-91. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30201-8_9.
  2. Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-692, 1986. Google Scholar
  3. 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. AAAI Press, 2013. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI13/paper/view/6470.
  4. A. Darwiche. SDD: A New Canonical Representation of Propositional Knowledge Bases. In Proc. of IJCAI'11, pages 819-826, 2011. Google Scholar
  5. Adnan Darwiche. Decomposable negation normal form. J. ACM, 48(4):608-647, 2001. URL: https://doi.org/10.1145/502090.502091.
  6. 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.
  7. Alexis de Colnet. A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 312-321. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_22.
  8. Alexis de Colnet and Stefan Mengel. Lower Bounds on Intermediate Results in Bottom-Up Knowledge Compilation. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, pages 5564-5572. AAAI Press, 2022. URL: https://ojs.aaai.org/index.php/AAAI/article/view/20496.
  9. Luke Friedman and Yixin Xu. Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams. In Andrei A. Bulatov and Arseny M. Shur, editors, Computer Science - Theory and Applications - 8th International Computer Science Symposium in Russia, CSR 2013, Ekaterinburg, Russia, June 25-29, 2013. Proceedings, volume 7913 of Lecture Notes in Computer Science, pages 127-138. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38536-0_11.
  10. Jinbo Huang and Adnan Darwiche. Using DPLL for Efficient OBDD Construction. In SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, 2004. URL: http://www.satisfiability.org/SAT04/programme/61.pdf.
  11. Jinbo Huang and Adnan Darwiche. DPLL with a Trace: From SAT to Knowledge Compilation. In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 - August 5, 2005, pages 156-162. Professional Book Center, 2005. URL: http://ijcai.org/Proceedings/05/Papers/0876.pdf.
  12. Dmitry Itsykson, Alexander Knop, Andrei E. Romashchenko, and Dmitry Sokolov. On OBDD-based Algorithms and Proof Systems that Dynamically Change the order of Variables. J. Symb. Log., 85(2):632-670, 2020. URL: https://doi.org/10.1017/jsl.2019.53.
  13. Dmitry Itsykson, Artur Riazanov, and Petr Smirnov. Tight Bounds for Tseitin Formulas. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 6:1-6:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.6.
  14. Jan Krajícek. An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams. J. Symb. Log., 73(1):227-237, 2008. URL: https://doi.org/10.2178/jsl/1208358751.
  15. Pierre Marquis. Compile! In Blai Bonet and Sven Koenig, editors, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA, pages 4112-4118. AAAI Press, 2015. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9596.
  16. Nina Narodytska and Toby Walsh. Constraint and Variable Ordering Heuristics for Compiling Configuration Problems. In Manuela M. Veloso, editor, IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007, pages 149-154, 2007. URL: http://ijcai.org/Proceedings/07/Papers/022.pdf.
  17. Guoqiang Pan and Moshe Y. Vardi. Search vs. Symbolic Techniques in Satisfiability Solving. In SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, 2004. URL: http://www.satisfiability.org/SAT04/programme/62.pdf.
  18. Guoqiang Pan and Moshe Y. Vardi. Symbolic Techniques in Satisfiability Solving. J. Autom. Reason., 35(1-3):25-50, 2005. URL: https://doi.org/10.1007/s10817-005-9009-7.
  19. 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.
  20. Knot Pipatsrisawat and Adnan Darwiche. Top-Down Algorithms for Constructing Structured DNNF: Theoretical and Practical Implications. In Helder Coelho, Rudi Studer, and Michael J. Wooldridge, editors, ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 3-8. IOS Press, 2010. URL: http://www.booksonline.iospress.nl/Content/View.aspx?piid=17704.
  21. Steven D. Prestwich. CNF Encodings. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 75-100. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200985.
  22. Nathan Segerlind. On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs. In Proceedings of the 23rd Annual IEEE Conference on Computational Complexity, CCC 2008, 23-26 June 2008, College Park, Maryland, USA, pages 100-111. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/CCC.2008.34.
  23. Olga Tveretina, Carsten Sinz, and Hans Zantema. Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond. J. Satisf. Boolean Model. Comput., 7(1):35-58, 2010. URL: https://doi.org/10.3233/sat190074.
  24. Romain Wallon and Stefan Mengel. Revisiting Graph Width Measures for CNF-Encodings. J. Artif. Intell. Res., 67:409-436, 2020. URL: https://doi.org/10.1613/jair.1.11750.
  25. Ingo Wegener. Branching Programs and Binary Decision Diagrams. SIAM, 2000. URL: http://ls2-www.cs.uni-dortmund.de/monographs/bdd/.
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