TQBF 的 PSPACE 完全性

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

公式

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

若量词交替层数固定，问题落在多项式层级相应层；TQBF 允许随输入增长的多次交替，才达到 PSPACE 完全。公式编码必须避免在递归归约中指数展开，常用共享结构或分治可达性维持多项式长度。

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 展示了固定交替和多项式交替之间的能力跃迁。

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