References & Citations
Computer Science > Logic in Computer Science
Title: Dependency Stochastic Boolean Satisfiability: A Logical Formalism for NEXPTIME Decision Problems with Uncertainty
(Submitted on 11 Nov 2019 (this version), latest version 25 Feb 2021 (v3))
Abstract: 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.
Submission history
From: Jie-Hong Jiang [view email][v1] Mon, 11 Nov 2019 06:58:25 GMT (26kb)
[v2] Fri, 17 Jul 2020 03:16:23 GMT (177kb,D)
[v3] Thu, 25 Feb 2021 08:46:47 GMT (816kb,D)
Link back to: arXiv, form interface, contact.