SharpSSAT: A Witness-Generating Stochastic Boolean Satisfiability Solver
DOI:
https://doi.org/10.1609/aaai.v37i4.25509Keywords:
CSO: Satisfiability, CSO: Constraint Optimization, CSO: Constraint Satisfaction, CSO: Other Foundations of Constraint Satisfaction & Optimization, CSO: Search, CSO: Solvers and Tools, SO: Other Foundations of Search & OptimizationAbstract
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.Downloads
Published
2023-06-26
How to Cite
Fan, Y.-W., & Jiang, J.-H. R. (2023). SharpSSAT: A Witness-Generating Stochastic Boolean Satisfiability Solver. Proceedings of the AAAI Conference on Artificial Intelligence, 37(4), 3949-3958. https://doi.org/10.1609/aaai.v37i4.25509
Issue
Section
AAAI Technical Track on Constraint Satisfaction and Optimization