Document Open Access Logo

SAT Backdoors: Depth Beats Size

Authors Jan Dreier , Sebastian Ordyniak , Stefan Szeider

PDF
Thumbnail PDF

File

LIPIcs.ESA.2022.46.pdf
  • Filesize: 0.94 MB
  • 18 pages

Document Identifiers

Author Details

Jan Dreier
  • Algorithms and Complexity Group, TU Wien, Austria
Sebastian Ordyniak
  • Algorithms and Complexity Group, University of Leeds, UK
Stefan Szeider
  • Algorithms and Complexity Group, TU Wien, Austria

Funding

  • Ordyniak, Sebastian: Supported by the Engineering and Physical Sciences Research Council (EPSRC, project EP/V00252X/1).
  • Szeider, Stefan: supported by the Austrian Science Fund (FWF, project P32441) and the Vienna Science and Technology Fund (WWTF, project ICT19-065).

Cite AsGet BibTex

Jan Dreier, Sebastian Ordyniak, and Stefan Szeider. SAT Backdoors: Depth Beats Size. In 30th Annual European Symposium on Algorithms (ESA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 244, pp. 46:1-46:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ESA.2022.46

Abstract

For several decades, much effort has been put into identifying classes of CNF formulas whose satisfiability can be decided in polynomial time. Classic results are the linear-time tractability of Horn formulas (Aspvall, Plass, and Tarjan, 1979) and Krom (i.e., 2CNF) formulas (Dowling and Gallier, 1984). Backdoors, introduced by Williams, Gomes and Selman (2003), gradually extend such a tractable class to all formulas of bounded distance to the class. Backdoor size provides a natural but rather crude distance measure between a formula and a tractable class. Backdoor depth, introduced by Mählmann, Siebertz, and Vigny (2021), is a more refined distance measure, which admits the utilization of different backdoor variables in parallel. Bounded backdoor size implies bounded backdoor depth, but there are formulas of constant backdoor depth and arbitrarily large backdoor size. We propose FPT approximation algorithms to compute backdoor depth into the classes Horn and Krom. This leads to a linear-time algorithm for deciding the satisfiability of formulas of bounded backdoor depth into these classes. We base our FPT approximation algorithm on a sophisticated notion of obstructions, extending Mählmann et al.’s obstruction trees in various ways, including the addition of separator obstructions. We develop the algorithm through a new game-theoretic framework that simplifies the reasoning about backdoors. Finally, we show that bounded backdoor depth captures tractable classes of CNF formulas not captured by any known method.

Subject Classification

ACM Subject Classification
  • Theory of computation → Fixed parameter tractability
Keywords
  • satisfiability
  • backdoor (depth)

Metrics

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

Related Versions

References

  1. Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information Processing Letters, 8(3):121-123, 1979. Google Scholar
  2. Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #SAT and Bayesian inference. In 44th Annual IEEE Symposium on Foundations of Computer Science (FOCS'03), pages 340-351, 2003. Google Scholar
  3. Jannis Bulian and Anuj Dawar. Graph isomorphism parameterized by elimination distance to bounded degree. Algorithmica, 75(2):363-382, 2016. Google Scholar
  4. Stephen A. Cook. The complexity of theorem-proving procedures. In Proc. 3rd Annual Symp. on Theory of Computing, pages 151-158, Shaker Heights, Ohio, 1971. Google Scholar
  5. William F. Dowling and Jean H. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Programming, 1(3):267-284, 1984. Google Scholar
  6. Fedor V Fomin, Petr A Golovach, and Dimitrios M Thilikos. Parameterized complexity of elimination distance to first-order logic properties. arXiv preprint arXiv:2104.02998, 2021. Google Scholar
  7. Vijay Ganesh and Moshe Y. Vardi. On the unreasonable effectiveness of SAT solvers. In Tim Roughgarden, editor, Beyond the Worst-Case Analysis of Algorithms, pages 547-566. Cambridge University Press, 2020. URL: https://doi.org/10.1017/9781108637435.032.
  8. Robert Ganian, M. S. Ramanujan, and Stefan Szeider. Backdoor treewidth for SAT. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 20-37. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_2.
  9. Robert Ganian, M. S. Ramanujan, and Stefan Szeider. Combining treewidth and backdoors for CSP. In Heribert Vollmer and Brigitte Vallée, editors, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017), volume 66 of Leibniz International Proceedings in Informatics (LIPIcs), pages 36:1-36:17, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.36.
  10. Robert Ganian, M. S. Ramanujan, and Stefan Szeider. Discovering archipelagos of tractability for constraint satisfaction and counting. ACM Transactions on Algorithms, 13(2):29:1-29:32, 2017. Full version of a SODA'16 paper. URL: https://doi.org/10.1145/3014587.
  11. Serge Gaspers, Neeldhara Misra, Sebastian Ordyniak, Stefan Szeider, and Stanislav Zivny. Backdoors into heterogeneous classes of SAT and CSP. J. of Computer and System Sciences, 85:38-56, 2017. URL: https://doi.org/10.1016/j.jcss.2016.10.007.
  12. Serge Gaspers, Sebastian Ordyniak, M. S. Ramanujan, Saket Saurabh, and Stefan Szeider. Backdoors to q-Horn. Algorithmica, 74(1):540-557, 2016. URL: https://doi.org/10.1007/s00453-014-9958-5.
  13. Serge Gaspers and Stefan Szeider. Strong backdoors to bounded treewidth SAT. In 54th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2013, 26-29 October, 2013, Berkeley, CA, USA, pages 489-498. IEEE Computer Society, 2013. Google Scholar
  14. Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Satisfiability solvers. In Handbook of Knowledge Representation, volume 3 of Foundations of Artificial Intelligence, pages 89-134. Elsevier, 2008. Google Scholar
  15. Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding first-order properties of nowhere dense graphs. J. ACM, 64(3):17:1-17:32, 2017. URL: https://doi.org/10.1145/3051095.
  16. Leonid Levin. Universal sequential search problems. Problems of Information Transmission, 9(3):265-266, 1973. Google Scholar
  17. Nikolas Mählmann, Sebastian Siebertz, and Alexandre Vigny. Recursive backdoors for SAT. In Filippo Bonchi and Simon J. Puglisi, editors, 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia, volume 202 of LIPIcs, pages 73:1-73:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.73.
  18. Dániel Marx. Parameterized complexity and approximation algorithms. Comput. J., 51(1):60-78, 2008. URL: https://doi.org/10.1093/comjnl/bxm048.
  19. Jaroslav Nesetril and Patrice Ossona de Mendez. Tree-depth, subgraph coloring and homomorphism bounds. European J. Combin., 27(6):1022-1041, 2006. Google Scholar
  20. Jaroslav Nešetřil and Patrice Ossona de Mendez. Sparsity - Graphs, Structures, and Algorithms, volume 28 of Algorithms and combinatorics. Springer, 2012. Google Scholar
  21. Naomi Nishimura, Prabhakar Ragde, and Stefan Szeider. Detecting backdoor sets with respect to Horn and binary clauses. In Proceedings of SAT 2004 (Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May, 2004, Vancouver, BC, Canada), pages 96-103, 2004. Google Scholar
  22. Sebastian Ordyniak, Andre Schidler, and Stefan Szeider. Backdoor DNFs. In Zhi-Hua Zhou, editor, Proceeding of IJCAI-2021, the 30th International Joint Conference on Artificial Intelligence, pages 1403-1409, 2021. URL: https://doi.org/10.24963/ijcai.2021/194.
  23. Marko Samer and Stefan Szeider. Backdoor trees. In AAAI 08, Twenty-Third Conference on Artificial Intelligence, Chicago, Illinois, July 13-17, 2008, pages 363-368. AAAI Press, 2008. Google Scholar
  24. Marko Samer and Stefan Szeider. Algorithms for propositional model counting. J. Discrete Algorithms, 8(1):50-64, 2010. Google Scholar
  25. Thomas J. Schaefer. The complexity of satisfiability problems. In Conference Record of the Tenth Annual ACM Symposium on Theory of Computing (San Diego, Calif., 1978), pages 216-226. ACM, 1978. Google Scholar
  26. Ryan Williams, Carla Gomes, and Bart Selman. Backdoors to typical case complexity. In Georg Gottlob and Toby Walsh, editors, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, IJCAI 2003, pages 1173-1178. Morgan Kaufmann, 2003. 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