TQBF 的 PSPACE 完全性

TQBF 在布尔公式前加入交替量词，求值过程像一场有限完全信息博弈：存在量词表示“计算者选择一个可行分支”，由一方选择使公式为真；全称量词表示“两个分支都必须成立”，由另一方选择反驳，最终无量词公式决定胜负。交替量词能用多项式长度描述指数大的搜索树，而深度优先遍历量词树只需保存当前赋值路径，所以属于 PSPACE；困难性则把任意多项式空间计算的配置可达性递归压缩成量词公式。

公式

为真，因为取 $x=1$ 后任意 $y$ 都满足；而 $\mathrm{\forall }x\mathrm{\exists }y(x\wedge y)$ 为假，因为当 $x=0$ 时无 $y$ 可补救。递归求值每层只保存一个变量选择与子公式位置；朴素展开整棵赋值树需要指数时间，但不需要指数空间。

若量词交替层数固定，问题落在多项式层级相应层；TQBF 允许随输入增长的多次交替，才达到 PSPACE 完全。公式编码必须避免在递归归约中指数展开。这里使用下面的量词选择构造，输出仍是普通公式树，而不偷偷改成允许共享子图的电路编码。

用一个选择位保留一份子公式 ​

固定判定某个 PSPACE 语言的机器和输入 $x$，取多项式位数 $b=b(|x|)$ 编码完整配置。合法性 $\mathsf{Valid}(u)$、接受状态 $\mathsf{Acc}(u)$ 和一步关系 ${\mathsf{Step}}_x(u,v)$ 都有可在多项式时间写出的布尔公式：枚举固定转移表及可能带头位置，逐格检查读写和其余位置不变。输入 $x$ 固定写进这些测试；不需要列出指数多个完整配置。

沿用Savitch 中点递归理路Savitch 定理Savitch's theorem通过配置可达性的中点递归与工作区复用，把非确定空间 s 确定化为平方空间。的“至多 $2^i$ 步”口径，先令

对 $i>0$，取每层都新鲜的 $b$ 位向量 $m,p,q$ 与一个布尔位 $c$，定义

向量量词是对每一位量化，向量相等是逐位相等的合取。$m$ 在 $c$ 之前选择，所以两个挑战必须使用同一个中点；$p,q$ 在选位之后被等式强制成对应端点。因而 $c=0$ 核对前半路径，$c=1$ 核对后半路径，恰好表达两半都可达。反向把两半路径拼接，正向沿路径选中点；长度不足半程时用零长度路径补齐。这给出按 $i$ 的双向归纳。 若把 $\mathrm{\forall }c$ 移到 $\mathrm{\exists }m$ 前面，就改变了问题：在两个不同且无边相连的配置 $u,v$ 上，前半挑战可选 $m=u$，后半挑战可选 $m=v$，两次都靠零路径通过，却没有从 $u$ 到 $v$ 的路径。

关键在于 $R_{i-1}$ 的文本只出现一次。每层增加 $O(b)$ 个逻辑符号，展开到 $i=b$ 后共有 $O(b^2)$ 个新增符号，变量编号的位编码只再带来多项式因子。最后输出闭公式

合法配置数不超过 $2^b$；若有接受路径，去环后便不超过这个长度预算。因此公式为真当且仅当机器接受 $x$。初始配置、接受测试和递归文本均能在多项式时间写出，才真正完成多项式归约，而不仅说明存在一份语义正确的巨大公式。Håstad 讲义 Theorem 7.17 及后面的选择位展开给出这一标准构造。

TQBF 是 PSPACE 对应的典型完全问题：规划、博弈和模型检测中的交替选择可归约到它。若 TQBF 有多项式时间算法，则 $\mathrm{P}=\mathrm{PSPACE}$，并使其间所有已知包含类一同坍缩。

它以PSPACE理路复杂度类 PSPACEComplexity class PSPACE可由确定性图灵机在多项式空间内判定的语言类。为上界，以多项式时间归约理路多项式时间归约Polynomial-time reduction · Karp reduction用一个多项式时间可计算的变换把问题 A 的实例转换为问题 B 的实例。建立困难性，并把命题逻辑理路命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。扩展为量词逻辑。与多项式层级理路多项式层级Polynomial hierarchy · PH由交替存在和全称多项式证书或逐层 NP 预言机构成的复杂性层级。对比，TQBF 展示了固定交替和多项式交替之间的量词预算差别；这不证明 PH 与 PSPACE 严格不同。

在交互式证明路线中，TQBF 还是连接空间计算与随机验证的桥梁：先用算术化理路算术化Arithmetization把布尔关系嵌入有限域低次多项式，使离散正确性声明可由随机代数恒等式检查。把量词递归变成受控次数的多项式关系，再由sum-check 协议理路Sum-check 协议Sum-check protocol · Sumcheck protocol以逐变量低次多项式承诺和随机挑战验证 Boolean cube 上指数项多项式求和的交互协议。逐层核验，最终得到IP = PSPACE理路IP = PSPACEIP equals PSPACE · Shamir's theorem多项式时间随机交互验证恰好能够判定全部多项式空间语言。。这些页面分别承担代数编码、协议检查和复杂度类等价的完整论证，本页只定位这条证明主线。