SAT dynamics: small summaries, shared updates and unique certificates

5 October 2026 · Primary-literature assessment

The question is which ordinary constraint languages admit native scaffolding recognition. A useful next candidate is stronger than the established small-cover construction:

Bounded-treedepth candidate. For every fixed nonempty finite domain $D$, finite unary/binary constraint language $\Gamma$, and fixed $d$, one native deterministic scaffolding automaton recognizes exactly the well-formed satisfiable instances whose loopless primal graph has treedepth at most $d$.

Here treedepth is the minimum height of a rooted forest in which each graph edge joins an ancestor and descendant. The forest is not supplied. Names are literal nonempty binary words; constraints arrive in arbitrary order, including late pins. Malformed words reject. Every distinct-name binary record contributes an edge, even a full relation. Constants may depend on $D,\Gamma,d$, never input length $N$. The machine has fixed degree, radius and finite labels, fixed initialization, immutable old nodes and the strict final-symbol deadline. This is a conjecture, not a consequence of a general polynomial-time algorithm.

It would extend native recognition from a bounded total set of influential variables to arbitrarily many interacting pieces. The review supports this as a serious positive target, while identifying the exact missing operation.

What the dynamic structural proofs actually provide

Dvořák, Kupec and Tůma, §2, especially §§2.1–2.4, maintain compressed bounded-depth decompositions. Equivalent branches share a cabinet; a drawer groups vertices with one parent. Extracting a root-to-vertex path exposes only boundedly many types. Rerooting reorganizes these types. Crucially, vertices in a drawer reach their common parent through a shared pointer that can be overwritten. The proof’s small update count uses this collective change; it does not visit every vertex in the drawer.

Chen and coauthors, §§7–8, sharpen this method using bounded cores. Section7’s structure stores one mutable parent cell per bucket. Algorithms3–4 redirect whole buckets when trimming and extending the decomposition. The model has single-word vertex identifiers and an initialized vertex universe. Section8 adds composable finite configurations, with a precise pointwise redundancy condition. These are strong dynamic algorithms, but a native literal-name dictionary does not supply their mutable shared cells.

Assessment: finite structural summaries are available. The outstanding native issue is keeping old references consistent when a whole group acquires a new parent. Copying a parent cell leaves old references pointing to its previous contents; rewriting every incoming reference can cost arbitrarily much. This is a failure of that direct translation, not a lower bound against every representation.

The strongest next test is therefore a native construction for bounded-treedepth constraint insertion that handles repeated regrouping and immediate short-name queries. A successful construction must explain how it avoids shared-cell rewriting, rather than merely replace a mutable container by a persistent one.

A small but necessary algebraic check

For a fragment with boundary $X$, let $F\subseteq D^X$ contain the boundary assignments that cannot extend to a satisfying assignment. For fragments sharing only their boundaries, lift their forbidden assignments to the combined boundary and take union. When forgetting $x\in X$, use

$$F'=\{a\in D^{X\setminus\{x\}}:\ \forall z\in D,\ a[x\mapsto z]\in F\}.$$

These equations follow directly from independent extension of the two interiors. For fixed boundary size they are finite tables. At empty boundary, the empty assignment belongs to $F$ exactly when the instance is unsatisfiable.

Union also satisfies the reviewed configuration scheme’s pointwise redundancy condition with threshold one: if every forbidden assignment contributed by a fragment already occurs in another fragment, deleting it changes nothing. Using feasible assignments with intersection would fail that particular condition. For example, $\{0\}$ contributes an essential restriction despite its sole element occurring in arbitrarily many copies of $\{0,1\}$.

This also completes a mutable control. For fixed $D,\Gamma,d$, the ordinary record stream can be processed by a deterministic mutable word-RAM in $O_{D,\Gamma,d}(N)$ total work and allocation, with a bounded batch at each delimiter, checking both satisfiability and treedepth at most $d$. Store each vertex’s unary mask and each present edge’s finite relation label. A label update changes only constraints inside a core containing its endpoints, so the trim/extend and configuration proofs still apply; a new edge uses the depth-violation test. A mutable binary-name trie supplies endpoints as their names arrive; first occurrences add isolated vertex records. Words contain $O(\log(N+2))$ bits, and old writes and pointer equality are permitted. These are checked adaptations of the structural algorithm, not a new dynamic decomposition technique.

The missing native step is therefore shared-reference maintenance, rather than finite-state CSP semantics or a linear total-work bound.

Minimal stored information does not determine native recognition

Sharma and Velusamy, Theorems1.1 and3.1, §§3–4, characterize single-pass exact CSP satisfiability memory, up to a logarithmic factor, by non-redundancy. This parameter is the largest number of constraints for which deleting any one enlarges the solution set. The shifted finite-domain theorem and the non-constant-satisfiable positive Boolean theorem have different hypotheses. Their upper bound repeatedly removes redundant constraints, permitting exhaustive assignment searches and final computation. Their lower bound sends the streaming state in a one-way INDEX protocol; a witness-specific suffix isolates the selected constraint. Thus the theorem measures information storage, with no native update deadline.

Our existing positive and negative controls give a precise comparison. Write $\operatorname{NRD}_n$ for this parameter on $n$ variables. For Boolean unary pins it is $\Theta(n)$. For equality with pins, and for ternary parity equations with pins, it is also $\Theta(n)$.

The affine calculation is elementary. In a satisfiable irredundant system, the equation rows are independent, so there are at most $n$. In an unsatisfiable irredundant system, deleting any equation restores consistency; its rows form a minimal inconsistent dependency, giving at most $n+1$ equations. Independent unary pins supply the linear lower bound. This argument concerns scalar equations; it does not silently replace an arbitrary relation by several atoms while preserving the parameter.

Consequently linear non-redundancy cannot characterize native recognition. This is a synthesis of the streaming theorem, elementary linear algebra and our completed native controls, not a new lower-bound technique.

The resource comparison also matters. With logarithmic-length identifiers, a fixed-arity record takes $O(\log n)$ symbols and an irredundant kernel uses $O(n\log n)$ bits in these examples. In our ordinary encoding, $N$ counts every actual name and delimiter, and names need not have logarithmic length. A native run retains $O(N)$ nodes and $O(N\log(N+2))$ explicit pointer bits, including history. A memory lower bound of $\Omega(n)$ is compatible with that allowance. The separating question is whether the information can be maintained and consulted before the last symbol.

Where the unique-certificate result sits in prior work

The complete Kim–Park paper is now available for comparison. Its witness and §5 already establish PEG homomorphism nonclosure through a marked factorization. The displayed grammar permits multiple witnessing records; duplicate matching records demonstrate that its particular witness selection is not unambiguous. Length preservation alone adds little: decorate a record delimiter instead of inserting and erasing a separate marker, using their inverse-homomorphism closure.

A direct extension using our existing native seen-key dictionary restricts their records to distinct keys. Guess one record, retain its key and payload in immutable stacks, and check them against the final query. Distinct keys permit at most one successful choice; their canonical hard inputs already have distinct keys. A bit at the chosen record’s opening symbol turns this into a unique letterwise certificate. All other hint bits are zero. The general separation and joint unique, length-preserving projection phenomenon therefore have a short route from that known witness plus the dictionary.

The appropriate classification of our late-value circuit result is an extension and SAT-dynamics application, with high confidence about this overlap. Its useful added content is the ordinary ordered circuit language, globally checked eventual source pins, and the early-value/late-value/verified-replay comparison. It should not be presented as a new general separation method.

A second comparison explains why erasure must be distinguished from letterwise projection. Loff–Moreira–Reis, Theorem18, provides a padding construction for computable functions. Combined with Boolean closure and Rubtsov–Chudinov, Lemma15, it gives a unique erasing representation of any decidable binary language: retain only its shortest accepted padding. More explicitly, choose $f(x)=\varepsilon$ on $A$ and $f(x)=1$ otherwise, and intersect the resulting padded language with $\$^+\{0,1\}^*$. Then $H_0=\{\$^\ell x:x\in A,\ell\ge \max(1,g(x))\}$ is PEG, and $H_0\setminus\$H_0$ contains exactly one padded word per $x\in A$. Erasing padding is bijective. This is a consequence of those existing results; padding supplies computation time that the letterwise circuit certificate does not.

Research priorities justified by the comparison

1. Test the bounded-treedepth candidate through an explicit immutable regrouping invariant. Charge names, historical references, all allocation and immediate final queries. Do not import a mutable constant-update theorem as native.
2. Keep unrestricted equality as the central unresolved affine case. A structural positive would teach more than another attempt to compress its already-small semantic information.
3. Use the existing parity and propagation exclusions as hostile controls for proposed positive mechanisms. Any proposal based only on small kernels or finite boundary tables misses the demonstrated distinction.
4. Keep unique certificates and verified replay as explanatory dynamics controls. Further closure refinements are lower priority than a new natural-family construction or obstruction.

This review establishes no new native SAT membership or nonmembership theorem. The checked mutable control identifies the concrete structural construction worth attempting, rules out a storage-only characterization, and replaces an unresolved attribution question with a source-backed assessment.