An unconditional XOR-SAT obstruction for scaffolding automata

4 October 2026. Written reductions with independent proof review; the cell-probe lower bound is imported.

Unary constraints can be checked by a native scaffolding automaton. Ternary parity constraints already cross a boundary: no native scaffold recognizes ordinary XOR-SAT with true and false pins, in either input direction. This result needs no OMv assumption. It applies a theorem of Young Kun Ko to a formula that stores many linear computations and receives their inputs later.

The distinction becomes sharper when combined with the conditional NAND obstruction. With both pins available, every nonaffine Boolean relation is excluded under OMv. Among affine relations, any relation that cannot be expressed using only unary restrictions, equality and disequality is excluded unconditionally. Equality and disequality remain the central unresolved cases.

The subsequent propagation and replay note excludes implication, Horn-SAT and 2SAT unconditionally through directed reachability, and extends the obstruction to every genuinely multi-input Boolean gate. It also gives an ordered-circuit control where one verified replay changes native recognition. The parity argument and the conditional status of pure NAND below remain intact.

Statements and encoding

Fix a finite Boolean constraint language $\Gamma$ containing $T=\{1\}$ and $F=\{0\}$. Each relation has fixed finite arity and its own fixed tag. A record consists of its tag, parentheses, comma-separated nonempty binary variable names, and a semicolon. For example,

$$\texttt{X(001,010,011);}\qquad\texttt{F(001);},$$

where $X(a,b,c)$ means $a\oplus b\oplus c=0$. Names are literal words, so leading zeros matter. Records and arguments may repeat, occur in any order, and use names of any length. The empty conjunction accepts; malformed strings reject. All characters contribute to encoded length $N$.

A native deterministic SA has fixed finite control, labels, degree, radius and initialization. Each input symbol causes one new immutable node and bounded observation of the top’s labelled port unfolding. It has no physical pointer-equality test, address arithmetic, free preprocessing or computation after input end. One fixed automaton must work at every input length.

Call a relation 2-affine if it is definable by a conjunction of

$$x_i=c\quad\text{and}\quad x_i\oplus x_j=c,\qquad c\in\{0,1\}.$$

Include the full and empty relations. This definition allows equality and disequality, but no irreducible equation involving three or more variables.

Native constraint boundary. For the encoding above:

Thus, under OMv,

$$\operatorname{SAT}_{\rm enc}(\Gamma)\in\mathsf{SA} \quad\Longrightarrow\quad \text{every relation in }\Gamma\text{ is 2-affine}.$$

This is a necessary condition, not a characterization or an assertion that every 2-affine language is recognizable. The conclusions apply to PEGs in both orientations as well, by the reversal-sensitive SA/PEG equivalence. Ordinary signed-clause 3SAT is also excluded unconditionally by the direct construction below.

The unconditional parity construction

Imported lower bound

Preprocess $m=n^2$ Boolean row vectors of length $n$. Then receive the $n$ coordinates of a vector $v$ sequentially. A final index $i$ asks for the inner product of row $i$ with $v$ modulo two. In logarithmic-word cell-probe computation, Ko’s Theorem 1.1 rules out polylogarithmic coordinate-update cost together with query cost

$$o\!\left(\frac{\log^2 n}{(\log\log n)^2}\right).$$

We use the precise statement in §3, printed p12, and the final-query simulation in §3.1, Protocol 4, pp14–16, of Ko’s paper. It permits adaptive access and preprocessing. Its hard sequence uses sequential coordinates followed by one final query; no intermediate query or overwriting of a coordinate is needed. The paper is accepted at FOCS 2026, as checked on 4 October 2026.

Encode the rows before their inputs arrive

For a matrix $M\in\mathbb F_2^{m\times n}$, create variables $z$, $x_1,\ldots,x_n$, and $a_{ij}$ for $1\le i\le m$, $1\le j\le n$. Set $a_{i0}=z$ as a naming convention, not an additional variable. Prepare the formula prefix

$$F(z)\ \wedge\ \bigwedge_{i=1}^m\bigwedge_{j=1}^n X(a_{i,j-1},t_{ij},a_{ij}),\qquad t_{ij}=\begin{cases}x_j&M_{ij}=1,\\z&M_{ij}=0.\end{cases}$$

These are ordinary records written out in full. For every assignment to the $x_j$, there is a unique assignment to the accumulators, and

$$a_{in}=\bigoplus_{j=1}^n M_{ij}x_j.$$

When vector coordinate $v_j$ arrives, append exactly one pin, $T(x_j)$ or $F(x_j)$. After all $n$ coordinates, append $F(a_{in})$ for the queried row. The complete formula is satisfiable exactly when that row’s inner product is zero. The prefix and every partial assignment prefix are satisfiable, so an early inconsistency cannot erase needed information.

There is no default-zero assumption for coordinates that have not arrived. Queries occur only after all coordinates have been pinned.

Charge the entire input and simulation

There are exactly

$$b=1+n+mn$$

variables in the complete formula. Assign each a distinct $d$-bit name, where $d=\lceil\log_2(b+1)\rceil$. An $X$ record has $3d+6$ characters; a pin has $d+4$. Consequently every tested formula has exactly

$$N=(d+4)+mn(3d+6)+(n+1)(d+4)=\Theta(b\log(b+2)).$$

For $m=n^2$, this is $\Theta(n^3\log n)$, polynomial in $n$.

Suppose a native recognizer existed. Store each scaffold node in a constant number of cell-probe words. Its fixed radius and degree make every input transition cost $O(1)$ probes. Store the top pointer and finite control in a constant number of charged cells; neither persists as a free information channel. There are $O(N)$ stored words, or $O(N\log(N+2))$ literal bits, and word size $\Theta(\log n)$ suffices.

Processing the matrix prefix costs $O(n^3\log n)$ probes and words. Each arriving vector bit generates and processes $d+4=O(\log n)$ characters. The final row query has the same cost. Name generation, controller storage, allocation and the output bit are all accounted for. Thus the resulting data structure has

$$t_u=O(\log n),\qquad t_q=O(\log n),$$

contradicting Ko’s lower bound. For a read-only cell-probe query, query-local new nodes are ephemeral within that single query and cannot survive as an uncharged cache. Counting those nodes explicitly would also preserve the bound. This reduction needs one final query, so no snapshot or branch operation is required.

The contradiction ranges over every fixed native recognizer. It does not depend on an elimination order, dictionary presentation or chosen Gaussian-elimination implementation.

Both orientations and ordinary 3SAT

For a recognizer of the reversed language, reverse each individual record while retaining the construction’s record order. Reversing the whole word then gives valid original records in reverse order. Conjunction is order-independent, so the same reduction works. No closure of SA under reversal is assumed. Loff–Moreira–Reis Theorem 16 then excludes both PEG orientations too.

To obtain ordinary 3CNF directly, replace each parity gate by

$$(a\lor b\lor\neg c)\land(a\lor\neg b\lor c) \land(\neg a\lor b\lor c)\land(\neg a\lor\neg b\lor\neg c).$$

Use signed binary-name clauses with parentheses, commas and semicolons, allowing one to three literals. Matrix-gate expansion occurs during matrix preparation; arriving bits and the final query remain single unit clauses. All repeated names are written and charged. This preserves the phase bounds without assuming a general reduction closure for native SA.

If exactly three distinct variables per clause are required, remove tautologies and repeated literals first. Pad a two-literal clause $A$ by $(A\lor h)\land(A\lor\neg h)$, and a unit $\ell$ by the four clauses $\ell\lor(\pm h)\lor(\pm k)$, using private fresh variables. Each pin now costs only a constant number of logarithmic-length records. The same contradiction follows. This is a limitation of native recognition; it gives no separation of P from NP.

Why the result extends beyond one parity relation

Let $R=a+V$ be a nonempty affine relation and let $W=V^\perp$ be its equation rowspace. The inclusion-minimal nonzero supports in $W$ span $W$: subtract a row of proper sub-support from a nonminimal row and induct on support size.

If all those minimal supports have size at most two, $R$ is 2-affine. Otherwise choose a minimal support $C$ of size at least three. The only rows supported inside $C$ are zero and its defining row. Projection onto $C$ therefore has exactly one parity equation. Pin all but three coordinates of $C$ to zero and existentially quantify the other coordinates of $R$. This gives ternary parity, with some right-hand side $c$.

If $c=1$, two odd-parity constraints produce even parity:

$$\exists t\,[\,x\oplus y\oplus t=1\ \land\ t\oplus z\oplus0=1\,] \quad\Longleftrightarrow\quad x\oplus y\oplus z=0.$$

We have obtained a fixed gadget using $R$ and pins. Replace each gate of the matrix prefix by a fresh copy of that gadget. Its auxiliary variables are private to that copy, and its size depends only on the fixed relation $R$. The resulting prefix still has $O(n^3\log n)$ characters and variables of $O(\log n)$ name length. Updates and queries still pin only their named endpoints. This proves the affine line of the table.

The opposite branch uses a classical Boolean-CSP implementation theorem: every nonaffine relation, with pins, implements OR, NAND or implication. See Dyer–Goldberg–Jerrum, Lemma 15 and Appendix, pp16–17, crediting Creignou–Khanna–Sudan. Only existence of private witnesses is needed here.

Write the implemented binary relation as all four pairs except $(\alpha,\beta)$. Replace each one-entry of an OMv matrix by its fixed gadget on a left variable and a right variable. Activate selected left variables with value $\alpha$; test a row by pinning its right variable to $\beta$. The test is inconsistent exactly when that row meets the selected vector. Unselected left variables receive $1-\alpha$, unqueried right variables $1-\beta$, and private witnesses exist independently whenever the edge is allowed.

The completed snapshot simulation yields $O(n^2\log n)$ total OMv time, including all branches. If a gadget has $q$ auxiliaries and the matrix has $s$ ones, a tested formula has

$$b\le 2n+qs+O(1),\qquad N=O((s+n+1)\log(n+2)).$$

All allocated branching history is $O((s+n^2)\log(n+2))$ words. The earlier $b\le2n$ count for a bare NAND matrix must not be reused after introducing auxiliaries.

Both gadget arguments construct hard input strings directly. They assert no general inverse closure under primitive-positive reductions, variable copying or logspace transformations.

The positive Cartesian case processes each argument with its prescribed unary allowed set, using the native unary construction. In reversed records the tag arrives last. Start one candidate dictionary branch per possible relation tag from the committed root, processing the reversed arguments using that candidate’s known arity and unary masks. At the trailing tag select its candidate root. Reversing all names consistently preserves their identity. The number of candidates and all arities are fixed; the reviewed bounded-batch compiler therefore preserves constant native access and allocation per symbol. Empty-relation tags and source syntax are handled by finite control. Pins are essential to the negative classification: NAND without true pins is satisfied by the all-zero assignment and has a regular validity language.

An explicit access lower bound and the remaining boundary

The parity proof also applies to one fixed algorithm in a stronger deterministic one-pass model with polynomial storage, $\Theta(\log N)$-bit cells, a constant number of charged persistent registers, and an answer at input end. Suppose $h(N)$ bounds the number of cell probes per arriving symbol throughout every input of length at most $N$. The construction gives update and query costs $O(h(N)\log N)$. Ko’s theorem therefore rules out

$$h(N)=o\!\left(\frac{\log N}{(\log\log N)^2}\right).$$

This is a worst-case per-symbol access obstruction under the strict deadline. It is not a total-time lower bound for offline SAT algorithms. Native constant access is one excluded special case.

Equality and disequality survive these tests for a structural reason. Conjunction, pinning and existential projection of 2-affine relations remain 2-affine: every connected component fixes coordinates to one bit or its complement, possibly with that bit pinned. They cannot produce either the three-tuple binary gadget or ternary parity. This explains precisely where these two lower-bound constructions stop. It does not prove native recognition of the remaining families.

The immediate research choice is now focused: construct native recognition for equality/disequality, or find an obstruction that does not require either forbidden gadget. That would determine whether the necessary algebraic condition is close to sufficient.

Provenance and proof status

The transfer from suitably serialized data-structure problems to scaffold nonrecognition is established work of Kim and Park, Definition 3.2 and Theorem 3.5, already recorded in the Lab’s transfer note. Ko supplies the unconditional lower bound. The Boolean gadget theorem and affine projection argument are classical ingredients; the conditional branch uses the established OMv framework.

The contribution here is a SAT-family application with ordinary binary names, complete phase budgets, a parity-based unconditional separation, and the combined 2-affine necessary condition under OMv. This is an extension/application of known methods, with strong confidence in those attributions. No new general lower-bound technique or first-ever priority claim is made.

Independent reviews checked the source model, final-query requirement, formula assignments, names, storage, gadgets and reversal. The reductions are written proofs; they have not been formalized in a proof assistant. Ko’s theorem is an imported mathematical dependency, not an assumption like OMv.