Paper: The Complexity of Resolution Refinements (at LICS 2003)

Authors: Joshua Buresh-Oppenheim Toniann Pitassi

Abstract

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.

BibTeX

  @InProceedings{BureshOppenheimPita-TheComplexityofReso,
    author = 	 {Joshua Buresh-Oppenheim and Toniann Pitassi},
    title = 	 {The Complexity of Resolution Refinements},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)},
    year =	 {2003},
    month =	 {June}, 
    pages =      {138--147},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }