Equal-support SAT without a common literal order

5 October 2026. A written native construction using a delayed coverage update and four explicit survivors.

Every clause in this family uses the same variables, but can list them in any order. Clause width and binary variable-name lengths are unbounded. A clause excludes just one assignment. That last fact supplies a useful timing allowance: while many assignments remain, a small number of unfinished clauses cannot change the answer to UNSAT.

The recognizer uses that allowance to change representations before it becomes urgent. It initially processes each completed clause during the next clause. When its processed prefix leaves four assignments, it constructs explicit dictionaries for those four survivors and catches up. Thereafter each incoming clause is compared directly with four dictionaries while its names arrive. No copied clause or cleanup after input end is needed.

Statement and encoding

Use the ordinary records C(+u,-v,...); from the clause-order investigation. Names are nonempty binary words, with leading zeros significant. Each clause must contain distinct names, and all clauses must have exactly the same support. Repeated clauses are allowed. A repeated name within a clause rejects, even with opposite signs. No whitespace or additional marker is present. The empty conjunction accepts; C(); is unsatisfiable. Malformed or incomplete records reject.

Theorem. Exactly the well-formed satisfiable streams satisfying these checked conditions have a deterministic native scaffolding-automaton recognizer. Consequently their string reversals have PEGs.

The theorem is forward-native; it does not assert reverse-native recognition or solve arbitrary nested supports. One automaton handles every input length, with fixed degree, radius, finite labels and initialization, one new node per actual symbol, and final-state acceptance without an EOF step. No pointer identity, numerical addresses, supplied order, decomposition, padding or advice is used.

Let the nonempty common support have size $b$, with total name length $H$. Every valid clause has exactly

$$L=H+2b+3$$

symbols, regardless of its literal permutation. A master-name FIFO contains $T=H+b$ internal tokens: each name followed by a separator. Thus a complete internal scan fits inside the next clause. Constants in the number of parallel activities are fixed independently of $b,H,L$.

Existing primitives and structural checking

We use the saved strict FIFO, serial finite-payload dictionary, and coverage-spine construction. Each primitive has bounded worst-case observations and allocations; all queues and dictionaries are immutable versions.

During the first clause, build a dictionary of names and reject duplicates. Retain its encounter order in the master FIFO and one token per variable in a width FIFO. During each later clause, query the frozen master dictionary and a fresh current-clause Seen dictionary as bits arrive. At every name delimiter require membership in the master and absence from Seen, mark it, and consume one width token. Require exactly an empty width cursor at clause close. This checks common support and distinctness without sorting or a terminal scan.

While needed, also build a fresh name-to-falsifying-bit dictionary for the current clause. A positive literal contributes bit zero and a negative literal bit one. The next clause supplies the time for a master-order scan of this completed dictionary. Both structural checking and background scans continue in a bounded batch at each actual symbol.

Finite-width coverage with a capped hole count

The initial coverage structure represents the forbidden subset of $\{0,1\}^b$. We need its number of uncovered assignments, capped at five:

$$\gamma(U)=\min(5,|U|).$$

This is a finite payload. It is not an unbounded counter.

A subtree at remaining height $r$ is Blank, Covered, or a spine. Blank has $2^r$ holes; Covered has zero. A spine is a FIFO of frames Frame(a,other,w) ending at Covered, as in the prefix proof. Its holes are the disjoint union of its off-path subtrees’ holes. The second FIFO now carries a bounded number of identical markers per frame:

$$\text{frame contribution}=\gamma(\text{holes of other})\in\{0,1,2,3,4,5\}.$$

The contribution is also stored as the finite payload $w$ of its frame. The marker FIFO is their concatenation in frame order. Its length may be unbounded. Its capped length is obtained by trying at most five dequeues on a copied cursor, leaving the stored queue intact. Therefore

$$\gamma(\text{holes of spine})=\min(5,\text{marker length}).$$

The identity holds because $\min(5,\sum_i\min(5,h_i))=\min(5,\sum_i h_i)$. An empty marker queue means the whole spine is covered and is canonicalized to Covered.

To expose a spine, dequeue its first frame and then its contribution, at most five markers. The remaining queues describe the continuing child; five-token lookahead gives its exact capped hole count. The other child is the stored immutable reference. This avoids subtracting from a saturated scalar, which would be incorrect. All suffixes retain the full filtered-marker invariant.

Exposing Blank requires the remaining-height cursor. A cap of five alone does not determine its children’s caps. Along any master-order traversal, the width FIFO is advanced once per coordinate. After advancing, inspect at most three tokens of a copied remaining cursor: heights zero, one, two and at least three give child caps one, two, four and five respectively. Store the appropriate cap on the blank child reference. No numerical height is needed.

For insertion, traverse the completed clause’s falsifying assignment in master order, enqueuing each unchosen subtree and its at-most-five markers. If an already covered subtree is reached, the assignment was already forbidden; leave the root unchanged. Otherwise replace the depth-$b$ tip by Covered and publish the new spine. Root count is immediately available from five-marker lookahead. There is no upward walk. Each new distinct assignment removes exactly one hole; a duplicate removes none.

At initialization the blank root’s cap is found while counting the first clause’s variables only up to three. It is five when $b\ge3$. The fixed-width interpretation is established after that clause, before its assignment is inserted by the background worker.

Enumerating four holes without a global walk

When a frozen coverage root has cap four, it has exactly four holes. Number them zero through three in master-coordinate lexicographic order. Run four independent root cursors, one for each finite rank.

At a coordinate, expose the current node. If its left child’s capped count exceeds the rank, descend left. Otherwise descend right after subtracting the left count. Subtraction happens only when that count is at most the rank, so it is an exact integer at most three. An underestimated saturated value is never subtracted. The chosen subtree always contains the desired rank.

The width cursor supplies blank-child heights. In parallel, the master-name scan inserts the chosen bit into that rank’s name-to-bit dictionary. Choose the bit before processing that name’s first internal bit; commit the dictionary entry at its separator. Four simultaneous traversals require only a fixed number of primitive calls per token. At the end of the $T$-token scan, four complete, distinct assignment dictionaries are ready. They describe exactly the holes of the frozen snapshot.

The enumeration reads one root-to-leaf path per rank, not all trie nodes. Shared subtrees, long spines and discarded older versions do not change the bound. References are followed through labeled fields, never compared for identity.

The transition schedule

First suppose $b\ge3$, so at least eight assignments initially exist. Number actual clauses starting at one.

In the initial phase, process clause $i$ in master order during actual clause $i+1$. The arriving clause simultaneously builds its own sign dictionary and passes structural validation. All scans take $T<L$ token steps. At a complete record boundary there is at most one clause not yet included in the coverage root.

As long as the processed root has more than four holes, that one clause cannot eliminate them all. Acceptance at that boundary is therefore correct even though the stored root is one record behind. The first clause alone is also satisfiable.

Suppose processing clause $j$ first makes the root cap at most four. Its exact hole count is four: the preceding count was at least five, and one insertion removes at most one hole. Freeze this root and stop inserting further assignments into it. The worker finishes while actual clause $j+1$ is arriving.

During $j+3$, two parallel master scans query the two completed sign dictionaries and the four candidate dictionaries. These determine which candidates each saved clause forbids. At the same time, actual incoming name bits query the four candidate dictionaries; four finite equality flags determine whether the arriving clause forbids any candidate. The two internal jobs finish before record end. At the delimiter, remove the union of these match sets from the four-bit mask.

All later incoming clauses use the latter direct comparison. A clause can remove only its identical candidate. Duplicate clauses do nothing after their candidate has been removed. There is no rebuilding of a large structure in this phase.

This schedule stores at most two pending completed clauses at transition. Starting enumeration at the next record boundary avoids any assumption about how early the threshold was discovered inside $j+1$. If input stops during a record it is malformed and rejects. If it stops at either of the first two complete transition boundaries, the lower bounds in the table already certify SAT. Thus no unprocessed work is needed to decide the stopped input.

Zero, one or two variables

Small supports cannot wait for the threshold transition. During the first clause, build four candidate dictionaries in parallel. Candidate index $q\in\{0,1,2,3\}$ supplies its low-order index bits to the first and second encountered names. A finite register records the first clause’s falsifying pattern and whether a third name occurred.

If the first clause closes with $b=1$ or $2$, retain only candidate indices below $2^b$ and remove that pattern. These retained candidates enumerate all assignments exactly once. Subsequent clauses use direct comparison from the outset. If a third name appears, abandon this small-support construction and use the large-support phase. The extra work and history are bounded per input symbol. For $b=0$, the first record is the empty clause and makes the formula unsatisfiable; the empty input remains accepting.

Correctness, storage and native compilation

Induction on the background insertions gives exactly the forbidden assignment set of the processed prefix. The weighted-marker invariant gives its capped complement size at every exposed suffix. Before conversion, at most one additional point is missing from that representation, so its positive slack certifies SAT. At conversion, rank enumeration gives exactly the four surviving assignments. Two stored clauses and one streamed clause are then accounted for explicitly. Subsequent candidate removal is exact by induction on records. Structural checking separately ensures that each valid clause really excludes one full assignment on the same coordinates.

The fixed root families comprise the master and width FIFOs, structural dictionaries, the committed/current coverage paths, at most two pending sign dictionaries, four candidate builders or lookup cursors, four hole cursors and the worker/parser state. None of these families grows with $b$. Each actual symbol performs a fixed number of primitive calls: master/Seen lookup, any current dictionary update, bounded FIFO actions, up to four rank or candidate activities, and at most two pending-clause scans. Five-token peeks use copied cursors; their allocations count. Each call has fixed observation radius and a bounded allocation batch. Their fixed composition therefore satisfies the reviewed simultaneous-record compiler contract with some fixed arity, radius and batch bound. No optimized numerical certificate is asserted here.

For actual encoded length $N$, all preparation, background scans, abandoned small-support dictionaries, discarded paths and immutable versions use $O(N)$ logical records. The compiled native machine has $N+1$ physical nodes and literal pointer serialization uses $O(N\log(N+2))$ bits. It is deterministic. The theorem pays for the actual names every time they appear. For equal-length $h$-bit names with $b=2^h$, a stream of $m$ clauses has $N=m(b(h+2)+3)$; enumerating all $2^b$ forbidden assignments is already exponentially long in $b$.

A structurally invalid record need not supply enough time for an internal job. The machine still performs bounded work per actual symbol and latches rejection when the parser or structure check fails. It never accepts an incomplete record. The completion guarantees above are needed only on valid streams, where equal support proves the exact common length.

What changed, and what comes next

The three-paper review identified distinct-assignment occupancy as the useful invariant. The new scheduling step uses a bounded number of pending exclusions while there is a certified surplus of survivors, then changes to a representation whose comparisons follow the actual incoming names. It does not sort the output, contradict the earlier exact-normalization obstruction, or use inverse closure under copying.

The source methods are classical elimination and decision representations; strict queues, dictionaries and the original coverage spines are reused. The specific native contribution is the weighted-marker cap and four-survivor transition schedule. The reviewed papers provide neither this per-symbol schedule nor the single-copy native statement. This is a written construction with independent proof audits and finite semantic checks, not proof-assistant verification.

The next structural test is two nested supports differing by one variable, discovered from the input, followed by bounded differences in width. A shorter clause can remove several survivors, so the point-exclusion timing allowance must be replaced by an explicit bound on each clause’s effect. Arbitrary nested supports remain open: one late short clause can remove an unbounded number of assignments, and its short record also offers less processing time. Both the semantic deletion bound and the available input time must be proved together before extending this theorem.

Finite check: scripts/verify_equal_support_survivors.py passed 5,053 spine versions, 6,724 rank checks and 25,259 stopped pipeline prefixes, with 14,711 permuted-coordinate comparisons. Its tuple queues and Python sets check semantic invariants and phase accounting, not native primitives, costs or the complete character parser. Results: check output.