loading...
Memoization and DPLL: Formula Caching Proof Systems
Aarhus, Denmark July 07-July 10
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CCC.2003.121442518th Annual IEEE Conference on Comput ...
 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 
 
Paul Beame, Russell Impagliazzo, Toniann Pitassi, Nathan Segerlind, "Memoization and DPLL: Formula Caching Proof Systems," Computational Complexity, Annual IEEE Conference on, pp. 248, 18th Annual IEEE Conference on Computational Complexity (CCC'03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/CCC.2003.1214425,
author = {Paul Beame and Russell Impagliazzo and Toniann Pitassi and Nathan Segerlind},
title = {Memoization and DPLL: Formula Caching Proof Systems},
journal ={Computational Complexity, Annual IEEE Conference on},
volume = {0},
year = {2003},
issn = {1093-0159},
pages = {248},
doi = {http://doi.ieeecomputersociety.org/10.1109/CCC.2003.1214425},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computational Complexity, Annual IEEE Conference on
TI - Memoization and DPLL: Formula Caching Proof Systems
SN - 1093-0159
SP
EP
A1 - Paul Beame,
A1 - Russell Impagliazzo,
A1 - Toniann Pitassi,
A1 - Nathan Segerlind,
PY - 2003
KW - null
VL - 0
JA - Computational Complexity, Annual IEEE Conference on
ER -
 
Paul Beame, University of Washington
Russell Impagliazzo, UC, San Diego
Toniann Pitassi, University of Toronto
Nathan Segerlind, UC, San Diego
A fruitful connection between algorithm design and proof complexity is the formalization of the DPLL approach to satisfiability testing in terms of tree-like resolution proofs. We consider extensions of the DPLL approach that add some version of memoization, remembering formulas the algorithm has previously shown unsatisfiable. Various versions of such formula caching algorithms have been suggested for satisfiability and stochastic satisfiability ([10, 1]). We formalize this method, and characterize the strength of various versions in terms of proof systems. These proof systems seem to be both new and simple, and have a rich structure. We compare their strength to several studied proof systems: tree-like resolution, regular resolution, general resolution, and Res(k). We give both simulations and separations.
Citation:
Paul Beame, Russell Impagliazzo, Toniann Pitassi, Nathan Segerlind, "Memoization and DPLL: Formula Caching Proof Systems," ccc, pp.248, 18th Annual IEEE Conference on Computational Complexity (CCC'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.