loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
18th Annual IEEE Symposium on Logic in Computer Science (LICS'03)
The Complexity of Resolution Refinements
Ottawa, Canada
June 22-June 25
ISBN: 0-7695-1884-2
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.