Document Open Access Logo

Changing Partitions in Rectangle Decision Lists

Author Stefan Mengel

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.17.pdf
  • Filesize: 0.69 MB
  • 20 pages

Document Identifiers

Author Details

Stefan Mengel
  • Univ. Artois, CNRS, Centre de Recherche en Informatique de Lens (CRIL), Lens, France

Funding

  • Mengel, Stefan: This work has been partly supported by the PING/ACK project of the French National Agency for Research (ANR-18-CE40-0011).

Acknowledgements

The author would like to thank the reviewers for their generous and very detailed comments that greatly improved the presentation of this paper.

Cite AsGet BibTex

Stefan Mengel. Changing Partitions in Rectangle Decision Lists. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.17

Abstract

Rectangle decision lists are a form of decision lists that were recently shown to have applications in the proof complexity of certain OBDD-based QBF-solvers. We consider a version of rectangle decision lists with changing partitions, which corresponds to QBF-solvers that may change the variable order of the OBDDs they produce. We show that even allowing one single partition change generally leads to exponentially more succinct decision lists. More generally, we show that there is a succinctness hierarchy: for every k ∈ ℕ, when going from k partition changes to k+1, there are functions that can be represented exponentially more succinctly. As an application, we show a similar hierarchy for OBDD-based QBF-solvers.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Proof complexity
Keywords
  • rectangle decision lists
  • QBF proof complexity
  • OBDD

Metrics

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

References

  1. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods Syst. Des., 41(1):45-65, 2012. URL: https://doi.org/10.1007/s10703-012-0152-6.
  2. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Ján Pich. Frege systems for quantified boolean logic. J. ACM, 67(2):9:1-9:36, 2020. URL: https://doi.org/10.1145/3381881.
  3. Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for hardness in QBF proof systems. ACM Trans. Comput. Theory, 12(2):10:1-10:27, 2020. URL: https://doi.org/10.1145/3378665.
  4. Béla Bollobás. The isoperimetric number of random regular graphs. Eur. J. Comb., 9(3):241-244, 1988. URL: https://doi.org/10.1016/S0195-6698(88)80014-3.
  5. 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.
  6. Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering rule makes OBDD proof systems stronger. In Rocco A. Servedio, editor, 33rd Computational Complexity Conference, CCC 2018, June 22-24, 2018, San Diego, CA, USA, volume 102 of LIPIcs, pages 16:1-16:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  7. 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, March 13-16, 2019, Berlin, Germany, volume 126 of LIPIcs, pages 18:1-18:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.STACS.2019.18.
  8. Arkadev Chattopadhyay, Meena Mahajan, Nikhil S. Mande, and Nitin Saurabh. Lower bounds for linear decision lists. Chic. J. Theor. Comput. Sci., 2020, 2020. URL: http://cjtcs.cs.uchicago.edu/articles/2020/1/contents.html.
  9. Reinhard Diestel. Graph Theory, 5th Edition, volume 173 of Graduate texts in mathematics. Springer, 2016. Google Scholar
  10. Pavol Duris, Juraj Hromkovic, Stasys Jukna, Martin Sauerhoff, and Georg Schnitger. On multi-partition communication complexity. Inf. Comput., 194(1):49-75, 2004. URL: https://doi.org/10.1016/j.ic.2004.05.002.
  11. Andrea Ferrara, Guoqiang Pan, and Moshe Y. Vardi. Treewidth in verification: Local vs. global. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, volume 3835 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005. URL: https://doi.org/10.1007/11591191_34.
  12. Mika Göös, Pritish Kamath, Toniann Pitassi, and Thomas Watson. Query-to-communication lifting for P^NP. Comput. Complex., 28(1):113-144, 2019. URL: https://doi.org/10.1007/s00037-018-0175-5.
  13. Thomas P. Hayes. Separating the k-party communication complexity hierarchy: an application of the zarankiewicz problem. Discret. Math. Theor. Comput. Sci., 13(4):15-22, 2011. URL: http://dmtcs.episciences.org/546.
  14. Shlomo Hoory, Nathan Linial, and Avi Wigderson. Expander graphs and their applications. Bulletin of the American Mathematical Society, 43(4):439-561, 2006. Google Scholar
  15. Russell Impagliazzo and Ryan Williams. Communication complexity with synchronized clocks. In Proceedings of the 25th Annual IEEE Conference on Computational Complexity, CCC 2010, Cambridge, Massachusetts, USA, June 9-12, 2010, pages 259-269. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/CCC.2010.32.
  16. Svante Janson, Tomasz Luczak, and Andrzej Rucinski. Random graphs. Wiley-Interscience series in discrete mathematics and optimization. Wiley, 2000. URL: https://doi.org/10.1002/9781118032718.
  17. Stasys Jukna. Boolean Function Complexity - Advances and Frontiers, volume 27 of Algorithms and combinatorics. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-24508-4.
  18. Eyal Kushilevitz and Noam Nisan. Communication complexity. Cambridge University Press, 1997. Google Scholar
  19. Stefan Mengel and Friedrich Slivovsky. Proof complexity of symbolic QBF reasoning. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 399-416. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_28.
  20. Guoqiang Pan and Moshe Y. Vardi. Symbolic decision procedures for QBF. 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 453-467. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30201-8_34.
  21. Periklis A. Papakonstantinou, Dominik Scheder, and Hao Song. Overlays and limited memory communication. In IEEE 29th Conference on Computational Complexity, CCC 2014, Vancouver, BC, Canada, June 11-13, 2014, pages 298-308. IEEE Computer Society, 2014. URL: https://doi.org/10.1109/CCC.2014.37.
  22. Ronald L. Rivest. Learning decision lists. Mach. Learn., 2(3):229-246, 1987. URL: https://doi.org/10.1007/BF00058680.
  23. Fabio Somenzi. CUDD: CU decision diagram package-release 2.4. 0. University of Colorado at Boulder, 2009. Google Scholar
  24. György Turán and Farrokh Vatan. Linear decision lists and partitioning algorithms. In Foundations of Computational Mathematics: Selected Papers of a Conference Held at Rio de Janeiro, January 1997, page 414. Springer Science & Business Media, 2012. Google Scholar
  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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact