Nested clauses under arbitrary literal order

5 October 2026. A native structural check, an exact normalization obstruction, and a verified-replay construction.

Subsequent result: the survivor construction removes the replay requirement for equal supports. The open-status statements below record this earlier investigation; arbitrary nested supports remain unresolved. Its exact sorting obstruction is unchanged.

The prefix-clause recognizer handles unbounded clause width by tracking forbidden assignment prefixes. It checks that every clause lists a prefix of the same variable sequence. Can that common literal order be removed while the clause supports remain nested?

The unrestricted extension remains open. This investigation isolates a smaller test: every clause uses exactly the same variables, but may list them in any order. Checking that structural condition is native. The remaining SAT problem is exact coverage by distinct assignments. Sorting into the old format cannot meet a fixed output budget per input symbol. An explicitly verified second copy of each clause does supply enough time, giving a positive control on the same ordinary clause alphabet.

Target and exact input contract

Use ordinary signed records C(+u,-v,...);, where names are nonempty binary words, leading zeros matter, and each clause has distinct names. Repetition of a name within one clause rejects as a structural violation, including opposite signs. Repeated clauses are allowed. C(); is the empty clause. There is no whitespace, supplied variable order, decomposition or extra end marker.

The main candidate accepts exactly the well-formed satisfiable streams whose clause supports are pairwise comparable by inclusion. Clause order, literal order, widths and name lengths are arbitrary. Invalid syntax, incomplete records and failed structural conditions reject. The empty conjunction accepts.

A native recognizer means one deterministic scaffolding automaton for all lengths: finite control and labels, fixed degree and observation radius, starting at the unlabelled base and adding one node per input symbol. New edges follow bounded port paths from the previous top, are missing, or point to the new node. Observations are labeled unfoldings, without numerical addresses or pointer-identity tests. Acceptance is the final control state, with no additional computation at input end.

A nonempty clause on $k$ names of lengths $\ell_1,\ldots,\ell_k$ has length

$$L=\sum_i\ell_i+2k+3.$$

The empty clause has length four. All following budgets charge these literal lengths, including repeated records.

The forbidden regions remain laminar

A clause on support $S$ forbids one partial assignment $p:S\to\{0,1\}$. On the final variable set $V$, its forbidden region is

$$E_p=\{a\in\{0,1\}^{V}:a|_S=p\}.$$

If $S\subseteq T$, two such regions are disjoint when their assignments disagree on $S$; otherwise the region specified on $T$ lies inside the one specified on $S$. Nested supports therefore give a laminar family of forbidden regions, regardless of literal order.

Discard duplicate regions and retain the inclusion-maximal ones. They are pairwise disjoint and have the same union as all forbidden regions. Consequently

$$F\text{ is unsatisfiable}\quad\Longleftrightarrow\quad \sum_{E_p\text{ distinct maximal}}2^{-|\operatorname{dom}(p)|}=1.$$

This is the familiar prefix-free coverage calculation in coordinate-independent form. A global coordinate order can be obtained from successive differences of the nested supports. The identity does not construct that order during the input or maintain the maximal regions locally.

Simply adding every clause’s weight is incorrect. Two copies of a unit clause have total raw weight one while their conjunction remains satisfiable. Duplicate suppression and subsumption are essential operations.

Equal supports separate structural checking from coverage

Suppose all clauses have the same support $S$, with $b=|S|$. Each forbidden region is now a single assignment on $S$. SAT is equivalent to having strictly fewer than $2^b$ distinct falsifying assignments.

Native structural control. Equal supports and distinct names per clause can be checked without any common literal order.

During the first clause, use the existing serial-name dictionary to mark each encountered name Seen, rejecting a repeat. Append one token per name to a width FIFO. Freeze both structures when that clause ends.

For each later clause, start a fresh empty Seen dictionary and a cursor on the frozen width FIFO. The arriving bits simultaneously query the fixed master dictionary and the fresh dictionary. At each name delimiter, require membership in the master, reject a current-clause repeat, mark the name and consume one width token. Underflow rejects; at clause close require the token cursor empty.

Every later support is a subset of the master, has no duplicates and has exactly its cardinality, so it equals the master. Conversely, every valid equal-support stream passes. Empty first clauses force all later clauses to be empty. Ordinary parser state handles incomplete records. A fixed number of saved dictionary/FIFO primitives suffices per symbol, so the reviewed simultaneous-record compiler gives a native structural recognizer with $O(N)$ total logical history and $N+1$ physical nodes.

This does not decide coverage. For example,

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

has all four raw sign patterns. In the fixed variable order 0,1, however, its falsifying assignments are $00,10,10,11$. Assignment $01$ still satisfies the formula. Feeding signs into the old coverage trie without coordinating their names gives the wrong answer.

Nor does storing each clause as a name-to-sign dictionary finish the task. The saved dictionary answers a query whose name is supplied serially. It does not provide a constant-time test of extensional equality between two completed dictionaries, or a free ordered traversal of all their entries. Those are additional obligations, not pointer-identity operations.

Exact sorting cannot fit the original clock

Consider the exact normalization function that preserves clause order and rewrites every equal-support clause into the first clause’s variable order, preserving names and signs. There is no deterministic causal append-only transducer computing this function with at most a fixed $K$ output symbols per input symbol and at most a fixed $F$ additional output symbols at input end. This remains true even if internal computation and storage are unrestricted.

Take all $b=2^h$ distinct $h$-bit names $u_1,\ldots,u_b$. The first clause lists them in that order, all positive. The second lists them in reverse order. Its last literal, on $u_1$, has either sign; all its other literals are positive. Each clause has length

$$L=b(h+2)+3,\qquad N=2L.$$

The two inputs agree until that last sign. Their normalized outputs disagree at the first sign of the second clause, so before the distinguishing input sign a correct causal machine can have emitted at most the first clause and C(, a total of $L+2$ symbols. Starting with the distinguishing sign, only $h+3$ input symbols remain. At least $L-2$ output symbols remain, requiring

$$b(h+2)+1\le K(h+3)+F,$$

which fails for sufficiently large $h$. A fixed initial output cannot evade the common-prefix restriction. All inputs in this argument are well-formed equal-support formulas and, for $b\ge2$, satisfiable.

This rules out that exact normalization route through the program’s bounded-output inverse-closure theorem. It does not rule out a different reduction or a native recognizer that maintains an order-independent representation directly.

One verified replay supplies a complete positive control

Define a different, explicit language on the same ordinary alphabet. Records occur in adjacent identical pairs

$$C_1C_1C_2C_2\cdots C_mC_m.$$

Every clause has distinct names, all supports are equal, and the conjunction is satisfiable. The machine checks the pairing literally, including signs, name spelling and punctuation. No copy or favorable order is promised without verification.

Written replay theorem. This paired-record language has a forward native scaffolding recognizer. Its string reversal therefore has a PEG. No single-copy membership or reverse-native theorem is inferred.

Use the structural checker above on each first copy. Also build a fresh dictionary mapping each name to its falsifying bit, and enqueue the complete record in a character FIFO. From the first clause retain a master FIFO of its names, each followed by an internal separator. This fixes an internal coordinate order; subsequent clauses need not use it.

On the second copy perform two bounded activities in parallel:

1. Compare each actual symbol with the character FIFO’s front and dequeue it. A mismatch, premature end or excess symbol rejects.
2. Consume one token from the master FIFO cursor per actual symbol. Its stored name bits drive a read-only lookup in the completed sign dictionary. At an internal name separator, read that name’s falsifying bit and perform one step of the saved prefix-coverage insertion. When the master cursor empties, commit the coverage path using its filtered-marker invariant.

For $b>0$, this internal scan needs

$$T=\sum_{i=1}^{b}|u_i|+b$$

tokens, while the actual replay has $L=T+b+3$ symbols. The full canonical assignment is therefore inserted before the verified replay ends. Initialization and the constant final root replacement also fit this margin. An empty clause is handled directly and makes the conjunction unsatisfiable.

At the end of a verified pair, the coverage root represents exactly the assignments forbidden by all completed first copies, in the master’s order. The next pair starts from this root. The finite controller accepts only between complete pairs, after the copy FIFO has emptied and the coverage job has finished, with an uncovered root and no error. Induction over pairs proves correctness. A first copy by itself is never an accepting terminal position.

The source structures have a fixed number of roots and finite terminal payloads. Each actual symbol invokes only a fixed number of strict FIFO, serial-dictionary and coverage primitives; no equality test on physical pointers or traversal at EOF occurs. Their established bounded observations and allocations compose through the reviewed batch compiler. For total paired input length $M=2\sum_i L_i$, every stored copy, dictionary path, queue version and coverage insertion is charged: $O(M)$ logical history, $M+1$ physical nodes and $O(M\log(M+2))$ bits under literal pointer serialization. The construction is deterministic. All $b$ variables remain accessible; the replay is additional input, not free preparation or advice.

Although duplicating clauses leaves their logical conjunction unchanged, it changes the available input time. The earlier verified-replay investigation already shows that inverse closure under copying cannot be assumed. This control therefore gives no transfer back to the original single-copy language.

Assessment and next decisive question

The original arbitrary-order nested-support recognizer has not been constructed. Three attempted invariants remain incomplete: a raw coverage weight lacks duplicate/subsumption tests; completed sign dictionaries lack immediate whole-assignment comparison; an explicit maximal-region antichain lacks local identification of affected regions. The normalization theorem closes one proposed transfer mechanism. The verified-replay theorem shows precisely how a paid second encounter repairs that mechanism in the equal-support case. None is a language nonrecognition theorem.

Ordyniak, Paulusma and Szeider’s full paper, Section 3, supplies the classical broader context. Its weakly simplicial elimination order permits resolution without increasing the number of clauses. The proof computes the order and then performs elimination on the stored formula; polynomial total work does not establish the serial deadline here. The laminar calculation is elementary prefix coverage. The native controls are applications of the saved dictionary, FIFO, coverage and verified-replay constructions, with the explicit scheduling argument above. These are written, independently audited arguments, not formal verification or a new offline SAT tractability criterion.

The next test is direct single-copy coverage on equal supports, using a representation that need not emit sorted clauses. The accompanying literature review should compare elimination-based counting with compiled representations, checking whether either provides an incrementally maintainable invariant under arbitrary record and literal order. The nested-support target remains broader; verifying its support chain is a separate obligation from the equal-support control.