Solving SAT via Treewidth Backdoors in Linear Time: Beyond Sparsity

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.