随机限制法的归结下界

随机限制是一种受控显微镜。它冻结大量变量，擦掉与目标无关的子句，却希望把原公式的“硬骨架”留在未赋值变量上。对一份假设中的短证明，宽子句含许多文字，随机赋值很容易让其中某个文字为真，从而整行消失；即使没有被满足，通常也只剩少量未定文字。公式和证明同时经历同一个限制，因此不能任意挑一份只破坏证明、不尊重输入的赋值。

难点不在写出 $\rho$，而在平衡两个概率。冻结太多变量，证明确实会坍缩，但公式也可能直接被满足或只剩平凡矛盾；保留太多变量，困难核心仍在，宽证明行却未必缩小。优良的分布常利用公式的匹配、扩张或鸽巢结构，而不是对所有变量机械独立赋值。

对子句

取 $\rho (x)=0,\rho (y)=1,\rho (z)=\ast$，前两个文字为假，故 $C\upharpoonright \rho =z$；若改成 $\rho (y)=0$，文字 $\mathrm{\neg }y$ 为真，整条子句被删除。若每个变量以概率 $p$ 保持未定，其余时等概率取 $0,1$，那么恰有 $k$ 个文字幸存且没有文字满足的概率为

对宽度为 $w$ 且无互补文字的子句成立。对 $k>t$ 求和便能估计该子句限制后仍很宽的概率，再乘以假设证明的行数做联合界。

归结步骤在限制下可能退化。若从 $A\vee x$ 与 $B\vee \mathrm{\neg }x$ 推出 $A\vee B$，而 $\rho (x)=1$，第一前提已满足，第二前提缩成 $B$，结论限制后至少可由 $B$ 经 weakening 获得；整理证明时应保留较强父句，而不是要求原三行仍逐字构成一次 resolution。忽略这种剪枝会错误宣称限制操作不保证明。

方法的边界也很明确：联合界只能控制所假设的有限条证明行，不能一次排除指数多条潜在子句；困难性保存需要针对具体公式族另证。随机限制给出存在某个好限制，通常不直接产出确定性 SAT 算法。

Haken 对鸽巢原理的经典指数归结下界开创了瓶颈计数路线；Beame–Pitassi 随后用随机限制给出更简洁、改进的归结下界，后来的工作又把这套方法与宽度、扩张和 switching 思想系统化。切换引理公理库Håstad switching lemmaHåstad's switching lemma · Switching lemma说明窄 CNF 或 DNF 在独立随机限制后，以指数高概率退化为浅决策树的结构定理。也研究随机限制如何简化布尔结构，但其典型对象是小宽度 DNF/CNF 与决策树；把电路下界中的结论直接套到 resolution 行上，必须核对分布与证明封闭性。

这套方法还提示下界设计原则：公式应在大幅固定变量后仍留下同类型的小实例，证明行却不具备同样的自相似保护。鸽巢、Tseitin 和随机约束族分别用匹配、奇偶守恒与扩张性实现这种张力。具体指数取决于存活变量数、单行失败概率和困难核心参数，不能用“随机限制通常会简化”代替计算。