TY - JOUR AU - Chen, Pei-Wei AU - Huang, Yu-Ching AU - Jiang, Jie-Hong R. PY - 2021/05/18 Y2 - 2024/03/28 TI - A Sharp Leap from Quantified Boolean Formula to Stochastic Boolean Satisfiability Solving JF - Proceedings of the AAAI Conference on Artificial Intelligence JA - AAAI VL - 35 IS - 5 SE - AAAI Technical Track on Constraint Satisfaction and Optimization DO - 10.1609/aaai.v35i5.16486 UR - https://ojs.aaai.org/index.php/AAAI/article/view/16486 SP - 3697-3706 AB - Stochastic Boolean Satisfiability (SSAT) is a powerful representation for the concise encoding of quantified decision problems with uncertainty. While it shares commonalities with quantified Boolean formula (QBF) satisfiability and has the same PSPACE-complete complexity, SSAT solving tends to be more challenging as it involves expensive model counting, a.k.a. Sharp-SAT. To date, SSAT solvers, especially those imposing no restrictions on quantification levels, remain much lacking. In this paper, we present a new SSAT solver based on the framework of clause selection and cube distribution previously proposed for QBF solving. With model counting integrated and learning techniques strengthened, our solver is general and effective. Experimental results demonstrate the overall superiority of the proposed algorithm in both solving performance and memory usage compared to the state-of-the-art solvers on a number of benchmark formulas. ER -