Backdoor Sets on Nowhere Dense SAT

Lokshtanov, D. and Panolan, F. and Ramanujan, M.S. (2022) Backdoor Sets on Nowhere Dense SAT. In: 49th EATCS International Conference on Automata, Languages, and Programming, ICALP 2022, 4 July 2022 through 8 July 2022, Paris.

[img] Text
Leibniz_International_Proceedings_in_Informatics.pdf - Published Version
Available under License Creative Commons Attribution.

Download (910kB)


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 Kp,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 Kd+1,d+1 as a subgraph. © Daniel Lokshtanov, Fahad Panolan, and M. S. Ramanujan; licensed under Creative Commons License CC-BY 4.0

[error in script]
IITH Creators:
IITH CreatorsORCiD
Panolan, Fahad
Item Type: Conference or Workshop Item (Paper)
Additional Information: Funding Daniel Lokshtanov: Supported by United States-Israel Binational Science Foundation (BSF) grant no. 2018302 and National Science Foundation (NSF) award CCF-2008838. Fahad Panolan: Supported by Seed grant, IIT Hyderabad (SG/IITH/F224/2020-21/SG-79). M. S. Ramanujan: Supported by Engineering and Physical Sciences Research Council (EPSRC) grants EP/V007793/1 and EP/V044621/1.
Uncontrolled Keywords: Backdoors, Fixed-parameter Tractability, Satisfiability, Treewidth
Subjects: Computer science
Divisions: Department of Computer Science & Engineering
Depositing User: . LibTrainee 2021
Date Deposited: 18 Jul 2022 09:48
Last Modified: 18 Jul 2022 09:48
Publisher URL:
OA policy:
Related URLs:

Actions (login required)

View Item View Item
Statistics for RAIITH ePrint 9764 Statistics for this ePrint Item