Abstract
Stochastic Boolean Satisfiability (SSAT) is a powerful formalism to represent computational problems with uncertainty, such as belief network inference and propositional probabilistic planning.
Solving SSAT formulas lies in the PSPACEcomplete complexity class same as solving Quantified Boolean Formulas (QBFs). While many endeavors have been made to enhance QBF solving
in recent years, SSAT has drawn relatively less attention. This paper focuses on random-exist quantified SSAT formulas, and proposes an algorithm
combining modern satisfiability (SAT) techniques
and model counting to improve computational ef-
ficiency. Unlike prior exact SSAT algorithms, the
proposed method can be easily modified to solve
approximate SSAT by deriving upper and lower
bounds of satisfying probability. Experimental results show that our method outperforms the stateof-the-art algorithm on random k-CNF and AIrelated formulas in both runtime and memory usage, and has effective application to approximate
SSAT on VLSI circuit benchmarks