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.

Text
Leibniz_International_Proceedings_in_Informatics.pdf - Published Version
Available under License Creative Commons Attribution.
Download (910kB)

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 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 Creators	ORCiD
Panolan, Fahad	https://orcid.org/0000-0001-6213-8687

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