SAT Tableaux and Quantified-Space Completeness: Examples

Let $a_0=(q_0,0)$, $a_1=(q_1,\bigsqcup )$, $a_2=(q_{\mathrm{a}\mathrm{c}\mathrm{c}},0)$ and $B=\bigsqcup$. Set $X_{0,0,a_0}=X_{1,1,a_1}=X_{2,0,a_2}=1$, $X_{1,0,0}=1$, and select $B$ in all other cells. In every cell the positive symbol disjunction has one true term, and every pairwise exclusion has at least one true negated term. All initial units and the three right-guard units $X_{t,3,B}$ are 1. The final accepting disjunction has its $(j,a)=(0,0)$ term true.

The outputs required by the local rule at cells 0 through 3 for the first transition are $0,a_1,B,B$, and for the second are $a_2,B,B,B$. At cell zero the first tuple is $(\mathrm{\#},a_0,B,0)$; at cell one it is $(a_0,B,B,a_1)$. In the second transition the corresponding tuples are $(\mathrm{\#},0,a_1,a_2)$ and $(0,a_1,B,B)$. Here $\mathrm{\#}$ denotes the fixed exterior marker and contributes no Boolean literal. These four tuples follow the two table entries; cells two and three remain unmarked blanks because no head moves into them. Every forbidden-tuple clause therefore has at least one selected-symbol premise false, or its forbidden output false, and evaluates to 1.

Change just the first successor cell zero from unmarked 0 to unmarked 1, retaining one-hot encoding. The tuple $(\mathrm{\#},a_0,B,1)$ is forbidden, and its explicit clause $\mathrm{\neg }{X}_{0,0,a_0}\vee \mathrm{\neg }{X}_{0,1,B}\vee \mathrm{\neg }{X}_{1,0,1}$ now has values $0\vee 0\vee 0=0$. Thus the correct assignment satisfies every clause whereas this altered assignment fails an actual local clause. F2 identifies the satisfying tableau with the stated two-step accepting run; for any larger allowed bound simply repeat its last row and add blank columns.

Set $(x,y,z)=(1,0,0)$. Then $F=(1\cdot 1)\vee 0=1$. Its computed extension is $(u,v,w)=(1,1,1)$. The nine clause values in order are $1,1,1,1,1,1,1,1,1$. More generally, for any original assignment with $F=1$, setting $u=1-y$, $v=xu$, $w=\max (v,z)=1$ satisfies the gate clauses and final unit.

Conversely the first two clauses force $u=1-y$. The next three force $v=xu$, and the following three force $w=\max (v,z)$. The last clause forces $w=1$, whence $F=1$. For example $(x,y,z)=(0,1,0)$ has forced gate values $(0,0,0)$, so the last clause fails and there is no satisfying extension.

The satisfying original assignment from step 1.1 with the inconsistent extension $(u,v,w)=(0,0,0)$ still makes $F$ true, since $F$ does not mention fresh variables, but makes both $u\vee y$ and the unit $w$ false. Thus the enlarged formula is not equivalent to $F$ on arbitrary assignments to all six variables. Its existential projection onto the original variables is exactly $F$, by the two preceding arguments. No choice is required: the valid extension is computed uniquely.

Here $E(X,Y)$ is $(X=00\wedge Y=01)\vee (X=01\wedge Y=10)$ and $R_0(X,Y)$ is $(X=Y)\vee E(X,Y)$. Thus $R_0(00,10)=0$, $R_0(00,01)=1$ and $R_0(01,10)=1$. In $R_1(00,10)$ choose midpoint $Z=01$. The selector $b=0$ forces only $R_0(00,01)$ and $b=1$ forces only $R_0(01,10)$; all endpoint pairs not selected by the guard make the implication automatically true. Hence $R_1(00,10)=1$.

For general $m$-bit vertices, each level adds three $m$-bit vectors and one selector, so depth $d$ has $(3m+1)d$ new bound bits. At $m=2,d=2$ this is 14 bits. If $B$ is the base formula's occurrence count, the one-copy count is at most $B+Cdm$ for a fixed expansion constant $C$. The duplicated midpoint recursion instead satisfies $D_{i+1}=2D_i+O(m)$, with $2^{d}B$ base occurrences. At $d=m$, the former is polynomial after variable-name encoding, whereas the latter already contains $2^m$ base copies.

For $R_1(00,11)$, the first selected pair can satisfy $R_0(00,Z)$ only for $Z=00$ or $01$. But $R_0(00,11)=R_0(01,11)=0$, so the second selected pair fails in either case. For $Z=10$ or $11$ the first pair already fails. These are all four midpoints, proving $R_1(00,11)=0$. Equality also gives $R_0(11,11)=1$ despite the absence of outgoing edges.

If the encoded final formula has length $N$, a depth-first quantifier evaluator uses a table of at most $N$ variable bits, at most $N$ frames each holding an $O(\log (N+2))$ position and one saved answer, and polynomial space for matrix parsing. Even storing a whole length-$N$ residual formula per frame costs at most $O(N^2)$ cells. After the first child returns, only its answer bit is needed while reusing child storage for the second. It does not store the whole binary evaluation tree. At depth zero it simply evaluates $R_0$. These concrete bounds explain why an exponential number of possible assignments does not imply exponential workspace.