Document Open Access Logo

On Limits of Symbolic Approach to SAT Solving

Authors Dmitry Itsykson , Sergei Ovcharov

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.19.pdf
  • Filesize: 0.8 MB
  • 22 pages

Document Identifiers

Author Details

Dmitry Itsykson
  • Ben-Gurion University of the Negev, Beer-Sheva, Israel
  • On leave from Steklov Institute of Mathematics at St. Petersburg, Russia
Sergei Ovcharov
  • St. Petersburg State University, Russia

Funding

  • Itsykson, Dmitry: Supported by European Research Council Grant No. 949707.

Cite AsGet BibTex

Dmitry Itsykson and Sergei Ovcharov. On Limits of Symbolic Approach to SAT Solving. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.19

Abstract

We study the symbolic approach to the propositional satisfiability problem proposed by Aguirre and Vardi in 2001 based on OBDDs and symbolic quantifier elimination. We study the theoretical limitations of the most general version of this approach where it is allowed to dynamically change variable order in OBDD. We refer to algorithms based on this approach as OBDD(∧, ∃, reordering) algorithms. We prove the first exponential lower bound of OBDD(∧, ∃, reordering) algorithms on unsatisfiable formulas, and give an example of formulas having short tree-like resolution proofs that are exponentially hard for OBDD(∧, ∃, reordering) algorithms. We also present the first exponential lower bound for natural formulas with clear combinatorial meaning: every OBDD(∧, ∃, reordering) algorithm runs exponentially long on the binary pigeonhole principle BPHP^{n+1}_n.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Symbolic quantifier elimination
  • OBDD
  • lower bounds
  • tree-like resolution
  • proof complexity
  • error-correcting codes
  • binary pigeonhole principle

Metrics

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

References

  1. Alfonso San Miguel Aguirre and Moshe Y. Vardi. Random 3-SAT and BDDs: The plot thickens further. In Principles and Practice of Constraint Programming - CP 2001, 7th International Conference, CP 2001, Paphos, Cyprus, November 26 - December 1, 2001, Proceedings, pages 121-136, 2001. URL: https://doi.org/10.1007/3-540-45578-7_9.
  2. Michael Alekhnovich, Edward A. Hirsch, and Dmitry Itsykson. Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. Journal of Automated Reasoning, 35(1-3):51-72, 2005. URL: https://doi.org/10.1007/s10817-005-9006-x.
  3. Albert Atserias, Phokion G. Kolaitis, and Moshe Y. Vardi. Constraint propagation as a proof system. In Principles and Practice of Constraint Programming - CP 2004, 10th International Conference, CP 2004, Toronto, Canada, September 27 - October 1, 2004, Proceedings, pages 77-91, 2004. URL: https://doi.org/10.1007/978-3-540-30201-8_9.
  4. 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.
  5. Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, and Dmitry Sokolov. Lower bounds on OBDD proofs with several orders. ACM Trans. Comput. Log., 22(4):26:1-26:30, 2021. URL: https://doi.org/10.1145/3468855.
  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. URL: https://doi.org/10.4230/LIPICS.CCC.2018.16.
  7. Wěi Chén and Wenhui Zhang. A direct construction of polynomial-size OBDD proof of pigeon hole problem. Information Processing Letters, 109(10):472-477, 2009. URL: https://doi.org/10.1016/j.ipl.2009.01.006.
  8. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. URL: http://www.jstor.org/stable/2273702.
  9. E. N. Gilbert. A comparison of signalling alphabets. The Bell System Technical Journal, 31(3):504-522, 1952. URL: https://doi.org/10.1002/j.1538-7305.1952.tb01393.x.
  10. Ludmila Glinskih and Dmitry Itsykson. Satisfiable Tseitin formulas are hard for nondeterministic read-once branching programs. In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21-25, 2017 - Aalborg, Denmark, volume 83 of LIPIcs, pages 26:1-26:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.MFCS.2017.26.
  11. Ludmila Glinskih and Dmitry Itsykson. On tseitin formulas, read-once branching programs and treewidth. Theory Comput. Syst., 65(3):613-633, 2021. URL: https://doi.org/10.1007/S00224-020-10007-8.
  12. Venkatesan Guruswami. List decoding from erasures: bounds and code constructions. Institute of Electrical and Electronics Engineers. Transactions on Information Theory, 49(11):2826-2833, 2003. URL: https://doi.org/10.1109/tit.2003.815776.
  13. R. W. Hamming. Error detecting and error correcting codes. The Bell System Technical Journal, 29(2):147-160, 1950. URL: https://doi.org/10.1002/j.1538-7305.1950.tb00463.x.
  14. 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.
  15. Jan Krajícek. An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams. The Journal of Symbolic Logic, 73(1):227-237, 2008. URL: https://doi.org/10.2178/jsl/1208358751.
  16. Eyal Kushilevitz and Noam Nisan. Communication complexity. Cambridge University Press, 1997. Google Scholar
  17. Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, and Vijay Ganesh. Towards a complexity-theoretic understanding of restarts in SAT solvers. 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 233-249. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_17.
  18. Stefan Mengel. Bounds on BDD-based bucket elimination. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 16:1-16:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.16.
  19. Guoqiang Pan and Moshe Y. Vardi. Symbolic techniques in satisfiability solving. Journal of Automated Reasoning, 35(1-3):25-50, 2005. URL: https://doi.org/10.1007/s10817-005-9009-7.
  20. 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.
  21. R. R. Varshamov. The evaluation of signals in codes with correction of errors. Dokl. Akad. Nauk SSSR, 117:739-741, 1957. Google Scholar
  22. Ingo Wegener. Branching Programs and Binary Decision Diagrams. SIAM, 2000. 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 Imprint Privacy Contact