Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Algebraic Simplification Techniques for Propositional Satisfiability

  • Conference paper
  • First Online:
Principles and Practice of Constraint Programming – CP 2000 (CP 2000)

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

Abstract

The ability to reduce either the number of variables or clauses in instances of the Satisfiability problem (SAT) impacts the expected computational effort of solving a given instance. This ability can actually be essential for specific and hard classes of instances. The objective of this paper is to propose new simplification techniques for Conjunctive Normal Form (CNF) formulas. Experimental results, obtained on representative problem instances, indicate that large simplifications can be observed.

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
$34.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
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping 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. J. F. Groote and J. P. Warners. The propositional formula checker heerhugo. Technical Report SEN-R9905, CWI, January 1999.

    Google Scholar 

  2. C.-M. Li. Integrating equivalency reasoning into davis-putnam procedure. In Proceedings of the National Conference on Artificial Intelligence, August 2000. Accepted for publication.

    Google Scholar 

  3. J. P. Marques-Silva. Algebraic simplification techniques for propositional satisfiability. Technical Report RT/01/2000, INESC, March 2000.

    Google Scholar 

  4. G. Stålmarck. A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula, 1989. Swedish Patent 467 076 (Approved 1992), US Patent 5 276 897 (approved 1994), European Patent 0 403 454 (approved 1995).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Informatics, Technical University of Lisbon, IST/INESC/CEL, Lisbon, Portugal

    João Marques-Silva

Authors
  1. João Marques-Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of California at Irvine, Irvine, CA, 92697, USA

    Rina Dechter

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Marques-Silva, J. (2000). Algebraic Simplification Techniques for Propositional Satisfiability. In: Dechter, R. (eds) Principles and Practice of Constraint Programming – CP 2000. CP 2000. Lecture Notes in Computer Science, vol 1894. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45349-0_45

Download citation

  • DOI: https://doi.org/10.1007/3-540-45349-0_45

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41053-9

  • Online ISBN: 978-3-540-45349-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation