2005 · 223 citations · 20 references
ComputingComputer ScienceAlgorithmsSchedulingTheory Of ComputationAutomated ReasoningBayesian InferenceBayesian StatisticsConstraint Satisfaction#P-complete ProblemsBayesian NetworksComplete ProblemsModel-based AlgorithmsNp-complete ProblemsNp-completenessSatisfiabilitySatisfiability Problem
SAT algorithms have proven effective for CSPs such as planning and scheduling, and compilation to SAT has become both practically and theoretically valuable, with component caching enabling efficient model counting. The study investigates whether compiling to SAT can be a practical method for solving real‑world #P‑complete problems, specifically Bayesian inference. The authors translate Bayesian networks into weighted model counting, extend state‑of‑the‑art model‑counting algorithms to handle weights, devise a single‑pass method for computing all marginals, and evaluate the approach on challenging reasoning tasks. Recently, Sang et al.
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 (Kautz and Selman 2003). Solving such NP-complete tasks by compilation to has turned out to be an approach that is of both practical and theoretical interest. Recently, (Sang et al. 2004) have 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 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.
20
A machine program for theorem-proving
Martin Davis, George Logemann, Donald Loveland · Communications of the ACM · 1962 · 3.2K citations · Full text
GRASP - A New Search Algorithm for Satisfiability
1996 · 860 citations
Efficient Conflict Driven Learning in a Boolean Satisfiability Solver
2001 · 666 citations
Using CSP look-back techniques to solve real-world SAT instances
Roberto J. Bayardo, Robert Schrag · 1997 · 598 citations
Bucket elimination: A unifying framework for reasoning
Rina Dechter · Artificial Intelligence · 1999 · 593 citations