Stochastic Boolean Satisfiability

Michael L. Littman, Stephen M. Majercik, and Toniann Pitassi

Abstract: Satisfiability problems and probabilistic models are core topics
of artificial intelligence and computer science.  This paper looks at the
rich intersection between these two areas, opening the door for the use of
satisfiability approaches in probabilistic domains.  The paper examines a
generic stochastic satisfiability problem, SSAT, which can function for
probabilistic domains as SAT does for deterministic domains.  It shows the
connection between SSAT and well studied problems in belief network
inference and planning under uncertainty, and defines algorithms, both
systematic and stochastic, for solving SSAT instances.  These algorithms
are validated on random SSAT formulae generated under the fixed-clause
model.  In spite of the large complexity gap between SSAT (PSPACE) and SAT
(NP), the paper suggests that much of what we have learned about SAT
transfers to the probabilistic domain.