loading...
The Complexity of Resolution Refinements
Ottawa, Canada June 22-June 25
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2003.121005318th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Joshua Buresh-Oppenheim, University of Toronto
Toniann Pitassi, University of Toronto
Resolution is the most widely studied approach to propositional theorem proving. In developing efficient resolution-based algorithms, dozens of variants and refinements of resolution have been studied from both the empirical and analytic sides. The most prominent of these refinements are: DP (ordered), DLL (tree), semantic, negative, linear and regular resolution. In this paper, we characterize and study these six refinements of resolution. We give a nearly complete characterization of the relative complexities of all six refinements. While many of the important separations and simulations were already known, many new ones are presented in this paper; in particular, we give the first separation of semantic resolution from general resolution. As a special case, we obtain the first exponential separation of negative resolution from general resolution. We also attempt to present a unifying framework for studying all of these refinements.
Citation:
Joshua Buresh-Oppenheim, Toniann Pitassi, "The Complexity of Resolution Refinements," lics, pp.138, 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.