Solving Exist-Random Quantified Stochastic Boolean Satisfiability via Clause Selection

Solving Exist-Random Quantified Stochastic Boolean Satisfiability via Clause Selection

Nian-Ze Lee, Yen-Shi Wang, Jie-Hong R. Jiang

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Main track. Pages 1339-1345. https://doi.org/10.24963/ijcai.2018/186

Stochastic Boolean satisfiability (SSAT) is an expressive language to formulate decision problems with randomness. Solving SSAT formulas has the same PSPACE-complete computational complexity as solving quantified Boolean formulas (QBFs). Despite its broad applications and profound theoretical values, SSAT has received relatively little attention compared to QBF. In this paper, we focus on exist-random quantified SSAT formulas, also known as E-MAJSAT, which is a special fragment of SSAT commonly applied in probabilistic conformant planning, posteriori hypothesis, and maximum expected utility. Based on clause selection, a recently proposed QBF technique, we propose an algorithm to solve E-MAJSAT. Moreover, our method can provide an approximate solution to E-MAJSAT with a lower bound when an exact answer is too expensive to compute. Experiments show that the proposed algorithm achieves significant performance gains and memory savings over the state-of-the-art SSAT solvers on a number of benchmark formulas, and provides useful lower bounds for cases where prior methods fail to compute exact answers.
Keywords:
Constraints and SAT: Constraint Satisfaction
Constraints and SAT: Constraints and SAT
Constraints and SAT: Constraints: Solvers and Tools
Constraints and SAT: Constraints: Evaluation and Analysis