SAT Tableaux and Quantified-Space Completeness

Suppose an allowed certificate gives acceptance at time $s\le T$. Write its initial row, then its ordinary successor rows through $s$, then repeat its accepting row through $T$. Set exactly the variables for these symbols to 1. The initial tape length is less than $T$, and at time $t$ the head is at most $t$, so cell $T+1$ stays blank. Every local tuple is allowed: at the old head it performs the prescribed write, at the destination it receives the new head, and elsewhere it preserves the symbol. At zero the rule uses the clamped move. After halting it preserves the whole row. Thus every clause is true, including the final accepting clause.

Conversely, from a satisfying assignment the exactly-one clauses select a unique symbol in each cell. The initial-row clauses give one ordinary initial configuration with a certificate of the required length. Consider any decoded row already known to be a genuine padded configuration. It has one head. For each cell its three old symbols therefore have no conflicting heads; the local rule has exactly the unique output obtained from the ordinary transition, or from halting repetition. Any different new symbol would make the forbidden-tuple clause for these actual four symbols false: all its negated literals would be zero. Consequently the whole next row equals that padded successor.

Starting with row zero and applying the preceding implication $T$ times proves that every row is the actual padded run. The last clause locates an accepting head at time $T$. Rejection cannot become acceptance because a rejected row only repeats; a nonhalting run can acquire an accepting state only through a genuine transition. Deleting the repeated terminal rows therefore gives an accepting computation of length at most $T$. The verifier's own syntax check makes its certificate permitted.

This proves both implications, including empty inputs and zero-length certificates. The construction uses a positive padded bound, so no absent predecessor row is invoked; a hypothetical already-accepting row would simply repeat, while the actual initial state is nonhalting. Every symbol was read from a finite assignment or explicitly written from a run, so there is no choice assumption.

Put $a=\mathrm{\mid }A\mathrm{\mid }$, a constant of the fixed verifier. There are $a(T+1)(T+2)$ cell variables. Each cell contributes one size-$a$ clause and at most $a(a-1)\mathrm{/}2$ binary clauses. Each update contributes at most $a^4$ clauses of width at most four. The pinning clauses number $O(T^2)$ and the accepting clause has at most $a(T+2)$ literals. Thus the literal count is $O(T^2)$; indices take $O(\log (T+2))$ bits. Enumerate times, cells and the constant symbol tuples with binary counters, and output each clause. Counter arithmetic, the initial input lookup and evaluation of the fixed polynomials cost polynomial time. The binary list headers add only linear overhead in the number of entries.

For completeness, the gate clauses can be written explicitly. For $v=\mathrm{\neg }u$ use $(v\vee u)\wedge (\mathrm{\neg }v\vee \mathrm{\neg }u)$. For $v=u\wedge w$ use $(\mathrm{\neg }v\vee u)\wedge (\mathrm{\neg }v\vee w)\wedge (v\vee \mathrm{\neg }u\vee \mathrm{\neg }w)$. For $v=u\vee w$ use $(v\vee \mathrm{\neg }u)\wedge (v\vee \mathrm{\neg }w)\wedge (\mathrm{\neg }v\vee u\vee w)$. The two possible values of $v$ show that each conjunction holds exactly for the indicated equality: for AND, $v=1$ forces both inputs true and $v=0$ forces at least one false; OR is dual, and NOT forces opposite bits. Constants are pinned by a positive or negative unit clause. Finite list connectives are first expanded as binary trees, using the appropriate constant for an empty list. Finally require the output wire by a unit clause.

Assign gate values in order after a satisfying assignment to the original variables. Each equality clause and the output unit then holds. Conversely any satisfying CNF assignment obeys every gate equality; induction through the acyclic gate order identifies each gate bit with its evaluated value. The output unit makes the original formula true. These arguments also handle an output that is a lone literal or a constant. No assignment to fresh variables is asserted to work unless it obeys the gate equations.

Number the original distinct variables first and new gate variables next, retaining an explicit renaming list; alternatively take new indices above the largest original index. Their bit length is bounded by the input length plus $O(\log (g+2))$ for $g$ gates. There are $O(g)$ clauses after binary expansion, and they can be written by finite scans in polynomial time. Thus the conversion preserves satisfiability in both directions and the tableau's accepting-computation meaning. Zero gates, an empty CNF and an empty clause are handled respectively by the literal output, true constant and false constant rules.

Parse the proposed SAT input. Reject if malformed. Otherwise enumerate distinct variable names by first occurrence, read that many certificate bits and recursively evaluate the formula. There are at most as many variables and nodes as input bits, and even repeated scans and pairwise name comparisons take polynomial time. Accept exactly when evaluation is true. The empty conjunction and true constant need no certificate bits, while an empty clause and false constant never pass. Thus SAT belongs to verifier-defined NP.

Fix the verifier of $L$ and normalize its guarded certificates using the explicit length field. The tableau lemma then gives, for every binary $x$, $x\in L$ iff ${\mathrm{\Phi }}_{M,x}$ is satisfiable. All strings are legitimate source inputs; there is no implicit promise to parse $x$ as a machine or formula. The fixed verifier itself determines any desired rejection of special source encodings.

Output the CNF encoding from F4. Its polynomial construction bound includes the whole input and witness length, and it always returns a well-formed formula. The equivalence in step 1.2 makes this a total many-one reduction to SAT. At length zero the same normalized verifier and enlarged polynomial bound apply; no exceptional input is omitted. Since $L$ was arbitrary, SAT is NP-hard, and step 1.1 proves NP-completeness.

For a clause $l_1\vee \cdots \vee l_m$ with $m>3$, use distinct fresh variables $y_1,\dots ,y_{m-3}$ and replace it by the clauses $l_1\vee l_2\vee y_1$, then $\mathrm{\neg }{y}_j\vee l_{j+2}\vee y_{j+1}$ for $1\le j\le m-4$, then $\mathrm{\neg }{y}_{m-3}\vee l_{m-1}\vee l_m$. All variables used for different clauses are distinct. Leave clauses of lengths zero, one, two and three unchanged.

If the original clause is true, set $y_j=1$ exactly when $l_1,\dots ,l_{j+1}$ are all false. The first clause holds by this definition. In a middle clause, either $y_j=0$, or the first $j+1$ literals are false and then either $l_{j+2}=1$ or $y_{j+1}=1$. In the last clause, either $y_{m-3}=0$ or the first $m-2$ literals are false, forcing one of the last two true. This explicitly extends every satisfying assignment.

If all original literals were false, the first new clause would force $y_1=1$, the middle clauses successively force every next $y_j=1$, and the last would be false. Therefore a satisfying extension implies the original clause is true. For $m=4$ there are no middle clauses and the same first/last argument applies. Separate fresh variables let the extensions be performed for all clauses simultaneously.

The replacement has $m-2$ clauses for a long clause. Summing lengths gives linear literal count; the encoded indices and a finite scan for unused indices give polynomial bit length and construction time. Malformed CNF strings map to the fixed CNF containing an empty clause. To reduce an arbitrary NP language, first use F2's CNF output and then this map; composition of two polynomial running-time bounds is polynomial, and the two membership equivalences compose. Membership in NP guesses one bit per distinct variable and evaluates clauses. Empty CNF remains satisfiable, and any retained empty clause makes both formulas unsatisfiable. Hence 3SAT is NP-complete.

Every head begins at zero and moves by one cell per transition, with a left move at zero unable to leave the right-infinite tape. Hence the cells visited on each tape form an initial segment. A transition writes only at the currently scanned cell, so every unvisited cell retains its initial content. Suppose $S\ge k$. For each tape let $r_i\ge 1$ be the visited prefix length; ${\sum }_i{r}_i\le S$. Encode the state by a fixed-width word, each $r_i$ and head position by a width-$\lceil {\log }_2(S+1)\rceil$ field, and the concatenation of the visited tape prefixes by at most $S\lceil {\log }_2(\mathrm{\mid }\mathrm{\Gamma }\mathrm{\mid }+1)\rceil$ bits. Pad the last field to this fixed length with zeros. Reconstruct the unvisited suffix on tape one from the fixed $x$, and all other unvisited cells as blank. These data recover the full configuration, extending F2's triple to the fixed number of tapes.

To make the map canonical on configurations rather than histories, use on tape $i$ the least prefix containing its head and every cell whose current content differs from its initial content. This prefix is nonempty and no longer than the visited prefix, because writes require a visit. Apply the encoding just described to these canonical prefixes. Their lengths sum to at most $S$, and decoding recovers the exact configuration, so equal codes imply equal configurations. Different histories reaching the same configuration now give the same code.

The code length is at most $c_M+2k\lceil {\log }_2(S+1)\rceil +S\lceil {\log }_2(\mathrm{\mid }\mathrm{\Gamma }\mathrm{\mid }+1)\rceil =O_M(S)$ for $S\ge k\ge 1$. There are at most $2^m$ binary words of a fixed length $m$, proved by doubling the count for each appended bit, starting with one empty word. Hence the number of configurations is at most $2^{O_M(S)}$, in particular the stated weaker bound with the input-length logarithm. If $S<k$, even the initial head cells exceed the bound and the reachable set is empty; there is then a vacuous encoding. Empty input and blank-only tape data need no special extra field. No uniform code independent of the fixed input is claimed for an arbitrary unvisited input suffix.

Parse a TQBF input of length $N$, rejecting violations of the statement's syntax. Keep the parsed formula and a table of assigned bits. Recursively assign the next quantified variable 0, evaluate the remaining prefix, save that answer bit, then assign it 1 and evaluate again using the same child workspace. Combine with OR or AND as indicated and undo the assignment. A frame stores an input position and the saved bit; at most $N$ frames and a size-$O(N^2)$ parsed representation suffice. Matrix evaluation likewise uses at most $O(N^2)$ cells. Every recursive call decreases the remaining prefix length; the finite matrix recursion terminates. The empty prefix evaluates the variable-free matrix directly. Counting input cells as well still gives polynomial space.

Fix a decider $M$ of $L$ and a known integer polynomial $S(n)\ge n+k+1$ bounding its visited cells on every input. On input $x$, represent each tape by its first $S=S(\mathrm{\mid }x\mathrm{\mid })$ symbols and its head offset, together with the state. All actual configurations fit because each tape's visited prefix is at most $S$ and the complete input fits too. Use fixed-width fields and add a tag for one special accepting vertex $a_{\ast }$. Invalid state/symbol codes and head offsets outside $0,\dots ,S-1$ are excluded; the special vertex has all remaining fields zero. Choose one common bit length $m=O_M(S)$ for all these vertices. This is the explicit full-prefix variant of F3's bounded coding. There are at most $2^m$ vertices, including $a_{\ast }$. The initial vertex $s_x$ is written directly from $x$.

Construct a Boolean formula $E(X,Y)$ for edges of this finite graph. For every possible state, scanned-symbol tuple and head-offset tuple, enumerate the finitely specified instruction of $M$, assert those source fields, the target state and the componentwise head offsets (using F4's clamped-left rule on each right-infinite tape), the prescribed written symbols, and equality of every unscanned tape cell. Conjoin validity of both endpoint codes. There are $O_M(S^k)$ cases and $O_M(S)$ field comparisons in each, with $O(\log (S+1))$ bits per offset. Thus the disjunction has polynomial encoded size and is produced by polynomial finite loops. Omit transitions leaving the represented interval. Add edges from every ordinary accepting configuration to $a_{\ast }$, and a self-loop at $a_{\ast }$. Rejecting configurations have no outgoing edges. This supplies a unique terminal target without assuming a physical tape-erasing normalization. From the initial vertex, ordinary edges are exactly M's steps; actual runs never leave the interval. Thus $a_{\ast }$ is reachable exactly when M accepts $x$.

Let $R_0(X,Y)$ be $\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{d}(X)\wedge \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{d}(Y)\wedge (X=Y\vee E(X,Y))$. For each next level introduce fresh $m$-bit vectors $Z,U,V$ and a fresh bit $b$. Set $G=(\mathrm{\neg }b\wedge U=X\wedge V=Z)\vee (b\wedge U=Z\wedge V=Y)$, and define $R_{i+1}(X,Y)=\mathrm{\exists }Z\mathrm{\forall }b\mathrm{\forall }U\mathrm{\forall }V(\mathrm{\neg }G\vee R_i(U,V))$. Here equality means conjunction of bit equalities, each expanded with AND, OR and NOT. There is just one occurrence of $R_i$.

For all bit vectors $X,Y$, $R_i(X,Y)$ holds iff they are valid vertices joined by a path of length at most $2^i$. At level zero this follows from its definition, including the length-zero path. For the successor, a true formula supplies a midpoint $Z$. Specializing the universals to $b=0,(U,V)=(X,Z)$ and $b=1,(U,V)=(Z,Y)$ forces both shorter paths by the induction hypothesis; concatenate them. Conversely split a path of length $h\le 2^{i+1}$ after $\min (h,2^i)$ edges. Both portions have length at most $2^i$, so their midpoint works. For any universal assignment either $G$ is false, making the implication true, or it selects one of these two paths. Invalid midpoints cannot pass either selected base validity condition. This proves the induction in both directions.

Any reachable vertex has a path without a repeated vertex: delete the segment between two equal vertices and retain its subsequent edges, reducing the length until no repetition remains. Its length is less than $2^m$. Therefore $R_m(s_x,a_{\ast })$ is true exactly when $x\in L$. If $s_x$ already equals a target in another instance, the equality part of $R_0$ handles it; here the distinct special tag keeps the actual initial and accepting target separate.

Each recursion level introduces $3m+1$ bound bits and $O(m)$ equality/connective occurrences. Distinct variable names across $m$ levels use $O(\log (m+2))$ bits, so the total encoded size is the polynomial base size plus $O(m^2\log (m+2))$. Put the formula in prenex form without duplication: if $z$ is fresh for $A$, then $A\vee (QzB)$ and $Qz(A\vee B)$ have the same truth value, for either quantifier, by checking whether $A$ is true or false and using the nonempty domain $\{0,1\}$. Apply this identity to pull each inner prefix through its outer guard. Fresh naming prevents capture. Each matrix connective remains once. Finite generation of the base cases, guards and prefix requires polynomial time and space, including substituting constant start/target bits. This proves the total reduction and, with step 1.1, PSPACE-completeness. All selections were finite enumerations or existential witnesses to a single formula; AC is unnecessary.

The same reduction may use a 3CNF or 3DNF matrix if desired. For each gate $v=\mathrm{\neg }u$, use $(v\vee u)\wedge (\mathrm{\neg }v\vee \mathrm{\neg }u)$; for $v=u\wedge w$, use $(\mathrm{\neg }v\vee u)\wedge (\mathrm{\neg }v\vee w)\wedge (v\vee \mathrm{\neg }u\vee \mathrm{\neg }w)$; for OR, dualize the AND clauses. Pin a constant by a unit clause and require the output by a unit clause. These are clauses of width at most three. For each assignment to the old variables, a gate-by-gate induction shows that exactly one assignment to the fresh gate variables satisfies all gate equations, and it satisfies the output unit exactly when $F=1$. This proves the pointwise property rather than inferring it from F7's mere equisatisfiability. Append existential quantifiers for the fresh gate bits after the old prefix; the resulting 3CNF preserves truth through every old quantifier. Alternatively apply this construction to $\mathrm{\neg }F$. Then $F=1$ iff every gate assignment falsifies $C_{\mathrm{\neg }F}$. Append universal gate quantifiers and use the matrix $\mathrm{\neg }{C}_{\mathrm{\neg }F}$, a disjunction of terms each containing at most three literals by De Morgan's laws. These conversions preserve the truth of the quantified formula in both directions, including constant matrices. They do not assert a polynomial DNF for unquantified equality without extra variables.

Here is also precise workspace accounting for generation: with read-only input and write-only output excluded from the auxiliary workspace measure, the fixed-M reduction uses $O_M(\log (n+2))$ auxiliary cells. Compute the fixed polynomial S and m in binary with a constant number of $O(\log (n+2))$-bit registers. The base edge formula is output by loops over k head offsets, finite states/symbols, tape cells and bit positions, all polynomially bounded; k is fixed, so the number of loop registers is constant. Initial-configuration bits are obtained by rescanning x with a binary position counter. Output the prenex prefix with one descending level counter; output the guards in the same order, using the current level to name its endpoint vectors, then the base formula, then the required closing symbols by a counter. The one-copy recurrence never requires storing a stack of levels. Every emitted variable name is computed from its level, vector type and bit offset, all polynomially bounded integers.

If a restricted matrix is requested, generate its gate clauses using rescans of that regular unquantified matrix. Number connective occurrences by their positions. Find a node's children by scanning its prefix-encoded subtree with a pending-child counter: reading a node changes the counter by its arity minus one, and zero marks the end of the subtree. Constants have arity zero. All indices and counters are bounded by the polynomial output length. Each requested matrix symbol can be recomputed by restarting the generator of step 7.2 and counting its output; save the constant number of current position registers on separate tracks. Thus iterating over gate positions and their children uses only a constant number of logarithmic registers, with polynomial repeated-scan time. Output F7's clauses, or their De Morgan negations with the appropriate new quantifiers from step 7.1. This proves regular logspace generation under the explicitly stated input/output-excluding convention, without claiming an all-tape visited-space bound smaller than n.