PaperlayerView exact revision on arXiv

Source-linked AI summary

Solving SAT via Treewidth Backdoors in Linear Time: Beyond Sparsity

Jan Dreier, Robert Ganian, Marlene Gründel, Roohani Sharma, Simon Wietheger

arXiv:2610.18540v1cs.DScs.CC

TL;DR

Finding weak t-treewidth backdoors is hard in general, with prior tractability results focused on sparse formulas. The paper studies signed semi-ladder-freeness and gives a linear-time algorithm for detecting these backdoors, while showing hardness under nearby structural restrictions.

  • Problem

    Finding weak t-treewidth backdoors is W[2]-hard in general, and prior tractability results concern sparse formulas.

    Source: §1 · p. 2

  • Method

    The paper uses signed incidence graphs that encode literal polarity and restricts signed semi-ladder height to obtain a backdoor-detection algorithm.

    Source: §1 · p. 4

  • Results

    For fixed d, k, and t, the algorithm runs in linear time on signed d-semi-ladder-free instances, while detection is W[1]-hard on signed ladder-free instances.

    Source: §1 · pp. 3–4

  • Takeaways & Limitations

    Signed semi-ladder-freeness provides a structural condition for tractable weak-backdoor detection beyond sparse SAT classes.

    Source: §6 · p. 37

    The current algorithmic write-up expects a bound on signed semi-ladder height as input, and determining a tight upper bound is non-trivial.

    Source: §6 · p. 37

Abstract

from arXiv · show

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.

1 Introduction

Weak t-treewidth backdoors expose a hidden tractable structure by assigning a small set of variables, but finding them is hard without structural restrictions. The paper identifies signed semi-ladder-freeness as a dense-graph condition permitting linear-time detection, while related hardness results delimit that tractability.

1 Introduction

  • A weak t-treewidth backdoor is a set of variables with an assignment that leaves a satisfiable instance of treewidth at most t whenever the original formula is satisfiable.Unlike a strong backdoor, it requires only one suitable assignment rather than every assignment.Source: §1 · p. 2
  • Finding weak t-treewidth backdoors is W[2]-hard in general, while prior tractability results rely on sparse inputs such as d-SAT or K_d,d-free formulas.The cited K_d,d-free algorithm has a superlinear n^O(d) factor.Source: §1 · p. 2
  • Semi-ladders retain forced upper-triangle edges and horizontal non-edges but leave the lower triangle unconstrained, unlike ladders.Their bounded index also combines bounded ladder height and co-matching index, connecting stability with a Helly-type finite-obstruction property.Source: §1 · p. 3
  • Signed incidence graphs retain whether each variable occurs positively or negatively, and signed semi-ladder-freeness is equivalent up to a factor of 2 and an additive constant to the corresponding duplicated-literal representation.This addresses the limitation of unsigned incidence graphs, which do not encode literal polarity.Source: §1 · p. 4
  • For fixed d, k, and t, a linear-time algorithm on signed d-semi-ladder-free instances returns a satisfying assignment and weak t-treewidth backdoor of size at most k, or reports none exists.This generalizes the d-SAT algorithm and avoids the n^O(d) factor of the K_d,d-free result.Source: §1 · p. 4
  • Signed semi-ladder-freeness marks a boundary: detection is W[2]-hard when only unsigned semi-ladders are excluded and W[1]-hard on signed ladder-free instances.Both lower bounds hold for constant d and every fixed t ≥ 0.Source: §1 · p. 5

2 Technical Overview

The overview combines a reducer, extractor, and progressor to find weak treewidth backdoors, with the progressor’s bounded measure enabling termination. Dense instances require special care: the reducer and extractor are structure-oblivious, while progress depends on signed semi-ladder-freeness.

2 Technical Overview

  • The algorithm iteratively combines a reducer that prepares instances, an extractor that samples a backdoor-relevant variable or clause, and a progressor that eliminates it.The reducer creates conditions for successful extraction; the progressor acts on the extracted variable or clause to advance the search.Source: §2 · p. 7
  • Earlier K_d,d-free SAT algorithms waited through bounded extractor–progressor rounds and incurred |φ|^O(d) time, whereas this approach handles a broader class in linear time.The overview identifies this as a key challenge in extending the procedure beyond d-SAT.Source: §2 · p. 8

The progressor.

  • The progressor tracks k candidate sets P_i, narrows a guessed set when a clause must be satisfied, and cleanup makes the maximum annotated semi-ladder height strictly decrease.This bounds total progressor branching by s := (d − 1)k.Source: The progressor · pp. 8–9

The reducer.

  • The reducer compresses sufficiently large O(t)-protrusions to size f(k, t, d), because annotations make the graph boundary alone an incomplete account of information flow.The resulting bound differs from the f(t) bound available with a protrusion’s genuine boundary but suffices for the algorithm.Source: The reducer · p. 9
  • The extractor is deterministic and structure-oblivious, as are the reducer’s preprocessing steps; additional input structure is needed by the progressor to ensure progress.Earlier derandomization relied on sparse structure, while this approach does not.Source: §2 · p. 8, The reducer · p. 10
  • After reducer preprocessing, any weak backdoor neighborhood is a ρ-cover, which lets the extractor find a K_t+2,t+2 or identify a high-edge-share vertex in linear time.A found biclique is an obstruction to treewidth at most t and supplies candidate variables and clauses; the reducer’s cover guarantee supports the linear-time search.Source: The reducer · pp. 10–11
  • On dense instances, repeatedly removing a fraction of vertices may leave edge counts high and make naive preprocessing O(|φ| log |φ|), so the reducer must manage repetition carefully.In the sparse case, geometric decrease in vertices and linearly bounded edges keeps exhaustive preprocessing linear.Source: The reducer · p. 11

3 Preliminaries

The preliminaries define the graph and backdoor objects used to state the algorithm’s auxiliary problem. They relate signed and unsigned semi-ladder heights and connect weak backdoors to annotated graph instances.

Preliminaries

  • Signed incidence graph variants encode literal or variable–clause occurrences, with signs distinguishing positive and negative occurrences in the edge representation.The signed vertex representation uses literal vertices and opposite-literal edges; the signed edge representation assigns signs to variable–clause edges.Source: §3 · p. 12
  • A semi-ladder of height h has ordered vertex pairs (a_i,b_i), with {a_i,b_i} absent and {a_i,b_j} present whenever i < j; the stated bounds are hV ≤ h ≤ hV + 4 and hE ≤ hV ≤ 2hE.Source: §3 · pp. 12–13
  • For a formula φ with maximum signed semi-ladder height hs, maximum unsigned semi-ladder height hu is at most 4hs + 2; thus constant signed height implies constant unsigned height.Source: §3 · p. 14
  • A weak backdoor is a variable set with an assignment yielding a satisfiable residual formula whose unsigned incidence graph has treewidth at most t.The assigned literals may also represent the variables in the backdoor.Source: §3 · p. 14
  • An SL-pattern records, for each candidate set P_i, the largest proper semi-ladder whose literal vertices lie in P_i; its size sums those heights.The paper states that weak-backdoor detection is equivalent to an Ext-WB-TW instance in which every P_i contains all literal vertices.Source: §3 · pp. 15–16
  • Ext-WB-TW solutions choose one literal from each candidate set and satisfy non-conflict, bounded-treewidth, and domination conditions.Bounded treewidth concerns the residual graph after deleting the selected literals’ neighborhood and contracting opposite-literal edges; domination captures extendibility to a satisfying assignment.Source: §3 · pp. 15–16
  • A solution to Ext-WB-TW with target t gives both G − N_G[X] and G − N_G(X) treewidth at most 2t + 1.The bound accounts for replacing each contracted opposite-literal vertex in a width-t decomposition by its two endpoints.Source: §3 · p. 16

4 Weak Backdoors to Treewidth for Semi-Ladder-free SAT

This section develops a recursive algorithm for finding weak treewidth backdoors in signed semi-ladder-free SAT, using reduction, extraction, and branching to preserve solutions while reducing the search parameters. Together with simple base cases, the method yields a linear-time algorithm for deciding whether such a backdoor exists and solving SAT.

4 Weak Backdoors to Treewidth for Semi-Ladder-free SAT

  • Theorem 4.1 reduces each instance in O_{k,s,t}(n + m) time to at most q(k, s, t) instances, decrementing k or s, preserving yes/no status, and allowing solutions to be lifted.The input is a yes-instance exactly when at least one output instance is a yes-instance; a solution to an output can be converted to one for the input in O_{k,s,t}(n) time.Source: §4 · p. 16

4.1 The Reducer

  • The reducer iteratively replaces large protrusions, shrinking instances by a constant fraction per round until every solution’s neighborhood is a ρ-cover.The cover property makes each solution’s neighborhood include a constant fraction of edge-endpoints, enabling extraction; the reducer preserves yes/no status and supports solution recovery.Source: §4 · p. 16, §4.1 · p. 17

4.1.1 The Protrusion Replacer

  • Bounded-treewidth protrusions have computable bounded-size equivalent representatives with solution lifting, enabling replacement of sufficiently large protrusions while preserving well-formedness and yes/no status.The representative can be computed in time f(k, r, s, t) · |G|; replacing an r-protrusion of size at least f(k, r, s, t) + 1 strictly reduces the graph’s vertex count.Source: §4.1.1 · pp. 18, 20, 21

4.1.2 Constructing the Reducer

  • Each replacement round runs in O_{k,s,t}(n) time and recovers solutions; under specified protrusion-decomposition bounds it shrinks vertices by a constant factor, making iteration linear even if edges do not shrink.The shrink condition includes β ≤ 4t + 4; the linear-in-vertices bound tightens the O(n + m) bound of.Source: §4.1.2 · p. 21
  • The reducer runs in O_k,s,t(n + m) time, preserves equivalence and solution recovery, and stops with an instance where every solution neighborhood is a ρ-cover.It repeatedly applies equivalent shrinking rounds until the next round fails to shrink the graph.Source: §4.1.2 · pp. 23–24

4.2 The Extractor

  • The extractor deterministically returns V′ of size at most (2k/ρ)^O(t) intersecting N_G[X] for every solution, in time (2k/ρ)^O(t²)·|G|.A random-edge sample can hit the neighborhood of one fixed solution, but the extractor constructs a single set that works for all solutions.Source: §4.2 · pp. 24, 25, 27

4.3 The Progressor

  • Given a vertex, the progressor runs in O(k²(n + m)) time and returns at most 2k instances reducing k or s by one, preserving the specified yes-instance condition and solution transfer.The condition is that the original yes-instance has a solution X with v ∈ N_G[X]; solutions of returned instances transfer in O(n) time.Source: §4.3 · p. 27
  • For a literal-vertex branch, removing its selected coordinate yields an equivalent instance, and solutions transfer back by restoring that literal.Source: §4.3 · p. 29
  • For a clause vertex C, the progressor restricts one candidate set to literals adjacent to C and deletes clauses guaranteed satisfied, reducing SL-pattern size by at least one while preserving solutions.Source: §4.3 · pp. 29–30

4.4 Deriving the Main Result

  • The recursion produces a parameter-bounded number of well-formed instances, each decreasing k or s, preserves yes-instance equivalence, and lifts solutions in O_k,s,t(n) time.The overall recursion runs in O_k,s,t(n + m) time.Source: §4.4 · pp. 30–31
  • With no clause vertices, Ext-WB-TW is solvable in O(k^{k+1}+kn) time; for k=0 on an n-vertex, m-edge graph, it is solvable in 2^{O(t^3)}·(n+m) time.Source: §4.4 · p. 31
  • A linear-time algorithm for signed d-semi-ladder-free SAT outputs a satisfying assignment and weak t-treewidth backdoor of size at most k, or detects that none exists.Source: §4.4 · p. 32
  • The formula is translated into Ext-WB-TW and recursively reduced until k or s is zero; the resulting bounded number of instances and total procedure run in O_d,k,t(n + m) time.The translation identifies consistent literal selections with partial assignments whose residual incidence graph has treewidth at most t and is satisfiable.Source: §4.4 · pp. 32–33

5 Hardness of Finding Weak Backdoors

The section establishes hardness boundaries for weak-backdoor detection using two different structural restrictions. Red-Blue Dominating Set reductions yield hardness on signed ladder-free and unsigned semi-ladder-free SAT instances.

Hardness results

  • Weak-backdoor detection is W[1]-hard on L_d-free signed incidence graphs for d ≥ 18 and W[2]-hard on SL_d-free unsigned incidence graphs for d ≥ 4.Together, the lower bounds support signed semi-ladder-freeness as the structural restriction used for the tractability result.Source: §5 · pp. 34, 36

Signed ladder-free instances

  • For the signed-graph reduction, each red vertex yields t + 1 positive literals and each blue vertex yields t + 1 clauses, with occurrences encoding adjacency.The constructed signed incidence graph is L_{d+1}-free when the Red-Blue Dominating Set instance is L_d-free, and the reduction preserves the decision.Source: §5 · pp. 34–35

Unsigned semi-ladder-free instances

  • The unsigned-graph reduction uses k(t + 1) variables per red-vertex family, blue-vertex clauses, and special clauses to encode domination.Its correctness argument links a size-k dominating set to an assignment leaving treewidth zero, and conversely recovers a dominating set from a suitable assignment.Source: §5 · pp. 36–37
  • The unsigned construction excludes semi-ladders of height four by separating variable neighborhoods of special clauses into disjoint sets.A height-four semi-ladder would force two such sets to coincide while also requiring a variable in their difference, a contradiction.Source: §5 · p. 36

6 Concluding Remarks

The paper gives a linear-time algorithm for weak-backdoor detection on SAT instances with bounded signed semi-ladder height and complements it with lower bounds. It identifies structural questions for future work and notes that the current algorithm expects the height bound as input.

Main result

  • For fixed d, k, and t, weak t-treewidth backdoors of size at most k can be detected in linear time when the signed incidence graph excludes semi-ladders of height d.The result generalizes prior algorithms for bounded-clause-width SAT and K_d,d-free SAT.Source: §6 · p. 37

Structural boundaries and future work

  • The lower bounds show that excluding large signed ladders or unsigned semi-ladders does not suffice for the same tractability result.The paper points to excluding large ladders as transductions, or to bounded twin-width, as directions not ruled out by those bounds.Source: §6 · p. 37

Algorithmic scope

  • The current algorithm expects a signed semi-ladder-height bound as input, while a modified version can return a height-d semi-ladder as a witness when that bound is insufficient.The authors note that no linear-time algorithm for determining a tight upper bound is known to them.Source: §6 · pp. 37–38

A W[1]-hardness of Minimum Weight SAT on K2,2-free instances

This appendix establishes W[1]-hardness of Minimum Weight SAT on K2,2-free instances by reducing from Multicolored Clique. The reduction encodes color choices and non-adjacency constraints as clauses.

Hardness result

Reduction

  • The reduction creates one variable per graph vertex, a positive clause for each color class, and a negative clause for each non-adjacent vertex pair.A clique of size k corresponds to setting its k vertex variables to 1 and all others to 0.Source: A W[1]-hardness of Minimum Weight SAT… · p. 42

Correctness

  • Conversely, any satisfying assignment with at most k ones selects exactly one vertex from each color class, and those vertices form a clique.The color-class clauses force one selected vertex per class, while the non-adjacency clauses rule out selected non-edges.Source: A W[1]-hardness of Minimum Weight SAT… · p. 42
Loading 2610.18540v1…