命题证明系统的可自动化性

验证器回答“这份候选证明对不对”，自动化器回答“没有候选时怎样找到一份接近最佳尺度的证明”。穷举按长度枚举所有串最终会找到最短证明，却要检查约 $2^{s_P(\phi )}$ 个候选，远非 $s_P(\phi )$ 的多项式。可自动化性要求搜索开销与隐藏在输入背后的最短证书同阶可控，而不是仅仅保证迟早成功。

它也不同于p-模拟公理库证明系统的 p-模拟p-simulation of proof systems · Polynomial-time simulation用可多项式时间计算且只产生多项式长度膨胀的证明翻译比较两个命题证明系统。。翻译器拿到一份源系统证明，自动化器只拿到公式。一个系统可以轻易翻译别人已经找到的证明，却仍不知道到哪里寻找第一份证明。证明系统最优性公理库命题证明系统的最优性Optimal proof system · p-optimal proof system以能否统一模拟或 p-模拟所有命题证明系统定义的全局最优性概念。比较最短长度的全局支配关系，同样不自带搜索算法。

对二元 CNF

2-SAT implication graph 同时给出 $x⇝\mathrm{\neg }x$ 与 $\mathrm{\neg }x⇝x$，在线性时间判定不可满足。沿两条路径回溯子句，可输出归结证书：前两式归结得 $y$，后两式归结得 $\mathrm{\neg }y$，再得到空子句。对 2-CNF 这一受限输入类，判定算法与证书重建都为多项式时间，所以它展示了一次真实自动化流程。

这个例子不能证明一般 resolution 可自动化。一般 CNF 上可以枚举所有至多宽度 $w$ 的子句，数量约为 $\sum _{i\le w}{2}^i(\genfrac{}{}{0ex}{}{n}{i})$；当最短证明宽度是常数时这给出高效搜索，但 $w$ 随 $n$ 增长后不再是相对最短证明长度的固定多项式。已知 hardness 结果表明，一般 resolution 自动化会带来标准复杂度假设下不可信的算法后果。

还有一种标准的较弱口径：若存在可自动化系统 $Q$，且 $Q$ 在证明长度上多项式模拟 $P$，即某个固定多项式 $q$ 满足 $s_Q(\phi )\le q(s_P(\phi ))$，则称 $P$ 弱可自动化。算法找到的是 $Q$-证明，而非原来的 $P$-证明；它只需利用短 $Q$-证明的存在，所以定义本身不要求拿到一份 $P$-证明再高效翻译。p-模拟公理库证明系统的 p-模拟p-simulation of proof systems · Polynomial-time simulation用可多项式时间计算且只产生多项式长度膨胀的证明翻译比较两个命题证明系统。 $P{\le }_{p}Q$ 是充分但更强的条件；无论采用哪种口径，方向写反都无法从短 $P$-证明推出短 $Q$-证明。

证明搜索器、SAT 求解器和 theorem prover 都可用 automatizability 作理想化基准，但工程上的平均速度不等于最坏情况下的输出敏感保证。启发式算法可能在基准实例上迅速找到证明，却在某个拥有短证明的输入族上搜索指数久；这正是定义试图排除的情况。反过来，算法在不可满足实例上找不到短 resolution 证明，也可能因为所选系统本身没有短证明，而非搜索策略差。

可行插值把自动化与学习、分离电路联系起来：在适当系统中，高效搜索短证明可能导出高效构造 interpolant 的算法，进而触及电路下界。对 Frege 和更强系统的自动化问题仍高度开放；对 resolution 已有条件不可自动化与 NP-hardness 结果。引用这些结果时应保留其随机化、近似因子、promise 和参数化假设，不能把论文标题缩写成无条件的 $\mathrm{P}\ne \mathrm{NP}$ 定理。