Paper Info
Title
On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs
Abstract
We show that tree-like OBDD proofs of unsatisfiability require an exponential increase (s 7! 2s(1)) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase (s 7! 22(log s)(1)) in proof size to simulate Res (O(log n)). The "OBDD proof system" that we consider has lines that are ordered binary decision diagrams in the same variables as the input formula, and is allowed to combine two previously derived OBDDs by any sound inference rule. In particular, this system abstracts satisfiability algorithms based upon explicit construction of OBDDs and satisfiability algorithms based upon symbolic quantifier elimination.
Year
DOI
Venue
2007
10.1109/CCC.2008.34
CCC '08 Proceedings of the 2008 IEEE 23rd Annual Conference on Computational Complexity
Keywords
DocType
ISSN
proof size,relative efficiency,exponential increase,ordered binary decision diagram,obdd proof system,log n,unrestricted obdd proof,almost-exponential increase,unrestricted resolution,tree-like obdd proof,system abstracts satisfiability algorithm,satisfiability algorithm,resolution-like proofs,inference rule,satisfiability,quantifier elimination,lower bound,color,computational complexity,computational modeling,algorithm design and analysis,resolution,formal verification,interpolation,construction industry,software performance,boolean functions,data structures,computability
Journal
1093-0159
Citations 
PageRank 
References 
4
0.46
26
Authors
1
Name
Order
Citations
PageRank
Nathan Segerlind122311.22