Document Open Access Logo

Backdoor Sets on Nowhere Dense SAT

Authors Daniel Lokshtanov, Fahad Panolan , M. S. Ramanujan

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.91.pdf
  • Filesize: 0.86 MB
  • 20 pages

Document Identifiers

Author Details

Daniel Lokshtanov
  • University of California, Santa Barbara, CA, USA
Fahad Panolan
  • Indian Institute of Technology Hyderabad, India
M. S. Ramanujan
  • University of Warwick, Coventry, UK

Funding

  • Lokshtanov, Daniel: Supported by United States-Israel Binational Science Foundation (BSF) grant no. 2018302 and National Science Foundation (NSF) award CCF-2008838.
  • Panolan, Fahad: Supported by Seed grant, IIT Hyderabad (SG/IITH/F224/2020-21/SG-79).
  • Ramanujan, M. S.: Supported by Engineering and Physical Sciences Research Council (EPSRC) grants EP/V007793/1 and EP/V044621/1.

Cite As Get BibTex

Daniel Lokshtanov, Fahad Panolan, and M. S. Ramanujan. Backdoor Sets on Nowhere Dense SAT. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 91:1-91:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ICALP.2022.91

Abstract

For a satisfiable CNF formula ϕ and an integer t, a weak backdoor set to treewidth-t is a set of variables such that there is an assignment to this set that reduces ϕ to a satisfiable formula that has an incidence graph of treewidth at most t. A natural research program in the work on fixed-parameter algorithms (FPT algorithms) for SAT is to delineate the tractability borders for the problem of detecting a small weak backdoor set to treewidth-t formulas. In this line of research, Gaspers and Szeider (ICALP 2012) showed that detecting a weak backdoor set of size at most k to treewidth-1 is W[2]-hard parameterized by k if the input is an arbitrary CNF formula. Fomin, Lokshtanov, Misra, Ramanujan and Saurabh (SODA 2015), showed that if the input is d-CNF, then detecting a weak backdoor set of size at most k to treewidth-t is fixed-parameter tractable (parameterized by k,t,d). These two results indicate that sparsity of the input plays a role in determining the parameterized complexity of detecting weak backdoor sets to treewidth-t. 
In this work, we take a major step towards characterizing the precise impact of sparsity on the parameterized complexity of this problem by obtaining algorithmic results for detecting small weak backdoor sets to treewidth-t for input formulas whose incidence graphs belong to a nowhere-dense graph class. Nowhere density provides a robust and well-understood notion of sparsity that is at the heart of several advances on model checking and structural graph theory. Moreover, nowhere-dense graph classes contain many well-studied graph classes such as bounded treewidth graphs, graphs that exclude a fixed (topological) minor and graphs of bounded expansion. 
Our main contribution is an algorithm that, given a formula ϕ whose incidence graph belongs to a fixed nowhere-dense graph class and an integer k, in time f(t,k)|ϕ|^O(1), either finds a satisfying assignment of ϕ, or concludes correctly that ϕ has no weak backdoor set of size at most k to treewidth-t. 
To obtain this algorithm, we develop a strategy that only relies on the fact that nowhere-dense graph classes are biclique-free. That is, for every nowhere-dense graph class, there is a p such that it is contained in the class of graphs that exclude K_{p,p} as a subgraph. This is a significant feature of our techniques since the class of biclique-free graphs also generalizes the class of graphs of bounded degeneracy, which are incomparable with nowhere-dense graph classes. As a result, our algorithm also generalizes the results of Fomin, Lokshtanov, Misra, Ramanujan and Saurabh (SODA 2015) for the special case of d-CNF formulas as input when d is fixed. This is because the incidence graphs of such formulas exclude K_{d+1,d+1} as a subgraph.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parameterized complexity and exact algorithms
Keywords
  • Fixed-parameter Tractability
  • Satisfiability
  • Backdoors
  • Treewidth

Metrics

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

References

  1. Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy problems for tree-decomposable graphs. Journal of Algorithms, 12:308-340, 1991. Google Scholar
  2. Christian Bessiere, Clément Carbonnel, Emmanuel Hebrard, George Katsirelos, and Toby Walsh. Detecting and exploiting subproblem tractability. In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013. IJCAI/AAAI, 2013. Google Scholar
  3. Hans L. Bodlaender. A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM J. Comput., 25(6):1305-1317, 1996. Google Scholar
  4. Clément Carbonnel, Martin C. Cooper, and Emmanuel Hebrard. On backdoors to tractable constraint languages. In Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings, volume 8656 of Lecture Notes in Computer Science, pages 224-239. Springer Verlag, 2014. Google Scholar
  5. Rajesh Chitnis, Marek Cygan, MohammadTaghi Hajiaghayi, Marcin Pilipczuk, and Michal Pilipczuk. Designing FPT algorithms for cut problems using randomized contractions. SIAM J. Comput., 45(4):1171-1229, 2016. URL: https://doi.org/10.1137/15M1032077.
  6. Pratibha Choudhary, Lawqueen Kanesh, Daniel Lokshtanov, Fahad Panolan, and Saket Saurabh. Parameterized complexity of feedback vertex sets on hypergraphs. In Nitin Saxena and Sunil Simon, editors, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, December 14-18, 2020, BITS Pilani, K K Birla Goa Campus, Goa, India (Virtual Conference), volume 182 of LIPIcs, pages 18:1-18:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2020.18.
  7. Bruno Courcelle. The monadic second-order logic of graphs I: Recognizable sets of finite graphs. Information and Computation, 85:12-75, 1990. Google Scholar
  8. Bruno Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. Handbook of Graph Grammars, pages 313-400, 1997. Google Scholar
  9. Y. Crama, O. Ekin, and P. L. Hammer. Variable and term removal from Boolean formulae. Discr. Appl. Math., 75(3):217-230, 1997. Google Scholar
  10. Rina Dechter and Judea Pearl. Tree clustering for constraint networks. Artif. Intell., pages 353-366, 1989. Google Scholar
  11. Pål Grønås Drange, Markus Sortland Dregi, Fedor V. Fomin, Stephan Kreutzer, Daniel Lokshtanov, Marcin Pilipczuk, Michal Pilipczuk, Felix Reidl, Fernando Sánchez Villaamil, Saket Saurabh, Sebastian Siebertz, and Somnath Sikdar. Kernelization and sparseness: the case of dominating set. In 33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France, volume 47 of LIPIcs, pages 31:1-31:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.STACS.2016.31.
  12. Eduard Eiben, Mithilesh Kumar, Amer E. Mouawad, Fahad Panolan, and Sebastian Siebertz. Lossy kernels for connected dominating set on sparse graphs. SIAM J. Discret. Math., 33(3):1743-1771, 2019. URL: https://doi.org/10.1137/18M1172508.
  13. Fedor V. Fomin, Daniel Lokshtanov, Neeldhara Misra, M. S. Ramanujan, and Saket Saurabh. Solving d-sat via backdoors to small treewidth. In Piotr Indyk, editor, Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2015, San Diego, CA, USA, January 4-6, 2015, pages 630-641. SIAM, 2015. URL: https://doi.org/10.1137/1.9781611973730.43.
  14. Fedor V. Fomin, Daniel Lokshtanov, Neeldhara Misra, and Saket Saurabh. Planar F-deletion: Approximation, kernelization and optimal FPT algorithms. In Proceedings of the 53rd Annual Symposium on Foundations of Computer Science (FOCS), pages 470-479. IEEE, 2012. Google Scholar
  15. Eugene C. Freuder. A sufficient condition for backtrack-bounded search. J. ACM, 32(4):755-761, 1985. URL: https://doi.org/10.1145/4221.4225.
  16. Robert Ganian, Sebastian Ordyniak, and M. S. Ramanujan. Going beyond primal treewidth for (M)ILP. In Satinder P. Singh and Shaul Markovitch, editors, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, February 4-9, 2017, San Francisco, California, USA, pages 815-821. AAAI Press, 2017. URL: http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14272.
  17. Robert Ganian, M. S. Ramanujan, and Stefan Szeider. Discovering archipelagos of tractability for constraint satisfaction and counting. In Robert Krauthgamer, editor, Proceedings of the Twenty-Seventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2016, Arlington, VA, USA, January 10-12, 2016, pages 1670-1681. SIAM, 2016. URL: https://doi.org/10.1137/1.9781611974331.ch114.
  18. 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, March 8-11, 2017, Hannover, Germany, volume 66 of LIPIcs, pages 36:1-36:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.36.
  19. Valentin Garnero, Christophe Paul, Ignasi Sau, and Dimitrios M Thilikos. Explicit Linear Kernels via Dynamic Programming. In STACS, pages 312-324, 2014. Google Scholar
  20. Serge Gaspers, Neeldhara Misra, Sebastian Ordyniak, Stefan Szeider, and Stanislav Zivny. Backdoors into heterogeneous classes of SAT and CSP. In Carla E. Brodley and Peter Stone, editors, Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada., pages 2652-2658. AAAI Press, 2014. Google Scholar
  21. 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.
  22. Serge Gaspers, Sebastian Ordyniak, and Stefan Szeider. Backdoor sets for CSP. In Andrei A. Krokhin and Stanislav Zivny, editors, The Constraint Satisfaction Problem: Complexity and Approximability, volume 7 of Dagstuhl Follow-Ups, pages 137-157. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/DFU.Vol7.15301.5.
  23. Serge Gaspers and Stefan Szeider. Backdoors to acyclic SAT. In Proceedings of the 39th International Colloquium on Automata, Languages, and Programming (ICALP), volume 7391 of Lecture Notes in Computer Science, pages 363-374. Springer, 2012. Google Scholar
  24. Serge Gaspers and Stefan Szeider. Strong backdoors to nested satisfiability. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, volume 7317 of Lecture Notes in Computer Science, pages 72-85. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_7.
  25. Serge Gaspers and Stefan Szeider. Backdoors to satisfaction. In The Multivariate Algorithmic Revolution and Beyond, pages 287-317, 2012. URL: https://doi.org/10.1007/978-3-642-30891-8_15.
  26. 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
  27. 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.
  28. Donald E. Knuth. Nested satisfiability. Acta Informatica, 28(1):1-6, 1990. URL: https://doi.org/10.1007/BF02983372.
  29. Stephan Kreutzer, Roman Rabinovich, and Sebastian Siebertz. Polynomial kernels and wideness properties of nowhere dense graph classes. ACM Trans. Algorithms, 15(2):24:1-24:19, 2019. URL: https://doi.org/10.1145/3274652.
  30. Daniel Lokshtanov, M. S. Ramanujan, Saket Saurabh, and Meirav Zehavi. Reducing CMSO model checking to highly connected graphs. In Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella, editors, 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, July 9-13, 2018, Prague, Czech Republic, volume 107 of LIPIcs, pages 135:1-135:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.135.
  31. Jaroslav Nesetril and Patrice Ossona de Mendez. First order properties on nowhere dense structures. J. Symb. Log., 75(3):868-887, 2010. URL: https://doi.org/10.2178/jsl/1278682204.
  32. Jaroslav Nesetril and Patrice Ossona de Mendez. On nowhere dense graphs. Eur. J. Comb., 32(4):600-617, 2011. URL: https://doi.org/10.1016/j.ejc.2011.01.006.
  33. 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
  34. Geevarghese Philip, Venkatesh Raman, and Somnath Sikdar. Polynomial kernels for dominating set in graphs of bounded degeneracy and beyond. ACM Trans. Algorithms, 9(1):11:1-11:23, 2012. URL: https://doi.org/10.1145/2390176.2390187.
  35. Igor Razgon and Barry O'Sullivan. Almost 2-SAT is fixed parameter tractable. J. of Computer and System Sciences, 75(8):435-450, 2009. Google Scholar
  36. Neil Robertson and P. D. Seymour. Graph minors. V. Excluding a planar graph. J. Combin. Theory Ser. B, 41(1):92-114, 1986. Google Scholar
  37. Marko Samer and Stefan Szeider. Backdoor sets of quantified boolean formulas. In J. Marques-Silva and K. A. Sakallah, editors, Proceedings of SAT 2007, Tenth International Conference on Theory and Applications of Satisfiability Testing, May 28-31, 2007, Lisbon, Portugal,, volume 4501 of Lecture Notes in Computer Science, pages 230­-243, 2007. Google Scholar
  38. Marko Samer and Stefan Szeider. Constraint satisfaction with bounded treewidth revisited. J. Comput. Syst. Sci., 76(2):103-114, 2010. URL: https://doi.org/10.1016/j.jcss.2009.04.003.
  39. Stefan Szeider. Matched formulas and backdoor sets. In J. Marques-Silva and K. A. Sakallah, editors, Proceedings of SAT 2007, Tenth International Conference on Theory and Applications of Satisfiability Testing, May 28-31, 2007, Lisbon, Portugal,, volume 4501 of Lecture Notes in Computer Science, pages 94-99, 2007. Google Scholar
  40. Jan Arne Telle and Yngve Villanger. FPT algorithms for domination in sparse graphs and beyond. Theor. Comput. Sci., 770:62-68, 2019. URL: https://doi.org/10.1016/j.tcs.2018.10.030.
  41. 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 About DROPS Imprint Privacy Contact