SharpSSAT: A Witness-Generating Stochastic Boolean Satisfiability Solver


  • Yu-Wei Fan National Taiwan University
  • Jie-Hong R. Jiang National Taiwan University



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 & Optimization


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.




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.



AAAI Technical Track on Constraint Satisfaction and Optimization