A conditional SAT boundary for scaffolding automata

4 October 2026. Written reduction, independently reviewed.

Unary pins restrict variables separately: T(01); forces one variable to be true. Now allow N(01,10);, meaning those two variables cannot both be true. This adds only a negative two-literal clause. Every contradiction can still be witnessed by at most three records: two true pins and one forbidden pair.

Yet this small extension reaches a substantial conditional boundary. Under the online Boolean matrix-vector multiplication conjecture, no native scaffolding automaton recognizes all these satisfiable formulas. The previously established unary recognizer supplies the positive comparison.

The reason is the combination of rapid processing and immutable history. A hypothetical recognizer would let us prepare a matrix once, branch into alternative pin assignments, and answer all the corresponding matrix queries too quickly for that conjecture.

Exact statement and assumption

Let $T=\{1\}$ and $B=\{(0,0),(0,1),(1,0)\}$, the Boolean NAND relation. Write $L_B$ for satisfiability of records T(w); and N(u,v);. Every name is a nonempty literal binary word. Leading zeros matter; names, arguments and records may repeat or occur in arbitrary order. The empty conjunction accepts, and malformed strings reject. The alphabet and the two relation tags are fixed.

The target is one deterministic native scaffolding automaton for all input lengths: fixed finite control, labels, degree and inspection radius; fixed initialization; one immutable node per input symbol; bounded labelled-unfolding observations without physical pointer equality or address arithmetic; acceptance at ordinary input end, with no extra computation. Every name bit and delimiter contributes to actual encoded length $N$.

Reduction theorem. If either $L_B$ or its string reversal has a native scaffold recognizer, Boolean online matrix-vector multiplication on an $n\times n$ matrix and $n$ arriving vectors has a deterministic algorithm taking

$$O(n^2\log(n+2))$$

total word-RAM time and allocated words, including matrix preparation and every abandoned branch. Words have $O(\log(n+2))$ bits. Each product is output before the next vector arrives.

The OMv assumption used here excludes truly subcubic algorithms for this task on the ordinary word RAM with logarithmic-size words. Henzinger, Krinninger, Nanongkai and Saranurak formulate the usual, stronger bounded-error version as Conjecture1.1, printed p3 of their 2015 paper. The reduction is deterministic, so even the deterministic restriction of that assumption suffices.

Conditional separation. Under OMv,

$$L_B\notin\mathsf{SA},\qquad L_B^R\notin\mathsf{SA},$$

whereas ordinary unary Boolean-pin satisfiability belongs to $\mathsf{SA}$. Both $L_B$ orientations are also excluded from PEG recognition by the reversal-sensitive scaffold/PEG equivalence.

The implication from a recognizer to a fast OMv algorithm is proved below without assuming OMv. Nonmembership depends on the conjecture; it is not an unconditional language lower bound.

Why every native representation can be reused

Fix a hypothetical recognizer $A$, of degree $D$ and observation radius $r$. A word-RAM simulator stores each scaffold node as a finite label and $D$ pointers. Reading its entire radius-$r$ unfolding takes a number of RAM accesses depending only on $A$. The finite transition rule and allocation of one new node therefore cost $O_A(1)$ per input symbol.

A configuration is represented by its top-node pointer and finite-control state. Save that pair, process a suffix, and later return to the saved pair to process another suffix. The old records never change. No copying of the prefix graph is required.

The simulator may allocate separate branches in one global heap. On each branch, the allocated records and their port edges reproduce exactly the scaffold that would have been obtained by running that prefix and suffix alone. This follows by induction on the suffix: bounded labelled views agree, and the transition copies the same targets or creates its own self-reference. Gaps in global addresses are unobservable to $A$. There is no hidden history-length, address, or identity channel in the native model.

Thus $H$ actually simulated symbols across all branches require $O_A(H+1)$ time and records, even if no garbage is reclaimed. The simulator charges name generation, input reading, saved configurations and output separately below. This is a consequence of any native recognizer, not an added snapshot operation in the formula language or a restriction to one dictionary presentation.

Encode a matrix using forbidden pairs

Choose $d=\lceil\log_2(n+1)\rceil$. Use distinct $d$-bit encodings of indices $1,\ldots,n$, and give the variables disjoint names

$$\ell_j=0\operatorname{bin}_d(j),\qquad r_i=1\operatorname{bin}_d(i).$$

For a matrix $M\in\{0,1\}^{n\times n}$, prepare the formula prefix

$$P_M=\bigwedge_{M_{ij}=1} B(\ell_j,r_i).$$

This notation abbreviates literal N(left,right); records, with all name bits written out. Let $s$ be the number of matrix ones. Each record has $2d+7$ symbols, so the prefix length is exactly $s(2d+7)$. Feed it to $A$ once and save the resulting configuration $C_M$. It is satisfiable, since every variable may be false.

When the next Boolean vector $v$ arrives, start from $C_M$ and append T(left_j); for precisely the indices with $v_j=1$. Call the resulting configuration $C_{M,v}$. This prefix is still satisfiable: keep every right-side variable false.

To determine row $i$ of the product, start a fresh branch from $C_{M,v}$, append T(right_i);, and negate the recognizer’s acceptance bit. The decisive equivalence is

$$P_M\wedge\bigwedge_{j:v_j=1}T(\ell_j)\wedge T(r_i) \text{ is unsatisfiable} \quad\Longleftrightarrow\quad \bigvee_j(M_{ij}\wedge v_j)=1.$$

For the forward obstruction, any selected neighbor and the queried right vertex are both true, violating their NAND record. Conversely, if there is no selected neighbor, assign true exactly to the selected left vertices and the queried right vertex. Every forbidden pair is satisfied. Unselected variables need no explicit false pins.

Repeat the row branch for all $i$, output the complete product, and only then accept the next vector. That vector again starts from $C_M$. No future vector is used early, and no formula record is deleted or undone inside $A$.

Complete resource accounting

A pin record has $d+5$ symbols. For $n$ vectors, all vector branches use at most $n^2$ pins, and all row-query branches use exactly $n^2$ pins. Therefore

$$H\le s(2d+7)+2n^2(d+5)=O(n^2\log(n+2)).$$

Reading the matrix and vectors, generating the explicit names and writing $n^2$ output bits fit this bound. The initial configuration is fixed. Matrix preparation costs $O(n^2+s\log(n+2))$, each vector’s pins and all row queries cost $O(n\log(n+2))$, and saving or restoring a configuration costs $O(1)$. Each query costs $O(\log(n+2))$, including its whole name and punctuation. No post-input work by the recognizer is assumed.

All allocated history is $S=O(H+1)$ words, including unused branches; its literal bit size is $O(n^2\log^2(n+2))$. Since $H$ is polynomial in $n$, logarithmic-size address words suffice. The constants depend on the single fixed automaton, not on the matrix or its size. No advice or nonuniform family of recognizers is used.

Each tested formula has $b\le 2n$ distinct variables and length at most $s(2d+7)+(n+1)(d+5)$. In dense instances with all variables present this is $\Theta(b^2\log(b+2))$. There is no exponential-in-width claim and no free preprocessing of a succinct matrix. Sharing the already processed matrix is exactly the native immutability consequence just proved.

Since $n^2\log(n+2)=O(n^{5/2})$, the hypothesized recognizer contradicts OMv.

Reversal and implication constraints

The same proof applies to a recognizer for $L_B^R$. Feed the reversal of each individual record while retaining the chosen record order. Reversing the whole resulting string restores the original record spellings in reverse order. Conjunction order has no semantic effect, so the same acceptance equivalence holds at every complete-record boundary. Lengths and branch costs are identical. This proves a second reduction, without assuming that $\mathsf{SA}$ is closed under reversal.

The scaffold/PEG theorem says $K\in\mathsf{PEG}$ exactly when $K^R\in\mathsf{SA}$. Excluding both native orientations therefore excludes both PEG orientations, conditional on OMv. The source is Loff, Moreira and Reis, Theorem16.

There is also a direct implication-family version. Encode a matrix one by $\ell_j\Rightarrow r_i$, append true pins for selected left vertices, and test row $i$ with a false pin on $r_i$. Only left-to-right implication edges occur. The tested formula is inconsistent exactly when $(Mv)_i=1$: set each unselected left variable false and each unqueried right variable true. The same resource proof excludes ordinary $\{T,F,\Rightarrow\}$ recognition under OMv, in both orientations.

This does not settle equality SAT. Replacing directed implications by undirected equalities permits longer alternating paths through unselected vertices, which can connect a selected left vertex to a right vertex even when their matrix entry is zero. Equality remains a distinct open candidate in this investigation.

Structural consequences

Every NAND-and-pin formula is Horn and has clause size at most two. An offline decision procedure first collects the pinned variables and then scans the forbidden pairs. With a binary trie, all literal name routing and storage take $O(N)$ finite-pointer work over these passes. Native nonmembership under OMv therefore occurs inside an especially simple polynomial-time family.

More strongly, every inconsistent valid instance contains T(u);, N(u,v);, and T(v);. If the names coincide, two records suffice. Assigning exactly the pinned variables true proves this criterion in both directions. The maximum witness size is constant, with no long propagation chain. On the relational instance structure this is the fixed first-order condition $\neg\exists x\exists y\,[T(x)\land B_{\mathrm{record}}(x,y)\land T(y)]$, where $B_{\mathrm{record}}$ records the forbidden pairs. This concerns the variable/constraint structure, not first-order definability of its serialized binary-name string.

Consequently, assuming OMv:

• classical Horn or bijunctive tractability does not suffice for native scaffold recognition;
• even a constant bound on contradiction witnesses does not suffice;
• adding a single pair-exclusion relation to a native unary family can destroy native recognizability.

For a fixed relation-record language containing $T$ and $B$, restriction to just those tags transfers the obstruction directly. For conventional signed-clause 2CNF or Horn syntax allowing unit clauses, replace T(w); by a positive unit clause and N(u,v); by a clause with the two names negated. This copies each name only once and adds bounded punctuation/sign output per source symbol. The established bounded-output one-way inverse closure therefore gives the same conditional nonmembership for those encodings. The inverse-image recognizer is combined with the regular source-record parser, so malformed source strings reject even if their transformed text happens to be valid. This finite-control product preserves the native deadline. No arbitrary logspace or gadget closure is being assumed.

The mechanism is reuse across alternatives: the recognizer would make many different sets of forced endpoints cheap to explore from one stored relation. It is stronger than the observation that one late query is difficult, and it applies to all native representations.

Prior work and assessment

The matrix/independent-set connection is established prior work. Henzinger and coauthors’ §2.2.1, Theorem2.12 and its bipartite-graph proof, printed pp17–18, connect online products with independent-set and 2-CNF queries. Their §5.1, Definition5.1 and Lemma5.2, printed p38, explains the corresponding prepare-vector-row query pattern.

Assessment: this result is a conditional native-language application of that established framework. The contribution here is the explicit snapshot simulation for every native SA, ordinary serialized-name and all-history accounting, and the resulting SAT-family and bounded-witness consequences. The matrix gadget and hardness conjecture are not new. The proof gives a consequential model-specific conclusion without claiming a new general lower-bound technique or first-ever priority.

Two independent proof reviews checked the branch semantics, assignments, timing, reversal and allocation argument. The result is a written reduction, not a formal verification. OMv remains an explicit mathematical assumption throughout.

The next decisive question is whether an applicable unconditional query lower bound can exclude the same $O(n\log n)$ vector preparation and $O(\log n)$ row query with polynomial storage, or whether these parameters require a conditional obstruction. Equality recognition must separately resolve idempotent merges and current component information. It should no longer be treated as the only route to a meaningful SAT/scaffold distinction.