loading...
On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs
June 22-June 26
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CCC.2008.342008 IEEE 23rd Annual Conference on C ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Nathan Segerlind, "On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs," Computational Complexity, Annual IEEE Conference on, pp. 100-111, 2008 IEEE 23rd Annual Conference on Computational Complexity, 2008.
 
 
BibTex
x
 
@article{ 10.1109/CCC.2008.34,
author = {Nathan Segerlind},
title = {On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs},
journal ={Computational Complexity, Annual IEEE Conference on},
volume = {0},
year = {2008},
issn = {1093-0159},
pages = {100-111},
doi = {http://doi.ieeecomputersociety.org/10.1109/CCC.2008.34},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computational Complexity, Annual IEEE Conference on
TI - On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs
SN - 1093-0159
SP100
EP111
A1 - Nathan Segerlind,
PY - 2008
KW - propositional proof complexity
KW - resolution
KW - ordered binary decision diagrams
KW - lower bounds
VL - 0
JA - Computational Complexity, Annual IEEE Conference on
ER -
 
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.
Index Terms:
propositional proof complexity, resolution, ordered binary decision diagrams, lower bounds
Citation:
Nathan Segerlind, "On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs," ccc, pp.100-111, 2008 IEEE 23rd Annual Conference on Computational Complexity, 2008
Usage of this product signifies your acceptance of the Terms of Use.