Skip to main content
SpringerLink
Log in

Model Counting Using the Inclusion-Exclusion Principle

  • Conference paper
Theory and Applications of Satisfiability Testing - SAT 2011 (SAT 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6695))

Abstract

The inclusion-exclusion principle is a well-known mathematical principle used to count the number of elements in the union of a collection of sets in terms of intersections of sub-collections.We present an algorithm for counting the number of solutions of a given k-SAT formula using the inclusion-exclusion principle. The key contribution of our work consists of a novel subsumption pruning technique. Subsumption pruning exploits the alternating structure of the terms involved in the inclusion-exclusion principle to discover term cancellations that can account for the individual contributions of a large number of terms in a single step.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

References

  1. Bennett, H., Sankaranarayanan, S.: Model counting using the inclusion-exclusion principle, Draft (available upon request) (2011)

    Google Scholar 

  2. Gomes, C.P., Sabharwal, A., Selman, B.: Model counting. In: Handbook of Satisfiability, ch. 20. IOS Press, Amsterdam (2008)

    Google Scholar 

  3. Iwama, K.: CNF-satisfiability test by counting and polynomial average time. SIAM Journal on Computing 18(2), 385–391 (1989)

    Article  MATH  Google Scholar 

  4. Lozinskii, E.L.: Counting propositional models. Information Processing Letters 41, 327–332 (1992)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Colorado, Boulder, CO., USA

    Huxley Bennett & Sriram Sankaranarayanan

Authors
  1. Huxley Bennett
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sriram Sankaranarayanan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Michigan, 48109, Ann Arbor, MI, USA

    Karem A. Sakallah

  2. LRI / CNRS UMR8623 / INRIA Saclay, Univ Paris-Sud, F-91405, Orsay, France

    Laurent Simon

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bennett, H., Sankaranarayanan, S. (2011). Model Counting Using the Inclusion-Exclusion Principle. In: Sakallah, K.A., Simon, L. (eds) Theory and Applications of Satisfiability Testing - SAT 2011. SAT 2011. Lecture Notes in Computer Science, vol 6695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21581-0_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-21581-0_30

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-21580-3

  • Online ISBN: 978-3-642-21581-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation