A Sharp Leap from Quantified Boolean Formula to Stochastic Boolean Satisfiability Solving
Keywords:Solvers and Tools, Satisfiability, Search, Probabilistic Programming
AbstractStochastic 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.
How to Cite
Chen, P.-W., Huang, Y.-C., & Jiang, J.-H. R. (2021). A Sharp Leap from Quantified Boolean Formula to Stochastic Boolean Satisfiability Solving. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5), 3697-3706. https://doi.org/10.1609/aaai.v35i5.16486
AAAI Technical Track on Constraint Satisfaction and Optimization