Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability

TL;DR

This paper proves nearly-exponential lower bounds on the size of symbolic quantifier elimination algorithms and OBDD-based proofs of unsatisfiability for certain propositional formulas, showing fundamental limitations of these methods.

Contribution

It establishes the first nearly-exponential size lower bounds for all variable orderings and schedules in OBDD-based proof systems, extending previous results.

Findings

Refutes using size $2^{ ext{Omega}( oot7{rac{N}{ ext{log}N}})}$ for formulas of size $N$

Lower bounds apply universally across variable orderings and elimination schedules

Results demonstrate fundamental limitations of symbolic quantifier elimination algorithms

Abstract

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.