Equality SAT: linear work and the native input deadline

Working research, 4 October 2026. Written construction and primary-literature assessment; no native SAT recognition or separation theorem.

The statement worth resolving

Candidate E. One deterministic native scaffolding automaton recognizes every satisfiable conjunction of equality constraints and Boolean pins in the ordinary binary-name encoding below.

If true, E would establish native undirected connectivity for the encoding-equivalent graph language, by the proved translations in the preceding review. It would give a natural SAT family with unbounded, arbitrarily ordered interactions a genuine native implementation. If false, a proof against all native automata would already separate a polynomial-time SAT family from this model. Neither outcome is established here.

This assessment yields two useful results. First, a name-sensitive mutable pointer construction solves equality SAT in linear total work, with linear allocation. Second, the native recognizer conjecture implies a persistent connectivity service whose operation costs include the names. Those costs evade the reviewed standard connectivity lower bounds. The unresolved issue is therefore more specific than expensive propagation: it is maintaining component information immutably and delivering it within the serial input deadline.

Encoding and two different contracts

The fixed alphabet encodes records T(w);, F(w);, and E(u,v);. Names are nonempty binary words, compared literally; leading zeros matter. The first two records force their variable to 1 or 0, respectively, and the third equates its endpoints. Records may occur in any order, repeat, or introduce new names. The empty conjunction is satisfiable; malformed input is rejected. Let $N$ count every actual symbol, including all name bits and delimiters. The number $b$ of distinct variables is at most $N$.

The native target has fixed finite control and labels, fixed degree and inspection radius, fixed initialization, chronological immutable storage, and its usual single new node per input symbol. Its permitted local observations do not include physical pointer identity or address arithmetic. Acceptance is determined at ordinary input end, with no cleanup, external handles, padding, advice or free preparation. One automaton must work for every length.

The mutable control below instead has finitely many pointer registers, finite labels, bounded outgoing degree, and constant-cost local pointer reads, writes and allocations. Incoming degree is unrestricted. It may spend time after a complete record arrives, including the last record. Its guarantee is worst-case work proportional to that record’s length, not constant work between successive symbols. It starts from a fixed empty structure. This is a comparison algorithm, not a scaffolding automaton.

A name-sensitive linear-work construction

Written control theorem. The mutable model just specified decides equality SAT with $O(N)$ total work and $O(N)$ allocated records, counting all discarded storage. Each complete record costs $O(\text{record length})$ in the worst case. No numeric addresses, unbounded integer registers or pointer-equality primitive are needed.

Use a binary trie to map each literal name to an element of a union-find forest. A terminal port distinguishes a name from its proper extensions. Use union by rank without path compression, but initialize the rank of a newly encountered name $w$ by

$$r(w)=-2|w|-1.$$

Ranks are analytical integers; the implementation below stores unary chains. Attach the smaller-rank root to the larger-rank root. For equal ranks, choose one root, increase its rank by one, and attach the other. Do nothing if the roots already coincide.

Assign each name the proof weight $\mu(w)=2^{-2|w|-1}$. The total over all possible nonempty binary names is finite:

$$\sum_{w\in\{0,1\}^{+}}\mu(w)=\sum_{\ell\ge1}2^{\ell}2^{-2\ell-1}=\frac12.$$

Inductively, a component with root rank $r$ has total weight at least $2^r$. An unequal-rank merge preserves the larger root’s bound. An equal-rank merge doubles that bound and increments the rank. Thus every root rank is at most $-1$. Every parent edge goes to a strictly larger rank; once a node ceases to be a root, its rank is frozen, and later root increments preserve strictness. A node’s rank never falls below its initial value. Consequently,

$$\operatorname{depth}(w)\le -1-(-2|w|-1)=2|w|.$$

This bound depends on the queried name, not the size of its component. Even a fixed short name can belong to an arbitrarily large component without a long find path. No assumption about edge order enters the proof.

For an actual finite-label implementation, represent the positive deficit $d=-r$ by a unary linked chain. While reading a name, build two chain cells per bit and one extra cell. If the name is new, this chain initializes its rank. A duplicate name’s temporary chain may be abandoned; its allocation is still charged to that occurrence. A root reached from endpoint $w$ has deficit at most $2|w|+1$. Compare two root chains with temporary cursors in $O(|u|+|v|+1)$ steps. The shorter chain denotes larger rank. Equal-rank promotion drops one chain cell by changing the root’s chain pointer. The positivity of the remaining deficit follows from the weight bound. The machine never computes a real weight or performs integer arithmetic.

Root coincidence does not require primitive pointer equality. Set a temporary finite mark at the first root, inspect the second root’s mark, then clear the first. All such marks are clear between operations. A missing parent port identifies a root. Each root also carries a two-bit pin mask. Pins set the corresponding bit; a merge combines masks by Boolean OR. A mask containing both bits permanently sets a contradiction flag. This handles pins both before and after arbitrary edges. Invalid syntax likewise latches rejection.

Trie routing, initialization, find walks and rank comparison all fit the record-length budget. A fixed number of registers suffices for the trie root, input cursors, endpoint roots and chain cursors. Summing record budgets gives $O(N)$ work and allocation, including unreachable rank cells and temporary storage. With ordinary binary pointer serialization, $S=O(N)$ abstract records occupy $O(N\log(N+2))$ bits. Input preparation is just the charged parsing and insertion; there is no external preprocessing or deferred query beyond the explicitly allowed record-boundary work.

This is an elementary adaptation of classical union-by-rank reasoning. Its proof and finite-pointer implementation were independently checked; it has not been formally verified, and novelty is not claimed.

What the construction does not establish

Knowing that a lookup needs at most $2|w|$ steps does not make those steps available after $w$ has already arrived. The trie may expose its element pointer only at the final bit. A long final pin can then require a find walk with only a constant number of delimiters left. Work cannot be charged retroactively to input symbols. The construction also rewrites old trie, parent and pin fields, including its temporary identity mark. Neither timing nor mutation has been eliminated.

These are gaps in this construction, not impossibility proofs for other representations. A native recognizer might maintain different summaries or overlap work with the spelling of a name.

A necessary consequence of native recognition

Checked conditional implication. If E holds, equality insertion and Boolean connectivity queries have a persistent service using

$$O(|u|+|v|+1)$$

native simulation steps and fresh records per operation, with all history charged.

Keep the recognizer configuration after an equality-only prefix $P$: its top pointer and finite control. To test whether $u$ and $v$ are connected, fork that configuration, run the suffix T(u);F(v);, and negate its acceptance bit. This is correct because the prefix contains only equalities. The original branch remains available for future insertions and queries. Saving old configurations permits the external wrapper to update an older version as well. The wrapper’s version handle is an interface of this consequence, not a new primitive granted to the SAT input language.

Each native transition inspects a fixed-size neighborhood, so a stronger word-cell machine simulates it with $O(1)$ probes per symbol. If $H$ is the total number of serialized symbols processed across all branches, storage is $O(H+V+1)$ records for $V$ saved version handles. Dead query branches and old versions count. With $n$ identifiers of length $\Theta(\log n)$ and polynomially many operations, $O(\log n)$-bit cells suffice, and the operation bound becomes $O(\log n)$, not $O(1)$. For unrestricted history, address width must instead account for $\log(H+V+2)$.

The wrapper offers no arbitrary edge deletion. Restoring a version is not deleting one selected edge while retaining all subsequent insertions.

What five primary papers contribute

The preceding classification review remains the baseline. This review follows the construction and obstruction chains below. The scopes listed are the proofs actually examined, not claims that every theorem in each paper was rechecked.

The comparison has two further proof-level lessons. In the lower-bound simulations, crossing addresses, contents and evidence about whether a cell was written are accounted for; hiding these channels would invalidate a new communication argument. Neither snapshots nor Boolean output provide a shortcut around the incremental theorem: its proof already uses independent suffix tests and Boolean queries. The missing ingredient is a stronger bound under an applicable contract, not a cosmetic change to its output.

Petersen’s example is particularly useful against a premature deadline objection. The input explicitly lists $2^n$ values of length $\lfloor n/2\rfloor$, followed by addresses $x,y$. The construction finishes a delayed path during $x$, then uses queued bits and faster traversal during $y$. The proof relies on those ordered phases; arbitrary interleaving of the addresses is not covered. Its prefix has $\Theta(n2^n)$ symbols. We import neither the older pointer-machine lower bounds cited by that paper nor a claim about their current open status: those original proofs were not part of this review.

Direction justified by the comparison

Keep E as the central construction test. The next research pushes should investigate a concrete representation that resolves a serial name to current component pin information by its delimiter, while incorporating arbitrary merges immutably. Test late pins, a short name in a huge component, repeated names, names that are prefixes of others, and a long last record with no following input. The control above disposes of a component-size-only objection; it does not solve this combined test.

Across the next four research runs, prioritize a sustained direct construction attempt and its hostile examples, rather than four independent closure lemmas. If only a favorable order or delayed-query format works, retain it as a control and require a deadline-preserving translation before claiming E. A lower-bound route must beat the serialized-name allowance and cover alternative native summaries, with storage, initialization and observations explicit. Standard word union-find bounds and lower bounds for one parent-forest presentation are not enough. If neither route produces a consequential mechanism, reassess the equality candidate against the other live SAT statements at the next review rather than refining irrelevant constants.

The broader native tractability and polymorphism-invariance statements remain hypothetical. Unary-pin recognition still carries its saved deque premise; this mutable algorithm does not discharge it. No natural SAT family has been separated from native SA here, no ordinary 3SAT upper bound is claimed, and no P-versus-NP consequence follows from this control.

Construction follow-up: why direct persistence did not finish the job

A subsequent direct construction attempt did not establish native equality recognition. It tested sequential lookup, eager summaries, and a persistent dictionary of component records, then followed a compact-identifier repair. The failures below concern these implementations, not every scaffolding automaton. The linear mutable-work theorem above remains unchanged.

A small encoded family defeats the sequential pipeline

For example, the names 0, 10, 110, 1110 can acquire the parent chain

$$1110\longrightarrow110\longrightarrow10\longrightarrow0.$$

In general let $w_k=1^{k-1}0$ for $1\le k\le L$, and process

$$E(w_L,w_{L-1});\ E(w_{L-1},w_{L-2});\ \cdots;\ E(w_2,w_1);\ F(w_1);\ T(w_L);.$$

Here mathematical subscripts abbreviate the actual binary words; they are not the input encoding. There are $b=L$ variables and exactly $N=L^2+6L+3$ symbols in the literal records. The names are pairwise prefix-free. With the rank initialization above, each merge attaches the current longer-name root to the next shorter singleton, without a tie or rank promotion. Thus the final pin’s parent path has $L-1$ edges.

A sequential implementation that first routes the complete name and only then starts Find leaves this entire walk until the last name bit has arrived. Only ); remains. No fixed work allowance per remaining symbol covers arbitrarily large $L$. Prefix-freeness also defeats the particular suggestion of starting Find at an earlier terminal encountered along this name’s trie path: there is no such terminal. Internal-node summaries or speculative work are not excluded.

Eagerly caching the exact representative at every member exchanges that problem for another. Just before the eight-symbol record E(10,0);, the component of $w_2$ contains $L-1$ names. Under this rank policy its representative becomes $w_1$. Updating every direct member cache takes $\Omega(L)$ writes. A cache refreshed only when its own name is queried instead leaves old forwarding chains. These observations do not exhaust the possible representations: indirection and different semantic summaries remain available.

Replacing each mutable record by a name lookup can multiply costs

Consider the proposed persistent implementation whose dictionary maps each element’s original name to its current record. Following a parent means spelling its name through the current dictionary, starting again from the dictionary root. This is the exact access rule being tested; implementations with other maintained shortcuts are outside it.

Initialize all $2^m$ distinct names of length $m$ and merge equal-sized groups in a balanced tournament. Every merge joins equal-rank roots. Inductively there is a leaf with a parent path of length $m$, regardless of which root wins ties. Every name on that path has length $m$. Its uncompressed Find therefore performs $m+1$ complete dictionary routes and costs $\Theta(m^2)$, although the pin supplying that name has only $m+4$ symbols. The preparation has $\Theta(m2^m)$ symbols and $b=2^m$ variables. This is not an exponential lower bound for compact SAT inputs; it is a failed accounting argument for this dictionary implementation.

Name lengths can cause an even sharper failure. For the legitimate convention that the first endpoint root wins ties, a length-$L$ root can be promoted to rank $-5$ using only three fresh singleton names at each length $k=L,L-1,\ldots,3$. At a stage with root rank $-2k-1$, merge it with one length-$k$ singleton, separately merge two more such singletons, and merge the two resulting equal-rank roots, always retaining the distinguished root. Its new rank is $-2k+1$, ready for the next stage. The total preparation uses $O(L)$ names and $O(L^2)$ encoded symbols. A fresh length-two name can then attach directly below this root. Resolving the root by its original name costs $\Omega(L)$ for a constant-length pin, despite a one-edge forest path. Choosing the shortest name on ties avoids this particular example, but not the equal-length tournament.

Compact identifiers are a partial repair, not a completed algorithm

One can bound the number of events at which a root first acquires a fixed rank $r<0$. Their component sets are disjoint: once a component has root rank at least $r$, it cannot later take part in a promotion from $r-1$ to $r$. Each event component has weight at least $2^r$. The weight proof above therefore bounds the event count by $2^{-r-1}$. A rank and ordinal code of $O(-r)$ bits can identify these events.

This supplies short identifiers for promoted roots and repairs the long-original-name example for a newly attached short reference. It does not implement their allocation or preserve earlier references. Old immutable records cannot be redirected to a future identifier. Versioned entries, forwarding records or a different representation must account for that access. Moreover, the tournament’s successive rank deficits are $2m+1,2m,\ldots,m+1$. Independent dictionary routes using explicit rank-sized codes still cost $\Theta(m^2)$. Strictly increasing ranks do not make a sum of full code lengths telescope.

The next consequential construction test is therefore a maintained component-access invariant that bypasses repeated full-key resolution, while coupling lookup to the arriving name bits. It must explain current pin information, historical references, arbitrary merges and the final-record deadline together. A potential argument charging access to rank differences would need an actual representation realizing those charges. This attempt supplied no such representation, and no native SAT membership or separation result.