2007/01/09 by Nathan Segerlind, Segerlind, Nathan
Computer Science · #Computational Complexity (cs.CC) #F.2.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #cs.CC #cs.LO #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.cs/0701054
40 pages, 3 figures. First public draft, comments welcome. Also submitted at ECCC
arxiv created 2007/01/09 · openalex publication_date 2007/01/09 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We demonstrate a family of propositional formulas in conjunctive normal form so that a formula of size N requires size 2^Ω(√[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.