Model Counting using Component Caching and Clause Learning

Papers

Combining Component Caching and Clause Learning for Effective Model Counting. Tian Sang, Fahiem Bacchus, Paul Beame, Henry Kautz, and Toniann Pitassi. Seventh International Conference on Theory and Applications of Satisfiability Testing, Vancouver, Canada, 2004.

Heuristics for Fast Exact Model Counting.  Tian Sang, Paul Beame, and Henry Kautz.  Eighth International Conference on Theory and Applications of Satisfiability Testing, Edinburgh, Scotland, 2005.

Performing Bayesian Inference by Weighted Model Counting, Tian Sang, Paul Beame, and Henry Kautz.  Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05), Pittsburgh, PA, 2005.

• Benchmark problems from this paper

Downloads

• cachet-wmc-1-21 (July 2005). Updated since to compile under Linux with warnings as of August 2015.

Credits

• Cachet was implemented by Tian Sang at the University of Washington Department of Computer Science & Engineering.
• Cachet uses code from the satisfiability solver zChaff by S. Malik at Princeton University.
• The creation of Cachet was supported by the National Science Foundation under Grant No. 0120307. This software is provided "as is" without warranty of any kind, either express or implied.

Comments and questions

Email Henry Kautz <kautz@cs.washington.edu> and Tian Sang <sang@cs.washington.edu>