SAT families inside scaffolding automata

Research review · 4 October 2026

Subsequent results. The propagation and replay investigation gives unconditional native exclusions for implication and every Boolean gate depending essentially on at least two inputs. It also exhibits a nonnative ordered XOR-circuit language whose verified two-copy version is native, with a corresponding PEG separation. The parity theorem and the OMv-conditional 2-affine necessary condition remain in force. Equality/disequality recognition and algebraic invariance remain unresolved; a sharp query minimum closes one proposed matrix route. The four-paper review below is preserved as the original baseline; its initial status statements describe that earlier assessment.

Which natural Boolean constraint problems can scaffolding automata solve on their ordinary written input? A strong answer would classify constraint languages by a structural property, with implementations on one side and an obstruction applying to every native automaton on the other. No such classification is established here.

The literature suggests a sharper first question than simply asking whether the classical easy cases remain easy:

Can native scaffolding automata recognize consistency of arbitrarily ordered equality constraints with variables pinned to 0 or 1?

For example, $x=y,\ y=z,\ x=1,\ z=0$ is inconsistent. Removing either equality makes it consistent. The problem asks whether contradictory pins become connected through equality edges. It involves no search over assignments, yet already tests global coordination.

This review connects four primary papers. Its outcome is a research direction, a rigorous limitation on reduction-based reasoning, and an exact bridge to undirected connectivity. It does not establish a new SAT upper bound or a natural language outside scaffolding automata.

One recognition contract

Fix a finite language of nonempty Boolean relations of positive arity $\Gamma$, with a fixed token and arity for each relation. A formula is a sequence of records such as “T(101);E(101,11);F(11);”. Names are nonempty binary words, compared literally; leading zeros do not denote the same name. Relation tokens and punctuation belong to a fixed finite alphabet. Record order and repeated arguments are unrestricted. The empty string is the empty conjunction. Malformed strings are rejected. Constants occur only through explicitly included relations, such as $T=\{1\}$ and $F=\{0\}$.

With $m$ records and name occurrences $w_1,\ldots,w_\ell$, the actual encoded length is

$$N=\Theta\!\left(m+\sum_{i=1}^{\ell}|w_i|\right).$$

The number $b$ of distinct variables is at most $N$; it does not replace $N$ as the clock. Any auxiliary variables introduced by a reduction must also be encoded.

Write $\mathrm{SAT}_{\mathrm{enc}}(\Gamma)$ for this language and $\mathsf{SA}$ for native deterministic scaffolding recognition. One fixed automaton, depending on $\Gamma$ but not $N$, handles every input. Control, labels, degree and observation radius are finite constants. Starting from the unlabelled base, each input symbol adds exactly one node. New edges follow bounded port paths from the previous top, are missing, or point to the new node itself. Decisions inspect labelled unfoldings, not physical pointer identity or numerical addresses.

After $N$ symbols there are $N+1$ nodes, or $O(N\log(N+2))$ bits under literal pointer serialization. Acceptance is the final finite-control state. There is no growing initialization, independent preparation, supplied decomposition, padding, external dictionary, randomization or post-input cleanup. The contract is one Boolean recognition answer, not a prepared-fragment query service.

What the four papers supply

These are imported results. The Schaefer alternatives overlap; the finer complexity classes must not be asserted distinct without the corresponding assumptions. Schaefer explicitly counts names as strings on p219 and allows two-way input in the reduction model on p226. Fixed gadget size does not mean free access to arbitrarily long names.

A firm limitation on the reduction method

A classical-method consequence of the native model and the P-complete construction is

$$\mathsf{SA}\subsetneq\mathsf P, \qquad \mathsf{SA}\text{ is not closed under all logspace inverse images.}$$

For each fixed SA, a multitape Turing machine stores its $O(N)$ bounded-degree records using $O(\log(N+2))$-bit indices. Each transition needs a fixed number of record lookups. Scanning the record list implements each lookup, giving a conservative $O(N^2\log(N+2))$, hence cubic, simulation. The constant depends on the automaton; the exponent does not.

For completeness, the standard diagonal argument separates this fixed exponent from P. On an input encoding a machine $M$ followed by arbitrary padding, simulate $M$ on that very input for $n^4$ steps and reverse its answer if it halts; otherwise give a fixed answer. Universal simulation with this cutoff is polynomial. If some machine decided the resulting language in $c n^3$ time, its sufficiently long padded encodings would force it to disagree with itself. Malformed descriptions receive a fixed answer. Thus some P language lies outside SA. This is time-hierarchy reasoning, not a new method or a natural SAT example.

Let $K$ be the P-complete PEG language from Loff–Moreira–Reis. Their equivalence puts $K^R$ in SA. Reversal is logspace computable, so $K^R$ remains P-complete under logspace many-one reductions. Full inverse closure under those reductions would put every P language in SA, contradicting the separation.

Thus a general logspace transfer principle is false, rather than merely unchecked. This does not identify which SAT reductions fail or show that equality consistency is outside SA.

A bridge that preserves the native clock

Written closure consequence. For a deterministic one-way finite-state transducer $f$ with bounded output per input symbol, a fixed initial output and bounded state-dependent final output,

$$L\in\mathsf{SA}\ \Longrightarrow\ f^{-1}(L)\in\mathsf{SA}.$$

Regular source-validity conditions may be included. Constants depend on the transducer and target automaton.

If a source symbol emits at most $C$ target symbols, simulate those at most $C$ target transitions as one bounded batch of logical records. Unrolling the observations keeps every old target within a fixed radius; every fresh target is a specified batch slot. A zero-output transition copies the direct logical-top reference, so erased symbols never accumulate a forwarding chain. No identity test is introduced.

The reviewed simultaneous-record compiler packs such a batch into one physical scaffold node with finite slot tags, degree and radius. The target computation on the fixed initial output is a fixed finite virtual initial graph, handled by the compiler’s initialization clause.

Final output requires no cleanup. After every source symbol, also calculate what target acceptance would be if the transducer stopped and emitted its final word now. Its length is bounded, so this requires a bounded view. Store the answer in finite control; do not commit the hypothetical records to the continuing computation. On another input symbol continue from the real target state. The empty-input answer is a constant.

This covers erasure, final output, native initialization and ordinary termination, with all physical allocation charged to input symbols. It is a written specialization of the existing compiler, independently reviewed here, with no novelty or new formal-verification claim. It needs no deque or dictionary premise.

Equality consistency is a native connectivity test

Consider

$$\Gamma_{\mathrm{pin}}=\{T,F\},\qquad \Gamma_{\mathrm{eq}}=\{T,F,E\},\quad E=\{(0,0),(1,1)\}.$$

Both have exactly the idempotent Boolean operations as polymorphisms: preserving pins means preserving all-0 and all-1 tuples, while every operation preserves equality. Pins alone ask whether one name receives contradictory values. With equality, satisfiability asks whether any equality component contains opposite pins.

Encode undirected nonreachability by a header “S(s);Z(t);” followed by edge records “E(u,v);”, with the same binary names and regular syntax. From this language to equality consistency, replace the two header tokens by $T,F$, retaining the edge records.

In the reverse direction emit the fixed header “S(10);Z(11);”, prefix every original name by 0, and translate

$$E(u,v)\mapsto E(0u,0v),\quad T(u)\mapsto E(10,0u),\quad F(u)\mapsto E(11,0u).$$

Reserved names 10 and 11 cannot equal a prefixed original name. An anchor-to-anchor path exists exactly when an original equality component has opposite pins. Both translations are one-way finite-state with bounded output per symbol and $N'=O(N+1)$. Source syntax checks reject malformed inputs.

Consequently the closure proof establishes

$$\mathrm{SAT}_{\mathrm{enc}}(\Gamma_{\mathrm{eq}})\in\mathsf{SA} \ \Longleftrightarrow\ \mathrm{UNREACH}_{\mathrm{enc}}\in\mathsf{SA}.$$

Complementing finite control and restricting to valid graph encodings gives the same equivalence with reachability. This is an encoding-specific transfer of the classical graph interpretation, not a connectivity algorithm or lower bound.

The research burden is now concrete: construct a native recognizer for arbitrary edge order, or prove an obstruction covering every native recognizer. Failure of one union-find implementation would establish neither alternative.

The broader gadget-transfer problem

Fixed existential-conjunctive gadgets can preserve linear encoded size. Name each auxiliary by its relation, complete argument tuple and fixed gadget position, using an injective escaped encoding and a namespace distinct from original variables. Identical atoms may share witnesses because they repeat identical conjuncts; different tuples receive distinct auxiliary names. Each name is copied a bounded number of times, so $N'=O(N)$.

This corrects a tempting overstatement: naming auxiliaries by occurrence indices gives $O(N+m\log(m+1))$, but that overhead is not inherent.

The linear-size construction still copies and reorders unbounded argument strings. A two-way finite-state transducer can perform the fixed gadget substitution by a bounded number of scans within each record. The one-way closure proof does not cover those rescans. Total linear transformation time does not itself preserve native per-symbol deadlines.

Furthermore, eliminating equality may identify entire connected components and rewrite variable names—the global step in Allender and coauthors’ Lemma 2.5. It cannot be inserted as free preparation.

A useful stronger compilation statement would therefore cover explicit record-local copying and permutation. Its payoff would be transporting substantial fixed gadgets. It requires an actual simulation, not a definition of “allowed reductions” that already assumes native closure.

Live statements and consequences

A separation between the two pin languages would refute algebraic invariance and the broad native-tractability statement. A positive result for both would leave invariance undecided and justify moving to implication, Horn propagation and parity. Neither outcome is presumed.

Finite duality supplies a second predictor. Pins alone have a bounded contradiction witness; equality paths with opposite endpoint pins have arbitrarily long minimal obstructions. This contrast is not an SA lower bound. Conversely, small witnesses do not make serial lookup free.

For the unary-pin positive control, a locally navigated trie could process one name bit per move, compare or set a terminal pin flag, and reset to its root. The existing finite-rule trie route retains an explicit deque premise. It remains conditional here; no unconditional native membership follows from the published functional data-structure theorem alone.

Priorities and status

The next substantial effort should pursue equality consistency and the corresponding connectivity problem, with unary-name lookup as a positive control. Compare actual constructions and lower-bound models, including two late pins querying a graph supplied earlier. An obstruction that introduces ready external handles, a fixed storage layout or extra routing restrictions addresses a different contract.

The next comparison is directed implication, bounded-arity Horn propagation and bounded-arity affine constraints. Reassess priorities if the equality test undermines their proposed common mechanism. Work on record-local gadget transfer when it would carry one of these substantive results, rather than treating a sequence of closure lemmas as the goal.

Ordinary 3SAT in SA implies $\mathsf P=\mathsf{NP}$ by the polynomial simulation. Ordinary 3SAT outside SA does not imply $\mathsf P\ne\mathsf{NP}$: SA is already strictly inside P. Neither SAT result is claimed. SA recognition of $L$ gives a PEG for $L^R$, with exactly that reversal.

Status: substantive multi-paper assessment; imported classifications; written, independently reviewed reduction consequences. No new SAT recognition theorem, natural SA separation, formal verification or novelty claim. The consequence for research is to test coordination under the native clock instead of importing the classical tractability boundary.

Primary texts and precise locators

• Schaefer, The Complexity of Satisfiability Problems (1978). Primary scan, DOI. Theorem 2.1, Theorem 3.0 and supporting lemmas, Lemmas 4.1–4.3, pp217–223; name encoding p219; reduction model p226. Relevant proof chain read. The finer §5 results are stated there without proof.
• Loff–Moreira–Reis, The computational power of parsing expression grammars (2020). Author full text, version 2. Definitions 10–15, printed pp14–16; Theorem 16 and both constructions, pp21–27; Theorem 18 and Corollary 19, pp27–29. Native rules, reversal and padded simulation checked. Historical open-problem remarks do not establish current open status.
• Allender–Bauland–Immerman–Schnoor–Vollmer, The Complexity of Satisfiability Problems: Refining Schaefer’s Theorem (2009). Author full text. §§2–3; Example 2.4/Lemma 2.5, author-PDF pp8–9; Theorem 3.1/Corollary 3.2 p9; equality and hardness proofs pp11–15; constants §4. Corollary 3.2’s isomorphism proof explicitly uses padding, not a native-clock equivalence.
• Larose–Loten–Tardif, A Characterisation of First-Order Constraint Satisfaction Problems (2007). Primary full text. Theorem 2.5 p6; §4 tolerant powers; §5 dismantling, especially Theorem 5.7 p16; Theorem 7.2 pp18–19; §8 inferred relations. The solution proof gives $O(|B|^{d+2})$ time, maximum arity $d$. The FO/finite-duality equivalence is credited there to prior work; its entire original source chain is not claimed re-proved here.

Polynomial diagonalization is classical. For historical context see Hartmanis–Stearns, On the Computational Complexity of Algorithms, §VI, Definition 6/Theorem 13, pp303–304. Their online recognition convention differs from the ordinary decider above; our explicit argument avoids silently identifying those conventions.

Positive continuation: unary name access is now native

The FIFO-capsule construction establishes native recognition for every fixed finite unary constraint language under the ordinary binary-name encoding. It replaces the conditional unary-pin route above without assuming the deque premise. This is a written, independently audited proof, not a formally verified or novelty claim. Equality recognition remains hypothetical. The polymorphism-invariance candidate now predicts equality membership from a proved pin-language antecedent.

Unary constraints and online tapes

The primary comparison and structural theorem establish a sharper control. All fixed unary families and their reversals have native recognizers. A common value across nonempty relations gives regularity; without one, the ordinary encoding defeats small-delay deterministic online Turing machines. The proof combines a specialized functional-trie realization with a classical information argument. Equality recognition still requires a component-coherence mechanism.

A conditional separation inside tractable SAT

The OMv reduction now gives a conditional negative counterpart to native unary recognition. Under the online matrix-vector multiplication conjecture, positive pins plus NAND have no native scaffold recognizer, in either input orientation. This family is both Horn and bijunctive, and every inconsistency has a witness of at most three records. Broad native Schaefer tractability and the sufficiency of bounded witnesses are therefore conditionally refuted. Equality remains unresolved. The proof is a native-language application of established matrix/independent-set query methodology, with all serialized names, preparation and branching history charged.