The stochastic Boolean satisfiability (SSAT) problem was introduced by Papadimitriou in 1985 by adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, e.g., in probabilistic planning and, more recently by integrating arithmetic, in probabilistic model checking. In this paper, we first present a new result on the computational complexity of SSAT: SSAT remains PSPACE-complete even for its restriction to 2CNF. Second, we propose a sound and complete resolution calculus for SSAT complementing the classical backtracking search algorithms. © 2010 Springer-Verlag.
CITATION STYLE
Teige, T., & Fränzle, M. (2010). Resolution for stochastic Boolean satisfiability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6397 LNCS, pp. 625–639). Springer Verlag. https://doi.org/10.1007/978-3-642-16242-8_44
Mendeley helps you to discover research relevant for your work.