SharpSSAT: A Witness-Generating Stochastic Boolean Satisfiability Solver

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.

Authors

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

Keywords

• CSO: Constraint Optimization
• CSO: Constraint Satisfaction
• CSO: Other Foundations of Constraint Satisfaction & Optimization
• CSO: Satisfiability
• CSO: Search
• CSO: Solvers and Tools
• SO: Other Foundations of Search & Optimization