Document Open Access Logo

Recursive Backdoors for SAT

Authors Nikolas Mählmann , Sebastian Siebertz , Alexandre Vigny

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2021.73.pdf
  • Filesize: 0.86 MB
  • 18 pages

Document Identifiers

Author Details

Nikolas Mählmann
  • University of Bremen, Germany
Sebastian Siebertz
  • University of Bremen, Germany
Alexandre Vigny
  • University of Bremen, Germany

Funding

This research is funded by the German Research Foundation (DFG, Deutsche Forschungsgemeinschaft) - Projektnummer 444419611.

Cite AsGet BibTex

Nikolas Mählmann, Sebastian Siebertz, and Alexandre Vigny. Recursive Backdoors for SAT. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 73:1-73:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.MFCS.2021.73

Abstract

A strong backdoor in a formula φ of propositional logic to a tractable class C of formulas is a set B of variables of φ such that every assignment of the variables in B results in a formula from C. Strong backdoors of small size or with a good structure, e.g. with small backdoor treewidth, lead to efficient solutions for the propositional satisfiability problem SAT. In this paper we propose the new notion of recursive backdoors, which is inspired by the observation that in order to solve SAT we can independently recurse into the components that are created by partial assignments of variables. The quality of a recursive backdoor is measured by its recursive backdoor depth. Similar to the concept of backdoor treewidth, recursive backdoors of bounded depth include backdoors of unbounded size that have a certain treelike structure. However, the two concepts are incomparable and our results yield new tractability results for SAT.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Parameterized complexity and exact algorithms
Keywords
  • Propositional satisfiability SAT
  • Backdoors
  • Parameterized Algorithms

Metrics

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

Related Versions

References

  1. Stephen A Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing, pages 151-158, 1971. Google Scholar
  2. Marek Cygan, Fedor Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer Publishing Company, Incorporated, January 2015. Google Scholar
  3. Bistra Dilkina, Carla P. Gomes, and Ashish Sabharwal. Backdoors in the context of learning. In SAT, volume 5584 of Lecture Notes in Computer Science, pages 73-79. Springer, 2009. Google Scholar
  4. Vijay Ganesh and Moshe Y. Vardi. On the unreasonable effectiveness of SAT solvers. In Beyond the Worst-Case Analysis of Algorithms, pages 547-566. Cambridge University Press, 2020. Google Scholar
  5. Robert Ganian, M. S. Ramanujan, and Stefan Szeider. Backdoor treewidth for sat. In International Conference on Theory and Applications of Satisfiability Testing, pages 20-37. Springer, 2017. Google Scholar
  6. Robert Ganian, M. S. Ramanujan, and Stefan Szeider. Discovering archipelagos of tractability for constraint satisfaction and counting. ACM Transactions on Algorithms, 13(2):1–32, 2017. Google Scholar
  7. Serge Gaspers, Neeldhara Misra, Sebastian Ordyniak, Stefan Szeider, and Stanislav Živný. Backdoors into heterogeneous classes of SAT and CSP. Journal of Computer and System Sciences, 85:38–56, 2017. Google Scholar
  8. Serge Gaspers and Stefan Szeider. Backdoors to satisfaction. In The Multivariate Algorithmic Revolution and Beyond, pages 287-317. Springer, 2012. Google Scholar
  9. Serge Gaspers and Stefan Szeider. Strong backdoors to bounded treewidth SAT. 2013 IEEE 54th Annual Symposium on Foundations of Computer Science, 2013. Google Scholar
  10. Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? Journal of Computer and System Sciences, 63(4):512-530, 2001. Google Scholar
  11. N. Nishimura, P. Ragde, and Stefan Szeider. Detecting backdoor sets with respect to horn and binary clauses. In SAT, 2004. Google Scholar
  12. Sebastian Ordyniak, André Schidler, and Stefan Szeider. Backdoor DNFs. Technical Report AC-TR-21-001, Algorithms and Complexity Group, TU Wien, 2021. Google Scholar
  13. Neil Robertson and Paul D Seymour. Graph minors V. excluding a planar graph. Journal of Combinatorial Theory, Series B, 41(1):92-114, 1986. Google Scholar
  14. Marko Samer and Stefan Szeider. Backdoor trees. In Proceedings of the 23rd National Conference on Artificial Intelligence - Volume 1, AAAI'08, page 363–368. AAAI Press, 2008. Google Scholar
  15. Marko Samer and Stefan Szeider. Algorithms for propositional model counting. Journal of Discrete Algorithms, 8(1):50-64, 2010. Google Scholar
  16. Marko Samer and Stefan Szeider. Fixed-parameter tractability. Technical Report AC-TR-21-004, Algorithms and Complexity Group, TU Wien, 2021. Chapter 17, Handbook of Satisfiability, 2nd Edition, 2021. Google Scholar
  17. Ryan Williams, Carla P. Gomes, and Bart Selman. Backdoors to typical case complexity. In Proceedings of the 18th International Joint Conference on Artificial Intelligence, IJCAI'03, page 1173–1178. Morgan Kaufmann Publishers Inc., 2003. Google Scholar
  18. Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Robert Robere, Jia Hui Liang, Krzysztof Czarnecki, and Vijay Ganesh. Learning-sensitive backdoors with restarts. In CP, volume 11008 of Lecture Notes in Computer Science, pages 453-469. Springer, 2018. 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