SAT 2004 START ConferenceManager    


Combining Component Caching and Clause Learning for Effective Model Counting

Tian Sang, Fahiem Bacchus, Paul Beame, Henry Kautz, Toniann Pitassi

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

Model counting methods that cache the number of satisfying assignments of connected components of the residual formula were recently proposed by Bacchus, Dalmao, and Pitassi as solutions for #SAT and Bayes net evaluation. These component caching methods were shown theoretically to be at least competitive with previous methods, and to be better on certain inputs. However, it was not clear whether the overhead of component caching would outweigh its benefits in practice.

We show how to combine the ideas of component caching with clause learning in zchaff, a state-of-the-art SAT solver, and build a solver for #SAT that is orders of magnitude better on many problems, both random and structured, than previous #SAT solvers. We resolve some subtle interactions between component caching and clause learning that are far from apparent and can compromise the values returned if handled incorrectly.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com