符号量化消去算法及基于 OBDD 的不可满足性证明的近指数级规模下界

我们展示了一族合取范式命题公式，使得大小为 $N$ 的公式在使用 Atserias、Kolaitis 和 Vardi 的树状 OBDD 反驳系统并针对所有变量顺序进行反驳时，需要 $2^{\Omega(\sqrt[7]{N/logN})}$ 的规模。所有已知的用于可满足性的符号量化消去算法在不可满足的 CNF 上运行时都会生成树状证明，因此该下界适用于这些算法的运行时间。此外，该下界推广了先前关于基于 OBDD 的不可满足性证明的结果，因为它适用于所有变量顺序，适用于根据任意调度处理子句的情况，并且适用于通过量化消去变量的情况。