Prefix clauses have a native SAT recognizer

5 October 2026. Written construction using the existing strict persistent FIFO and serial name dictionary.

A clause can forbid one assignment prefix without fixing the rest of the variables. Many such clauses can eventually cover every assignment. The last clause may close a hole at arbitrarily large depth, so a recognizer cannot wait to walk back through the assignment tree after reading it.

The construction below maintains the answer at the clause delimiter. It also checks, from ordinary binary variable names, that the clauses follow prefixes of one common variable sequence. Neither the sequence nor an elimination order is supplied separately.

The exact language

Use records

C(+u1,-u2,...,+uk);

Each sign is + or -, each name is a nonempty literal binary word, and commas separate literals. The record C(); is an empty clause. Leading zeros and prefix relationships between names matter. There is no whitespace in this encoding.

Call a well-formed stream prefix-consistent if there exists a sequence of distinct names

$$u_1,\ldots,u_b$$

such that the name list of every clause is exactly $(u_1,\ldots,u_k)$ for some $0\le k\le b$. Signs and clause arrival order are unrestricted. The number of variables, clause widths, name lengths and distances between occurrences are unbounded.

Written theorem. The language of exactly the well-formed, prefix-consistent, satisfiable streams has a deterministic native scaffolding-automaton recognizer.

The recognizer checks prefix consistency and distinctness. Thus C(+0,+0); rejects despite being a satisfiable clause: it repeats a variable in the proposed sequence. Likewise, C(+0,+01);C(-01); rejects because the second clause does not start with the same variable. The empty conjunction accepts. An empty clause makes the formula unsatisfiable, and malformed or incomplete input rejects.

One fixed automaton handles every input length. There are no supplied variable handles, length headers, padding, preprocessing, mutation, pointer-identity tests or extra end-of-input steps. The theorem concerns the displayed forward encoding. The scaffold-to-PEG correspondence gives a PEG for its string reversal; no direct native theorem for the reversed encoding is asserted here.

This is an unbounded SAT family: a longest clause contains all $b$ variables, so the primal graph can be a clique of unbounded size and treewidth. The construction does not enumerate all $2^b$ assignments.

Clauses as forbidden prefixes

The clause with literals $(\ell_1,\ldots,\ell_k)$ is false on exactly one bit prefix $p_1\cdots p_k$: put $p_i=0$ when $\ell_i=+u_i$, and $p_i=1$ when $\ell_i=-u_i$. It forbids every full assignment extending that prefix.

Interpret the accumulated prefixes as a subset of infinite binary sequences. This avoids having to know the final number of variables while reading the input. At a complete input, membership of that subset depends only on the first $b$ coordinates. Consequently the formula is unsatisfiable exactly when all infinite binary sequences have been covered.

For example,

C(-0);C(+0,-01);C(+0,+01,-1);C(+0,+01,+1);

uses the distinct name sequence 0, 01, 1. Its forbidden prefixes are 1, 01, 001, then 000. The first three clauses leave one assignment; the final clause removes it. More generally, forbidding

$$1,01,001,\ldots,0^{b-1}1$$

and then $0^b$ closes a hole at depth $b$. The final answer must already be available at the ordinary closing delimiter.

Covered subtrees and paths that need no return walk

Use the counter-free strict persistent FIFO, including the opaque-frame payload extension justified in the unary SAT construction.

A logical assignment subtree has one of three types:

• Blank: no extension is covered.
• Covered: every extension is covered.
• Spine(Q,Z): a FIFO of path frames ending in Covered, with a second FIFO of marker tokens.

A frame Frame(a,other) contains a direction bit and one off-path subtree. Its context $C_f(t)$ is an unmarked binary trie node whose $a$-child is $t$ and whose other child is other. If the frames of $Q$ are $f_1,\ldots,f_m$, the meaning of a spine is

$$C_{f_1}\bigl(C_{f_2}(\cdots C_{f_m}(\mathrm{Covered})\cdots)\bigr).$$

This equation specifies its meaning; it does not instruct the machine to fold the queue.

The marker invariant is:

$$Z\text{ has one token for each frame of }Q \text{ whose off-path subtree is not `Covered'.} \tag{1}$$

All subtree references are canonical: a fully covered subtree is represented by the tag Covered; a stored Spine has nonempty $Z$. The direction or position of a marker need not be stored. When a frame leaves the front of $Q$, its off-path tag tells the machine whether one marker must leave $Z$.

To justify this invariant, a context has coverage value

$$\operatorname{cover}(C_f(t)) =\operatorname{cover}(\mathrm{other})\land\operatorname{cover}(t).$$

The final tip is covered. Therefore the whole path is covered exactly when every off-path subtree is covered, equivalently when $Z$ is empty. Canonicalizing an empty-marker path to Covered is an exact semantic replacement, even if the discarded frame queue is long.

Exposing one node

For Blank, view returns two Blank children. Covered needs no exposure: any further prefix below it is already redundant.

For Spine(Q,Z), read and dequeue the first frame Frame(a,other). If other is not Covered, dequeue one marker as well. This marker dequeue is legal by (1). Let the remaining queues be $Q'$ and $Z'$. The continuing child is

$$\begin{cases} \mathrm{Covered},& Z'\text{ is empty},\\ \mathrm{Spine}(Q',Z'),& Z'\text{ is nonempty}. \end{cases}$$

The other child is the stored other. If $Z'$ is nonempty then $Q'$ is nonempty by (1). This exposes exactly one logical node. It neither folds the path nor recursively exposes either child.

Inserting the current clause

Retain a committed coverage root. At clause start, set current to that root and start two empty path queues $P,W$.

For each literal sign, obtain its falsifying bit $a$. Unless the clause has already been found redundant:

1. If current is Covered, mark the clause redundant.
2. Otherwise expose its two children once.
3. Enqueue Frame(a,other) into $P$, where other is the unchosen child. Enqueue a marker into $W$ exactly when other is not Covered.
4. Descend to the chosen child.

If the chosen subtree is covered, this can be noticed immediately or at the next sign or closing delimiter. A redundant clause leaves the committed root unchanged; its partial path queues are discarded.

At the closing ), a nonredundant clause replaces its current subtree by Covered. The new committed root is Covered if $W$ is empty, and Spine(P,W) otherwise. The empty clause is exactly the empty-path case and therefore produces Covered. No old descendant must be copied or inspected.

The path queues contain precisely the contexts of the already-read falsifying prefix, in root-to-leaf order. Replacing their tip by Covered therefore adds exactly that forbidden prefix. Equation (1) holds because every enqueue and dequeue preserves its filtered-token interpretation. Induction over signs and completed clauses proves both the represented covered set and the immediately readable root answer.

This representation is stronger than keeping an old Boolean summary on each copied ancestor. Such summaries would become stale after a deep insertion. Here all summaries remain exact because the path’s coverage is determined by an immediately observable marker queue, and each suffix exposes its own updated marker queue in bounded work.

Checking the common sequence while names arrive

Maintain a master FIFO containing the longest complete name list seen so far, serialized internally as

$$u_1\#u_2\#\cdots u_b\#.$$

The marker # is an internal queue payload, not additional input. The actual comma or closing parenthesis supplies the step that processes it.

At the start of a clause, copy the then-current master root into a read cursor. This cursor is a frozen version. While it is nonempty, compare each arriving name bit with its front and dequeue on agreement. At each name delimiter, require and dequeue its internal #. Signs do not advance this cursor. A mismatch rejects. A clause may end with a suffix of the master cursor still unread: shorter prefixes are allowed.

If the cursor is empty before the next name starts, the clause extends the master sequence. Append that new name’s bits to the master FIFO as they arrive, then append its separator at its delimiter. Continue extending for the rest of this clause. In particular, do not redirect the frozen read cursor to newly appended bits and compare the clause against itself.

To check distinctness, maintain the existing serial binary-name dictionary with the finite terminal payload Seen. Only an extending name needs a dictionary lookup. Its bits drive that lookup as they arrive. At its delimiter, reject if it was already marked; otherwise set its payload to Seen. This detects repetition of any earlier master name, including one introduced earlier in the same clause. Proper-prefix names such as 0 and 01 remain distinct by the dictionary’s established terminal convention.

For a clause that stays inside the old master, direct character comparison already identifies each coordinate. It cannot introduce a duplicate name because the master was checked when constructed. The read cursor is persistent, so consuming it never changes the saved master or a future clause’s starting point.

Inductively, all completed clauses agree with prefixes of the master, and the master names are distinct. Conversely, any input admitting a common distinct sequence passes these comparisons and extends the master only by its new tail. Thus the structural condition is checked exactly, without a supplied order or a scan at clause end.

The assignment-trie operation and the name checks are independent bounded activities on the same actual input. Signs perform assignment-prefix steps; name bits perform sequence comparison or extension and dictionary work. Invalid names or malformed syntax latch rejection, so provisional work within an incomplete record needs no rollback.

Native resources and input-end correctness

The source representation has a fixed collection of roots: committed and current coverage subtrees, two new coverage-path queues, master and expected-name queues, and the dictionary’s committed root, current subtree and new path queue. Parser, extension and redundancy states are finite.

The opaque-frame FIFO theorem retains a bound of 12 fresh records per operation and has conservative old-access radius 7. A sign therefore needs at most 48 queue records plus a bounded number of frames, spine wrappers and header records. Other events have fewer queue operations. No transition performs a second nested view.

For a conservative simultaneous-record certificate, use one header root, arity bound $q=12$, fresh-batch bound $A=128$, and old-address radius $r=32$. The header has nine pointer fields. Queue records fit within the existing arity-six layout; coverage frames and wrappers have at most two pointers. Queue roots are at most two fields behind the header, and the extra front-frame/off-child observations fit within the stated radius. The fixed number of consecutive primitive calls and their same-batch records are included in these loose bounds. All targets are exposed old fields or declared same-batch slots.

Initialization consists of a fixed finite graph containing the blank and covered tags, empty FIFOs and the dictionary’s blank state. The reviewed simultaneous-record compiler therefore yields one fixed native automaton. At actual input length $N$, it has $N+1$ physical nodes; all source history, discarded paths and old queue versions comprise $O(N)$ records. Literal pointer serialization costs $O(N\log(N+2))$ bits.

Acceptance is allowed only between complete records, with no syntax or structural error and with an uncovered committed root. The root has already been settled at ), before the record’s final ;. No end-of-input action or deferred fold is needed.

Scope and attribution

The clause supports here are totally ordered by inclusion, and hence are β-acyclic. Ordyniak, Paulusma and Szeider’s full paper, §3, Lemmas 1–2 and Theorem 1, establishes polynomial-time SAT for the much larger β-acyclic class through elimination whose resolvents remain inside parent clauses. That result supplies structural context; it is not the native streaming construction above.

The additional restriction here is the checked serial order of literals: each clause must list a prefix of the same sequence. The theorem does not cover arbitrary permutations of literals in nested-support clauses, nor general β-acyclic CNF. Finding an elimination order offline or supplying one separately does not establish the same input-clock theorem.

The implementation reuses the program’s strict FIFO, opaque-frame capsule trie and native compiler. The additional mechanism is the filtered marker queue that makes every coverage spine and exposed suffix immediately exact. No new general persistence theorem or first-ever priority claim is made.

The proof is written, not formally verified. The finite checker scripts/verify_prefix_clause_native_sat.py tests the abstract coverage semantics on all insertion sequences of at most four prefixes of length at most three, including branches from retained versions. It separately checks the streamed common-sequence criterion on finite name-list families. Its tuple queues and Seen set are semantic models; it does not verify the strict FIFO implementation, local resource certificate or full character parser. Those claims rest on the stated invariants and saved construction dependencies.

Together with the shared-core construction, this gives two distinct positive mechanisms: condition on finitely many coordinating variables, or maintain a nested family of forbidden assignment prefixes. The next decisive test for the second mechanism is nested clause supports with arbitrary literal order. That changes a checked presentation requirement while keeping the same semantic family, so it directly tests how much of this result comes from the way the formula arrives.