A Resolution Proof System for Dependency Stochastic Boolean Satisfiability

Dependency stochastic Boolean satisfiability (DSSAT), which generalizes stochastic Boolean satisfiability (SSAT) and dependency quantified Boolean formula (DQBF), is a new logical formalism that allows compact encoding of NEXPTIME decision problems under uncertainty. Despite potentially broad applications, a decision procedure for DSSAT remains lacking. In this work, we present the first sound and complete resolution calculus for DSSAT. The resolution system deduces the maximum satisfying probability of a DSSAT formula and provides a witnessing certificate. We also show that when the special case of SSAT formulas is considered, the DSSAT resolution calculus p-simulates a known SSAT resolution scheme. Our result may pave a theoretical foundation for further development and certification of DSSAT solvers.