arXiv preprint ·
Solving SAT via Treewidth Backdoors in Linear Time: Beyond Sparsity
- Published
- Source
- arXiv preprint, posted before peer review
- Original
- Read it at arXiv
- Topics
Abstract
The Boolean Satisfiability (SAT) problem is a remarkably expressive computational problem, serving both as a cornerstone of complexity theory and as a unifying language for a wide range of search and reasoning tasks. While $\mathrm{NP}$-complete in general, SAT is well known to be linear-time solvable on instances with bounded treewidth. This motivates the search for "hidden" tree-like structures in formulas---for instance by detecting so-called weak $t$-treewidth backdoors. Such backdoors are sets of $k$ variables that can be assigned in such a way that the remaining instance has treewidth at most $t$ and is satisfiable whenever the original instance is. Ever since Gaspers and Szeider [ICALP 2012] showed that finding a weak $t$-treewidth backdoor for a SAT formula is $\mathrm{W}[2]$-hard with respect to $k$, tractability results have been restricted to structurally sparse formulas---most notably, a linear-time algorithm for $d$-SAT (bounded clause-length SAT) by Fomin, Lokshtanov, Misra, Ramanujan, and Saurabh [SODA 2015] and a non-uniform polynomial-time algorithm when the incidence graph of the input formula belongs to a nowhere-dense graph class (or more generally is $K_{d,d}$-free) by Lokshtanov, Panolan, and Ramanujan [ICALP 2022]. In this paper, we push the tractability boundaries of finding weak $t$-treewidth backdoors beyond sparsity and into the regime of "well-behaved" dense formulas. Aiming towards relaxing structural input restrictions from nowhere-dense to edge-stable graph classes, as featured in the theory of beyond sparsity for FO model checking, or to bounded VC-dimension set systems, we identify signed semi-ladder-freeness as the correct dense structural restriction that establishes the boundary between tractability and intractability along this line.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Data Structures & Algorithms
Query Complexity of Densest Sub(hyper)graph Problems
Geometric Kernel Diversity: An Axiomatic Diversity Measure in Euclidean Space
Nearly Optimal Quantum Sample Complexity of Learning Fourier-Sparse Boolean Functions
Undirected Network Coding and Faster External-Memory Integer Sorting
Hitting Minors: Stronger Lower Bounds
Get the few papers worth your time in Data Structures & Algorithms every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.