Stochastic Boolean Satisfiability for Two-Player Sequential Games under Uncertainty

Abstract

Stochastic Boolean satisfiability (SSAT) provides a compact framework for PSPACE-complete decision-making under uncertainty. Despite the theoretical inclusion of universal quantifiers (∀), existing solvers typically restrict inputs to random (R ) and existential (∃) quantifiers, limiting applications to single-player games against nature. In this work, we generalize SSAT to include universal quantification, enabling the modeling of competitive two-player games under uncertainty. Theoretically, we establish a reduction from finite two-player zero-sum stochastic games with perfect information to general SSAT. Unlike QBF-based solvers that yield binary deterministic outcomes, our approach computes rational-valued Nash equilibrium payoffs as satisfying probabilities. Practically, we extend SharpSSAT to create the first solver capable of handling all three quantifier types. It supports equilibrium value computation and generates strategies for both players (Skolem for ∃ and Herbrand for ∀). By utilizing an implicit representation, our solver offers a more scalable alternative to traditional explicit-state game theory algorithms. Experimental results demonstrate that our solver effectively reasons about complex stochastic adversarial interactions that were previously difficult to encode.