Computer Science – Computational Complexity
Scientific paper
2007-01-09
Computer Science
Computational Complexity
40 pages, 3 figures. First public draft, comments welcome. Also submitted at ECCC
Scientific paper
We demonstrate a family of propositional formulas in conjunctive normal form so that a formula of size $N$ requires size $2^{\Omega(\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.
No associations
LandOfFree
Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-722866