旧结果只保证算法存在却无法构造
对于有界树深的图，诱导子图下的良序关系保证 Strict NP 中的每个问题都存在线性时间算法。这一保证真实但很单薄。它说明对每个固定语句和每个固定树深上界都存在算法，却没有给出从语句和上界构造该算法的过程，没有给出运行时间对这两个输入的依赖的可计算界，也无法输出使正实例为正的见证关系。
在参数化复杂性中，这类算法被称为非一致固定参数算法。它们不是通常意义上的固定参数算法，因为固定参数可解性要求对公式长度和树深的依赖由可计算函数界定。论文的目标正是填补这一缺口：把存在性陈述转化为一个对所有 Strict NP 语句同时成立的算法。
一个算法覆盖所有 Strict NP 语句
主要结果以简化形式表述为定理 A：存在算法 A，输入 Strict NP 语句 φ 和关系结构 R，判定 R ⊨ φ，并在时间 f(|φ|, td(R)) · |R| 内运行，其中 f 可计算。这里 |R| 是输入结构的编码大小，td(R) 是其 Gaifman 图的树深，多项式次数不依赖于 φ。
有两点使这一结果区别于早先的保证。第一，算法是统一的：单一过程处理所有语句，而不是对每个语句和上界各有一个未指定的算法。第二，它是可构造的，且不要求把禁子结构刻画作为输入的一部分。Gaifman 图这一细节很重要，因为树深并非直接从输入关系读出，而是在以元素为顶点、以在同一输入关系元组中共现的元素为边的图上度量。
输出见证比判定是非代价更高
判定与见证是两项不同的保证，运行时间也不同。若 R ⊨ φ，算法可在时间 f(|φ|, td(R)) · |R|^ar(φ) 内输出见证，其中 ar(φ) 是存在量化关系 R1, …, Rr 中任一关系的最大元数。因此指数取决于该元数，见证的大小可达 |R|^ar(φ)。
这是一个有意义的区别，而非技术细节。Strict NP 与一元二阶逻辑的差别恰恰在于存在量化的关系可以有任意大的元数：见证可以包含整个域上的线性序，或描述多个顶点之间交互的高元数关系，而且即使输入结构稀疏，见证关系也可能是稠密的。论文定理 1 中更细粒度的陈述允许算法输出所请求的见证关系的任意子集，多项式指数只取决于这些被请求关系的最大元数。
剪枝加正实例证书替代缺失的界
证明策略从剪枝思想出发。固定 φ 和树深上界 h。存在有限禁子结构集 J(h, φ)，使得树深至多 h 的结构满足 φ 当且仅当它不包含 J(h, φ) 中任何成员作为诱导子结构。利用消去森林上的类型，可以把 R 剪枝为诱导子结构 R_p，其大小由可计算函数 g(p, h) 界定，同时保持 R 是否包含大小至多 p 的诱导子结构这一性质。
如果有一个预言机给出 J(h, φ) 中最大禁子结构的大小 M，那么取 p = M 就能使 R_p ⊨ φ 与 R ⊨ φ 等价，对大小有界的 R_p 暴力枚举即可判定实例。问题在于 M 未知。增大 p 对负实例有效，因为有限禁子结构终会被发现，但正实例没有终止判据。论文的关键一步是定义正实例证书，它们能在大小有界的剪枝实例上被识别，并扩展到原始输入。算法从只依赖 φ 和 td(R) 的阈值开始，逐步增大 p，对每个 p 检查是否 R_p ⊭ φ（输出否），或 R_p 是否具有正实例证书（输出是）。
运行时间界为何没有闭式表达
函数 f 可计算，但没有给出闭式形式。它的取值取决于 J(h, φ) 中最大禁子结构的大小，而论文对此没有显式界。证明通过一个具体且非平凡的过程确立可计算性，该过程构造 f 并保证终止，但不给出其增长的闭式上界。
这是对结果如何定量使用的限制，而非对其正确性的限制。读者在把这一元定理与 Courcelle 型结果比较时应注意，这里的保证是参数依赖的统一性和可计算性，而不是紧致或显式的运行时间表达式。论文还指出，正实例证书提供了把 R_p ⊨ φ 的见证扩展为 R ⊨ φ 的见证的方法。
应用解决了树深参数化的开放问题
该元定理给出计算图 G 的 stack number、queue number、track number、twin-width 和 boxicity 的 f(td(G)) · |V(G)| 时间算法。论文指出，这解决了以树深为参数计算 stack number、queue number、track number 和 twin-width 的固定参数可解性这一开放问题，这些问题即使在近期工作中也被明确列为开放问题。
这些应用正是统一性主张的价值所在。论文报告称，某些 Strict NP 问题在路径宽为 2 的图上已是 NP 难，因此在 P ≠ NP 的前提下，它们的可解性无法从适用于有界路径宽图类的元定理推出。与 Courcelle 定理的这一对比是问题本身的性质，而不是算法的缺陷。
三种自然推广在 P = NP 前均不成立
论文排除了三种扩展。在保持对树深可解的前提下，Strict NP 公式不能被 ESO 公式替换，这一点用 Fagin 定理证明。结果不能推广到路径宽，因为存在在路径宽为 2 的图上 NP 难的 Strict NP 问题。向 MaxSNP0（Strict NP 的自然优化变体）的推广同样被排除。
这些障碍界定了元定理的边界。相关的适用范围条件是树深在 Gaifman 图上度量，以及 Strict NP 语法内置的诱导子结构封闭性：满足性在取诱导子结构下保持，这正是禁子结构论证适用的原因。非遗传的性质，例如 Hamiltonian Cycle，落在这一逻辑之外，而由 MSO2 刻画。
应用元定理时该关注什么
论文中最具决策意义的分野是判定与见证之别。如果目标是对有界树深结构上某个固定 Strict NP 语句给出是非答案，保证是 f(|φ|, td(R)) · |R|，多项式次数不依赖于 φ。如果目标是显式见证，界变为 f(|φ|, td(R)) · |R|^ar(φ)，指数随所请求见证关系的元数变化。
第二个分野是树深与路径宽之别。对 stack number、queue number、track number、twin-width 和 boxicity 的应用都以树深为参数，而论文关于路径宽为 2 的难解性观察表明这不是证明技巧的产物。读者在权衡元定理是否适用于某个遗传图问题时，应检查该问题是否可在 Strict NP 中表达，以及参数是否为 Gaifman 图上的树深，而非路径宽或树宽。可计算但无闭式的 f 是统一性的代价，也正是论文的保证相对于它所取代的经典存在性结果最强之处。
本文引用的文献
A Uniform Algorithm for Strict NP on Bounded-Treedepth Graphs
单一、统一且可构造的固定参数算法在时间 f(|φ|, td(R)) · |R| 内判定有界树深关系结构上的每个 Strict NP 语句，其中 f 可计算；在时间 f(|φ|, td(R)) · |R|^ar(φ) 内输出见证；并解决了以树深为参数计算 stack number、queue number、track number 和 twin-width 的固定参数可解性这一开放问题。