PaperlayerView exact revision on arXiv

Source-linked AI summary

A Uniform Algorithm for Strict NP on Bounded-Treedepth Graphs

Thomas Depian, Robert Ganian, Jakob Greilhuber, Marlene Gründel, Simon Wietheger

arXiv:2610.06561v1cs.DScs.CC

TL;DR

Prior well-quasi-ordering results gave non-uniform linear-time algorithms for fixed SNP problems at bounded treedepth, without a construction procedure or computable parameter bounds. This paper provides a uniform constructive algorithm with computable parameter dependence and witness output, and applies it to graph parameters including stack number, queue number, track number, and twin-width.

  • Problem

    Existing bounded-treedepth results guaranteed linear-time algorithms for fixed SNP sentences but supplied neither a construction procedure nor computable bounds on parameter dependence, leaving several graph-parameter FPT questions open.

    Source: §1 · p. 2

  • Method

    The algorithm uses bounded-treedepth positive certificates in pruned instances to extend the earlier semi-FPT approach into a uniform decision procedure that can also output witnesses.

    Source: §2.1 · p. 5, §4 · p. 18

  • Results

    The algorithm decides SNP model checking in time f(|φ|, td(R)) · |R| for computable f and yields treedepth-linear-time algorithms for stack number, queue number, track number, twin-width, and boxicity.

    Source: Applications · p. 3, §4 · p. 18

  • Takeaways & Limitations

    The metatheorem resolves treedepth-parameterized fixed-parameter tractability for several hereditary graph problems, including stack number, queue number, track number, and twin-width.

    Source: Applications · p. 3

    Although the running-time function f is computable, the proof gives no closed-form upper bound on its growth.

    Source: Our Contribution · p. 3

Abstract

from arXiv · show

A classical well-quasi-ordering result guarantees the existence of non-uniform linear-time algorithms for all problems in Strict NP on relational structures of bounded treedepth; however, this provides neither a procedure for constructing these algorithms nor computable bounds on their parameter dependence. We turn this existential result into a uniform algorithmic metatheorem. Given a Strict NP sentence $\varphi$ and a relational structure $\mathcal{R}$, our algorithm decides whether $\mathcal{R}\models\varphi$ in time $f(|\varphi|, td(\mathcal{R})) \cdot |\mathcal{R}|$ for a computable function $f$, where the treedepth of $\mathcal{R}$ is measured on the Gaifman graph. The algorithm also constructs witness relations, with the polynomial exponent depending on their arity, and provides a unified framework for settling hereditary graph problems parameterized by treedepth. We also present several applications - among others, our result resolves open questions on the fixed-parameter tractability of computing the stack number, queue number, track number and twin-width parameterized by treedepth.

1 Introduction

Bounded treedepth gives well-quasi-ordering and existential linear-time algorithms for fixed SNP problems, but those results do not provide a construction procedure or computable parameter bounds. The paper supplies a uniform constructive metatheorem, applies it to graph parameters, and identifies limits to broader generalizations.

1 Introduction

  • Bounded-treedepth well-quasi-ordering yields linear-time algorithms for fixed SNP sentences, but the earlier result gives no construction procedure or computable parameter-dependence bound.The result also extends to relational structures over a fixed finite signature, with treedepth measured on the Gaifman graph.Source: §1 · p. 2
  • FPT status remained open for hereditary graph problems including queue number, stack number, track number, and twin-width, despite non-uniform linear-time guarantees.The passage identifies these as open questions in recent works [GR26] [DFGS25].Source: §1 · p. 2

Our Contribution

  • The metatheorem gives an SNP decision algorithm running in f(|φ|, td(R)) · |R| for computable f, without requiring forbidden-substructure characterizations as input.The treedepth is that of the input structure's Gaifman graph.Source: Our Contribution · p. 3
  • For positive instances, the algorithm can output requested witness relations, with the polynomial exponent depending on their maximum arity.A full witness may have size |R|^ar(φ), so witness output has a more relaxed time bound than decision.Source: Our Contribution · p. 3

Applications.

  • The metatheorem yields f(td(G)) · |V(G)|-time algorithms for computing stack number, queue number, track number, twin-width, and boxicity.These applications include the graph problems identified as open questions in the introduction.Source: §1 · p. 2, Applications · p. 3

Barriers for Generalizing the Metatheorem.

  • Three proposed generalizations are ruled out unless P = NP: replacing SNP with ESO, parameterizing by pathwidth, and extending to MaxSNP0.The pathwidth barrier includes SNP problems that are NP-hard on graphs of pathwidth 2.Source: Applications · p. 3

2 Technical Overview

This section develops a uniform approach to bounded-treedepth SNP model checking, combining pruning and positive and negative certificates with a Ramsey-based route to pure solutions. It outlines the resulting algorithm with computable bounds and its application to graph parameters.

2.1 Extending the Non-Uniform Algorithm

  • Positive certificates address the one-sided failure of obstruction-based pruning: together with negative certificates, they let the uniform algorithm terminate in computable f(φ, td(R))·|R| time.The pruning threshold p is increased until a negative instance is detected or a positive certificate appears; the runtime function is computable, though no closed-form bound is known.Source: §2.1 · pp. 5–6

2.2 Certificates for Positive Instances

  • Normalized p-routes define boundedly many tuple patterns that capture witness-relevant distinctions; p-purity assigns one solution type to each pattern, yielding bounded-size certificate descriptions.Naive vertex p-types can fail to distinguish tuples that behave differently under a witness, as in the total-order example on a star.Source: §2.2 · pp. 7–10

2.3 Extending Pure Solutions

  • For p ≥ |φ|·h, any p-pure solution of Rp extends to a solution of R; after f(p)·|R| preprocessing, membership in an arity-a witness relation is decidable in O(ah log(ah)) time.Source: §2.3 · p. 10, §4.2 · p. 29
  • p-purity lets the transfer argument preserve relevant relational atoms, so a forbidden tuple in the transferred solution would yield the same forbidden substructure in the original solution.The proof compares tuples with matching p-route patterns and uses purity to establish that their solution types agree.Source: §2.3 · p. 11

2.4 Obtaining Pure Solutions

  • For s ≥ p ≥ M, R satisfies φ exactly when its s-multiplicity structure Rs does; if p ≥ max{M, |φ|h}, satisfaction in R guarantees a p-pure solution on Rp.Ramsey-coloring tuples by solution type and pruning to a monochromatic index set yields purity across route patterns; the resulting large Ramsey structure is existential and is never constructed by the algorithm.Source: §2.4 · pp. 11–13

2.5 The Algorithm A

  • Algorithm A tests increasing p-multiplicity structures, rejecting when no solution exists and accepting when it finds a p-pure solution.It terminates by p ≤ max{M, |φ|(td(R)+1)}; Theorem 9 makes the obstruction set, and thus the iteration bound, computable from the formula and treedepth.Source: §2.5 · p. 13
  • Retaining the pure solution lets Algorithm A construct a witness for positive instances by extending it over tuples of R.Theorem 6 supplies the extension, and the computable bound on p supports the stated constructive part of Theorem A.Source: §2.5 · p. 14

2.6 Applications

  • A formula for stack number yields an algorithm running in f(td(G)) · |V(G)|, since graphs of treedepth at most k have stack number at most k.The formula encodes a vertex order, page assignments, and absence of crossings using forbidden substructures on at most four elements.Source: §2.6 · p. 14
  • The metatheorem gives treedepth-parameterized FPT algorithms for deciding whether a graph’s queue number, track number, twin-width, or boxicity is at most k.The overview notes that the twin-width formula is substantially more involved than the stack-number formula.Source: §2.6 · pp. 14–15

3 Preliminaries

The preliminaries define relational structures and treedepth, then set up SNP sentences and the decision problem parameterized by treedepth and formula length. They also establish atomic types and the induced-substructure property used in the paper.

Relational structures

  • The primal (Gaifman) graph connects elements that occur together in a relation tuple, and the size of a structure counts its domain elements and relation tuples.The structure's arity is the maximum relation arity; zero-arity relations can be replaced by unary relations without changing the primal graph.Source: §3 · p. 15

Atomic types

  • An atomic type records which atomic formulas over a tuple's variables hold, and tuples of length z have at most 2^(z^2 + Σ_i z^ar(E_i)) possible atomic types.The count follows because there are z^2 equality formulas and z^ar(E_i) formulas for each relation E_i, and a type is determined by a subset of these formulas.Source: §3 · p. 16

SNP

  • An SNP sentence existentially quantifies relations before universally quantifying elements, with a quantifier-free inner formula; its solutions are relation assignments satisfying that formula.A Q-solution is the projection of a full solution onto the relation variables indexed by Q.Source: §3 · pp. 16–17
  • SNP satisfaction is preserved under induced substructures: if a structure satisfies an SNP sentence, every induced substructure also satisfies it.An induced substructure keeps exactly the relation tuples whose entries all belong to its selected domain.Source: §3 · pp. 15–16

Problem definition

  • The decision problem asks whether R satisfies φ, with td(R) + |φ| as its parameter; the formula length sums the arities of its atom occurrences.The paper assumes the input structure and sentence have matching signatures and that the structure uses no relations absent from the sentence.Source: §3 · pp. 16–17

Treedepth

  • Treedepth is the minimum height of a rooted forest whose closure contains the graph, and td(R) is measured on the structure's primal graph.A decomposition of height at most td(G)+1 can be computed in time 2^O(td(G)^2) · |V(G)| using the algorithm of Reidl, Rossmanith, Sánchez Villaamil, and Sikdar [RRSS14].Source: §3 · p. 17

4 Formally Proving the Metatheorem

This section proves the metatheorem by developing bounded route-pattern and multiplicity structures, then using purity and finite obstruction sets to preserve satisfaction and obtain pure solutions. These ingredients establish a terminating model-checking algorithm with computable bounds and witness construction.

4 Formally Proving the Metatheorem

  • Q-solutions let the algorithm output only relations of interest, excluding auxiliary relations used to encode the problem as an SNP sentence.The size dependence is governed by the maximum arity among the requested relations.Source: §4 · p. 17
  • Algorithm A decides whether R satisfies φ in time f(|φ|, td(R)) · |R| and, when it does, outputs any requested Q-solution in time f(|φ|, td(R)) · |R|^max_{i∈Q} ar(R_i).The function f is computable, and Q must be non-empty.Source: §4 · p. 18

4.1 Types, Patterns, and Basic Properties

  • A vertex p-type records its ancestor label and subtree label, which capture its interaction with input relations and counts of child types capped at p.A subtree-label value ⋆ marks a child type that occurs at least p times.Source: §4.1 · p. 18
  • The number of distinct vertex p-types is bounded by a computable function of treedepth h, threshold p, and formula length |φ|.This bounds the types needed for an SNP model-checking instance.Source: §4.1 · p. 19
  • A tuple’s p-route pattern normalizes the routes of its entries, enabling tuples in one class to behave alike with respect to forbidden patterns.The method uses relative order among route indices rather than retaining their exact values.Source: §4.1 · pp. 20–22
  • A p-route identifies a vertex by the types along its root path and each vertex’s index among same-type siblings.The fixed total order on vertices determines those sibling indices.Source: §4.1 · p. 20
  • All vertex p-types and p-routes can be computed in time f(h, p, |φ|) · |R|.The construction computes ancestor labels top-down and subtree labels bottom-up, then assigns route indices among same-type siblings.Source: §4.1 · pp. 20–21
  • Normalization preserves route lengths and vertex types, bounds abundant-entry indices by |S|(h−1), and leaves non-abundant entries unchanged.Here S is the finite set of routes being normalized, each of length at most h.Source: §4.1 · p. 22
  • Tuples sharing a p-route pattern have matching depths, ancestor relationships, and atomic types, and corresponding subtuples also share a pattern.The subtuple property applies even when positions are repeated or reordered.Source: §4.1 · p. 23
  • At most f(h, p, |φ|, z) distinct p-route patterns occur for z-tuples, and candidates containing every such pattern can be computed within that bound.The candidate list can be enumerated from the vertex p-types occurring in the structure.Source: §4.1 · p. 24
  • When p ≥ z · h, every p-route pattern of a z-tuple has unique realizing vertices whose pattern is the original one.Every entry index in a realizing vertex’s p-route is at most p.Source: §4.1 · p. 25
  • An s-multiplicity structure prunes excess entries and copies subtrees so each abundant child type has exactly s children.The construction processes vertices bottom-up and keeps s ≥ p.Source: §4.1 · pp. 25–26
  • The multiplicity structure retains treedepth height, retained-element relations, and vertex p-types, while giving each abundant child type exactly s children.For non-abundant types, child counts match those of the corresponding original vertex.Source: §4.1 · p. 26
  • For p ≥ z · h, pruning to Rp preserves every z-tuple’s pattern, retains its realizing vertices, and preserves exactly which patterns occur.Source: §4.1 · p. 26
  • For an SNP Model Checking instance with p ≥ |φ|, the s-multiplicity structure has size at most f(h, p, s).Source: §4.1 · p. 27
  • The reduced structure R_s has size bounded by a computable function of h, p, and s.Its tree has bounded branching and height, and its relation tuples are bounded accordingly.Source: §4.1 · p. 28
  • A p-pure solution requires tuples with the same p-route pattern to have the same solution type, making purity the central ingredient of the algorithm.Purity applies to all tuple lengths up to |φ|.Source: §4.1 · pp. 28–29

4.2 Extending Pure Solutions

  • If p ≥ |φ|·h and R_p has a p-pure solution, that solution extends to R after f(p)·|R| preprocessing, with relation membership queries taking O(a h log(a h)) time for arity a.The query bound applies to each solution relation R_i.Source: §4.2 · p. 29
  • The extension defines relation membership using realizing tuples for p-route patterns, with p-purity ensuring that corresponding solution tuples agree.The proof preserves the truth of formula atoms across the input and reduced structures.Source: §4.2 · pp. 29–30

4.3 Pure Solutions Exist

  • For fixed h and φ, the obstruction set is finite because its minimal non-models form an antichain under induced substructure among bounded-treedepth structures.A well-quasi-order admits no infinite antichain.Source: §4.3 · p. 31
  • Once p exceeds obstruction sizes, R_s satisfies φ for every s ≥ p, since R and R_s have identical induced substructures of size at most p.The equivalence holds for any relational structure W on at most p elements.Source: §4.3 · p. 32
  • For s ≥ p ≥ M, R satisfies φ if and only if its s-multiplicity structure satisfies φ.The proof transfers bounded obstructions in either direction using induced copies.Source: §4.3 · p. 33
  • Each p-route pattern with β distinct abundant indices has a unique realization for every strictly increasing β-tuple from [s], and every matching tuple arises this way.This correspondence identifies tuples by their abundant indices, enabling the Ramsey coloring argument.Source: §4.3 · p. 33
  • For p ≥ max{M, |φ| h}, every positive instance has a p-pure solution on its p-multiplicity structure.Purity means tuples sharing a bounded-length p-route pattern have the same solution type.Source: §4.3 · pp. 34, 36
  • Nested hypergraph Ramsey refinements make solution types uniform across realizations of each short p-route pattern while retaining enough abundant children.An induced embedding into a larger multiplicity structure then transfers its solution back to a p-pure solution.Source: §4.3 · pp. 34–36

4.4 Combining Everything: The Algorithm

  • Theorem 1 gives a computable-time algorithm deciding SNP model checking in f(|φ|, td(R)) · |R| time and outputting Q-solutions in f(|φ|, td(R)) · |R|^max_{i∈Q} ar(R_i) time.The witness-output guarantee applies when R |= φ and Q is any non-empty subset of the relation variables.Source: §4.4 · p. 36
  • Algorithm A terminates correctly by p = max{M, |φ| (td(R)+1)}, deciding negative instances from an empty solution set and positive ones from a p-pure solution.The latter extends to a solution for R when p ≥ |φ|·h; the former follows from induced-substructure closure and the multiplicity-structure equivalence.Source: §4.4 · p. 37
  • Theorem 9 computes the obstruction set J_{h,φ} up to isomorphism in time f(h, |φ|) for a computable function f.Its procedure enumerates bounded-size structures and increases p until each has either no solution or a p-pure solution.Source: §4.4 · p. 38
  • Pφ terminates because its finite obstruction sets depend only on h and φ, so eventually each considered positive structure has a p-pure solution for some pφ.All other considered structures are no-instances, with empty solution sets.Source: §4.4 · p. 38
  • At termination, enumerating minimal no-instances among structures X with X^pφ = X recovers Jh,φ up to isomorphism.The proof uses minimality of obstructions and shows that a proper pφ-reduction would imply the obstruction satisfies φ, a contradiction.Source: §4.4 · pp. 38–39
  • Theorem 9 bounds obstruction sizes by a computable function of h and |φ|, although it does not provide an explicit value for that bound.The bound is obtained by maximizing over formulas of the same length, whose equivalence classes and renamings can be enumerated.Source: §4.4 · p. 39
  • Algorithm A decides in f1(|φ|, td(R))·|R| time and constructs Q-solutions in f2(|φ|, td(R))·|R|^max_{i∈Q} ar(R_i) time, for computable f1 and f2.The computable f2 incorporates the decision bound f1.Source: §4.4 · p. 40

4.5 Comparison with Kolaitis and Vardi

  • Unlike Kolaitis and Vardi’s canonical solutions [KV87, Section 5], pure solutions can distinguish vertices with the same ordered atomic type, as required even for K2 2-colorability.A canonical solution would assign the same color to both vertices of K2, so Theorem 8 cannot hold for canonical solutions in this setting.Source: §4.5 · pp. 40–41
  • Kolaitis and Vardi’s setting asks whether φ holds on every structure [KV87, Theorem 11], whereas this algorithm must decide φ on a given R and preserve its input structure during the Ramsey step.The step uses a common integer index set and encodes tuples with fixed p-route patterns as integer subsets.Source: §4.5 · pp. 40–41
  • The uniform search avoids constructing the large Ramsey structure or knowing M in advance, using Theorem 9 to bound the search and Theorem 6 to reconstruct witnesses on the input domain.It searches for either a negative certificate or a p-pure solution.Source: §4.5 · p. 41

5 Applying the Metatheorem

The section applies the metatheorem to graph parameters by encoding threshold properties in SNP or Strict NP and using treedepth to obtain parameterized algorithms. It covers stack, queue, and track number, twin-width, and boxicity, and describes relational encodings for these parameters.

5 Applying the Metatheorem

  • A computable SNP encoding of size bounded by k, together with a computable treedepth bound on the parameter, yields treedepth-FPT threshold testing and exact computation in time f(td(G)) · |G|.The generic deduction applies when the threshold sentence is computable from k and its arity is bounded.Source: §5 · pp. 41–42

5.1 Stack and Queue Layouts

  • Stack number and queue number are treedepth-FPT to decide and compute, using SNP sentences of length O(k) that encode their respective page-layout conditions.The paper presents these treedepth results as resolving an open question for both parameters.Source: §5.1 · pp. 43–44

5.2 Track Layouts

  • For graph G and t ∈ N, deciding tn(G) ≤ t is fixed-parameter tractable with respect to td(G), and tn(G) can be computed in time f(td(G)) · |G| for computable f.For every t ≥ 1, an SNP sentence has t + 1 existentially quantified relation symbols of arity at most 2, four first-order variables, and length O(t²). Its conditions include partitioning V into independent sets and forbidding X-crossings between distinct tracks.Source: §5.2 · pp. 45–46

5.3 Twin-Width

  • Twin-width thresholds are characterized by computable SNP sentences with two arity-4 relations and length O(k^2), encoding contraction sequences through a relation that orders pairs of vertex-pairs.This representation records when vertex pairs first join, so the sequence cannot stop before all pairs are joined; the supplied passages do not give the resulting algorithmic corollary.Source: §5.3 · pp. 47–48
  • The twin-width encoding uses an ordered merge relation and a red-adjacency relation, enforcing one merge per step and at most k red-adjacent parts in a sentence of length O(k^2).Source: §5.3 · pp. 48–49
  • Deciding whether tww(G) ≤ k is fixed-parameter tractable with respect to td(G), and tww(G) can be computed in time f(td(G)) · |G| for computable f.Source: §5.3 · p. 50

5.4 Boxicity

  • Boxicity at most d is expressed by an SNP sentence using 2d existential binary relations, three first-order variables, and length O(d), computable in polynomial time in d.The relations encode d interval graphs and their interval orders, whose intersection is the input graph.Source: §5.4 · pp. 51–52
  • Deciding whether box(G) ≤ d is fixed-parameter tractable with respect to td(G), and box(G) can be computed in time f(td(G)) · |G| for computable f.Source: §5.4 · p. 52

6 Barriers for Generalizing the Metatheorem

Assuming P ≠ NP, the section rules out three natural extensions: replacing treedepth with pathwidth, allowing ESO formulas, and applying the metatheorem to MaxSNP. The barriers include NP-completeness at treedepth at most 2 for fixed ESO and MaxSNP formulations.

6.1 Pathwidth

  • Queue number at most one is expressible by a constant-length SNP sentence but NP-hard at constant pathwidth, ruling out a pathwidth replacement unless P = NP.The question is motivated by treewidth-based model-checking results.Source: §6.1 · p. 53

6.2 More Expressive Formulas

  • A fixed ESO sentence defines an NP-complete problem even on graphs of treedepth at most 2.The reduction encodes 3-Partition integers as star sizes and uses a star forest.Source: §6.2 · p. 53

6.3 MaxSNP

  • MaxSNP0 maximizes the number of tuples satisfying a quantifier-free formula, unlike SNP’s requirement that every tuple satisfy it; parameterizing by treedepth does not inherit the stated guarantees for the natural parameter p.The section gives NP-completeness even for treedepth at most 2.Source: §6.3 · p. 54
  • A fixed quantifier-free formula with a binary relation and 10 tuple variables yields an NP-complete decision problem even when td(R) ≤ 2.The reduction represents item sizes by stars and bins by vertices, with the relation assigning star vertices to bins.Source: §6.3 · p. 54
  • The assignment constraints require each star to be assigned wholly to one bin or not assigned, while the Even formula rewards assignments spread evenly across bins.The number of tuples satisfying Even is maximized when all vertices are assigned and each bin receives the same number.Source: §6.3 · pp. 54–55
  • A valid Exact Bin Packing partition constructs an assignment meeting the tuple threshold, completing the reduction’s forward direction.The assignment places every vertex of a star in the bin corresponding to its item’s partition set.Source: §6.3 · p. 55
  • One violated assignment constraint loses |V(R)|^5 satisfying tuples, making the threshold unattainable and forcing every 4-tuple to meet the constraints.At the threshold, equality forces all star vertices to be assigned and the bin loads to match the exact packing target.Source: §6.3 · p. 56

AI Methodology

The authors used language models to help develop examples and proofs and to support writing and proofreading. They state that they checked the paper’s correctness and take full responsibility for it.

AI Methodology

  • GPT-5.6 Sol helped find an FPT proof for stack number parameterized by treedepth and prompted exploration of generalizations; the authors wrote the main SNP model-checking proofs.The authors say those proofs go beyond the stack-number proof provided by GPT.Source: AI Methodology · p. 56
  • GPT-5.6 Sol helped identify Boxicity as an additional example application, while GPT-5.6 Sol and GPT-6 Astra searched for a problem witnessing non-extendability, leading to Theorem 53.GPT-6 Astra was used to obtain Theorem 54’s result.Source: AI Methodology · p. 56
  • Language models also assisted with proofreading, writing, literature searches, and figure creation; the authors checked correctness and accept responsibility.Source: AI Methodology · pp. 56–57
Loading 2610.06561v1…