SharpSSAT: A Witness-Generating Stochastic Boolean Satisfiability Solver
Abstract
Stochastic Boolean satisfiability (SSAT) is a formalism allowing decision-making for optimization under quantitative constraints. Although SSAT solvers are under active development, existing solvers do not provide Skolem-function witnesses, which are crucial for practical applications. In this work, we develop a new witness-generating SSAT solver, SharpSSAT, which integrates techniques, including component caching, clause learning, and pure literal detection. It can generate a set of Skolem functions witnessing the attained satisfying probability of a given SSAT formula. We also equip the solver ClauSSat with witness generation capability for comparison. Experimental results show that SharpSSAT outperforms current state-of-the-art solvers and can effectively generate compact Skolem-function witnesses. The new witness-generating solver may broaden the applicability of SSAT to practical applications.
BibTeX
@article{Fan_Jiang_2023, title={SharpSSAT: A Witness-Generating Stochastic Boolean Satisfiability Solver}, volume={37}, url={https://ojs.aaai.org/index.php/AAAI/article/view/25509}, DOI={10.1609/aaai.v37i4.25509}, abstractNote={Stochastic Boolean satisfiability (SSAT) is a formalism allowing decision-making for optimization under quantitative constraints. Although SSAT solvers are under active development, existing solvers do not provide Skolem-function witnesses, which are crucial for practical applications. In this work, we develop a new witness-generating SSAT solver, SharpSSAT, which integrates techniques, including component caching, clause learning, and pure literal detection. It can generate a set of Skolem functions witnessing the attained satisfying probability of a given SSAT formula. We also equip the solver ClauSSat with witness generation capability for comparison. Experimental results show that SharpSSAT outperforms current state-of-the-art solvers and can effectively generate compact Skolem-function witnesses. The new witness-generating solver may broaden the applicability of SSAT to practical applications.}, number={4}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Fan, Yu-Wei and Jiang, Jie-Hong R.}, year={2023}, month={Jun.}, pages={3949-3958} }