SpringerLink
Log in

Space Bounds for Resolution

  • Conference paper
  • First Online:
STACS 99 (STACS 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1563))

Included in the following conference series:

Abstract

We introduce a new way to measure the space needed in a resolution refutation of a CNF formula in propositional logic. With the former definition [6] the space required for the resolution of any unsatisfiable formula in CNF is linear in the number of clauses. The new definition allows a much finer analysis of the space in the refutation, ranging from constant to linear space. Moreover, the new definition allows to relate the space needed in a resolution proof of a formula to other well studied complexity measures. It coincides with the complexity of a pebble game in the resolution graphs of a formula, and as we show, has strong relationships to the size of the refutation. We also give upper and lower bounds on the space needed for the resolution of unsatisfiable formulas.

Supported by ESPRIT LTR Project 20244, ALCOM-IT and CICYT Project TIC97-1475-CE, KOALA: DGES PB95-0787, SGR: CIRIT 1997SGR-00366

Partially supported by the DFG

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 85.59
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 106.99
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Aharoni, R., Linial, N.: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. Journal of Combinatorial Theory, 43 (1986) 196–204.

    Article  MATH  MathSciNet  Google Scholar 

  2. Beame, P., Pitassi, T.: Simplified and Improved Resolution Lower Bounds. Proc. 37th IEEE Symp. on Foundations of Computer Science, 37 (1996) 274–282.

    MathSciNet  Google Scholar 

  3. Chvátal, V., Szemerédi, E.: Many hard examples for resolution. Journal of the ACM, 35 (1988) 759–768.

    Article  MATH  Google Scholar 

  4. Esteban, J.L.: Complejidad de la resolución en espacio y tiempo. Masters thesis. Facultad de Informática de Barcelona. 1995.

    Google Scholar 

  5. Haken, A.: The intractability of resolution. Theoretical Computer Science. 39,2–3 (1985) 297–308

    Article  MATH  MathSciNet  Google Scholar 

  6. Kleine-Büning, H., Lettmann, T.: Aussagenlogik: Deduktion und Algorithmen. B.G. Teubner. Stuttgart. 1994.

    Google Scholar 

  7. Pudlák, P.: Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. The Journal of Symbolic Logic. 62,3 (1997) 981–998.

    Article  MATH  MathSciNet  Google Scholar 

  8. Savage, J.: Models of Computation. Addison-Wesley. 1998.

    Google Scholar 

  9. Schöning, U.: Resolution proofs, exponential bounds and Kolmogorov complexity. In Proc. 22nd MFCS Conference, Springer Verlag LNCS. 1295 (1997) 110–116.

    Google Scholar 

  10. Urquhart, A.: Hard examples for resolution. Journal of the ACM. 34 (1987) 209–219.

    Article  MATH  MathSciNet  Google Scholar 

  11. van Emde Boas, P., van Leeuwen, J.: Move rules and trade-offs in the pebble game. In Proc. 4th GI Conference, Springer Verlag LNCS. 67 (1979) 101–112.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. Llenguatges i sistemes informàtics, Universitat Politècnica de Catalunya, c/ Jordi Girona Salgado 1-3, 28023, Barcelona, Spain

    Juan Luis Esteban

  2. Abt. Teoretische Informatik, Universität Ulm Oberer Eselsberg, 89069, Ulm, Germany

    Jacobo Torán

Authors
  1. Juan Luis Esteban
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jacobo Torán
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. FB IV - Informatik, Universität Trier, D-54286, Trier, Germany

    Christoph Meinel

  2. LIFL, Université de Lille I, Bătiment 3, F-59655, Villeneuve d’Ascq Cedex, France

    Sophie Tison

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Esteban, J.L., Torán, J. (1999). Space Bounds for Resolution. In: Meinel, C., Tison, S. (eds) STACS 99. STACS 1999. Lecture Notes in Computer Science, vol 1563. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49116-3_52

Download citation

  • DOI: https://doi.org/10.1007/3-540-49116-3_52

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65691-3

  • Online ISBN: 978-3-540-49116-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation