符号量词消去算法的近指数下界及基于OBDD的不可满足性证明
Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability
摘要：
我们证明了一个家庭的命题公式在合取范式，使一个公式的大小$N$需要大小$2^{Ω(\sqrt[7]{N/logN})}$反驳使用树型OBDD反驳系统Atserias，Kolaitis和Vardi关于所有变量排序。所有已知的符号量词消去算法在不可满足的CNF上运行时都生成树状证明，因此该下限适用于这些算法的运行时。此外，下界推广了早期基于OBDD的不可满足性证明的结果，因为它适用于所有变量排序，它适用于根据任意时间表处理子句时，它适用于通过量化消除变量时。
英文摘要：
We demonstrate a family of propositional formulas in conjunctive normal form so that a formula of size $N$ requires size $2^{Ω(\sqrt[7]{N/logN})}$ to refute using the tree-like OBDD refutation system of Atserias, Kolaitis and Vardi with respect to all variable orderings. All known symbolic quantifier elimination algorithms for satisfiability generate tree-like proofs when run on unsatisfiable CNFs, so this lower bound applies to the run-times of these algorithms. Furthermore, the lower bound generalizes earlier results on OBDD-based proofs of unsatisfiability in that it applies for all variable orderings, it applies when the clauses are processed according to an arbitrary schedule, and it applies when variables are eliminated via quantification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
