Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR07-009 | 15th August 2007 00:00

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

RSS-Feed




Revision #1
Authors: Nathan Segerlind
Accepted on: 15th August 2007 00:00
Downloads: 3207
Keywords: 


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.

This version differs from the earlier version in that some of the proofs have been cleaned up and made shorter.


Paper:

TR07-009 | 8th January 2007 00:00

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





TR07-009
Authors: Nathan Segerlind
Publication: 19th January 2007 14:56
Downloads: 2969
Keywords: 


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.


Comment(s):

Comment #1 to TR07-009 | 15th February 2007 06:56

Brief summary of differences between TR07-007 and TR07-009 Comment on: TR07-009





Comment #1
Authors: Nathan Segerlind
Accepted on: 15th February 2007 06:56
Downloads: 3141
Keywords: 


Abstract:

A brief summary the differences between the main results in TR07-007 and TR07-009




ISSN 1433-8092 | Imprint