Tian Sang, Paul Beame, Henry Kautz
Over the past decade general satisfiability testing algorithms have proven to be surprisingly effective at solving a wide variety of constraint satisfaction problem, such as planning and scheduling. Solving such NP-complete tasks by compilation to SAT has turned out to be an approach that is of both practical and theoretical interest. Recently, it has been shown that state of the art SAT algorithms can be efficiently extended to the harder task of counting the number of models (satisfying assignments) of a formula, by employing a technique called component caching. This paper begins to investigate the question of whether compilation to model-counting could be a practical technique for solving real-world #P-complete problems, in particular Bayesian inference. We describe an efficient translation from Bayesian networks to weighted model counting, extend the best model-counting algorithms to weighted model counting, develop an efficient method for computing all marginals in a single counting pass, and evaluate the approach on computationally challenging reasoning problems.
Content Area: 6. Constraint Satisfaction and Satisfiability
Subjects: 15.2 Constraint Satisfaction; 3.4 Probabilistic Reasoning
Submitted: May 10, 2005