Dependency Stochastic Boolean Satisfiability: A Logical Formalism for NEXPTIME Decision Problems with Uncertainty
share
Stochastic Boolean Satisfiability (SSAT) is a logical formalism to model decision problems with uncertainty, such as Partially Observable Markov Decision Process (POMDP). SSAT, however, is limited by its descriptive power within the PSPACE complexity class. More complex problems, such as the NEXPTIME-complete Decentralized POMDP (Dec-POMDP), cannot be succinctly encoded with SSAT. To provide a logical formalism of such problems, we generalize Dependency Quantified Boolean Formula (DQBF), a representative problem in the NEXPTIME-complete class, to its stochastic variant, named Dependency SSAT (DSSAT), and show that DSSAT is also NEXPTIME-complete. To demonstrate the descriptive power of DSSAT, we further establish a polynomial-time reduction from Dec-POMDP to DSSAT. Our results may encourage DSSAT solver development to enable potential broad applications.
READ FULL TEXT