A Sharp Leap from Quantified Boolean Formula to Stochastic Boolean Satisfiability Solving
Journal
35th AAAI Conference on Artificial Intelligence, AAAI 2021
Journal Volume
5A
Pages
3697-3706
Date Issued
2021
Author(s)
Abstract
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. Copyright © 2021, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
Other Subjects
Artificial intelligence; Benchmarking; Learning systems; Stochastic systems; Boolean formula satisfiability; Decision problems; Expensive models; Model Counting; PSPACE-complete; Quantified Boolean formulas; Satisfiability solvers; Satisfiability solving; Stochastic boolean satisfiability; Uncertainty; Boolean functions
Type
conference paper