承诺下命题证明的复杂性

我们在命题证明复杂性的框架内，研究在“任何可满足的公式都有许多满足赋值”的承诺下，证明CNF公式不可满足性的问题，其中“许多”代表关于变量数$n$的显式指定函数$\Lam$。为此，我们将不同承诺度量（即不同的$\Lam$）下的命题证明系统作为消解法的扩展来开发。这是通过用公理增强消解法来实现的，这些公理粗略地说可以消除由布尔电路定义的真值赋值集合。随后我们研究了此类系统的复杂性，在不同大小承诺下的消解法之间获得了平均情况下的指数分离：1. 当承诺为$\eps\cd2^n$（对于任意常数$0<\eps<1$）时，消解法对所有不可满足的3CNF公式具有多项式大小的反驳。2. 当承诺为$2^{\delta n}$（且子句数为$o(n^{3/2})$）时（对于任意常数$0<\delta<1$），随机3CNF公式不存在次指数大小的消解法反驳。