Dependency Stochastic Boolean Satisfiability: A Logical Formalism for NEXPTIME Decision Problems with Uncertainty

Authors

  • Nian-Ze Lee Graduate Institute of Electronics Engineering, National Taiwan University
  • Jie-Hong R. Jiang Department of Electrical Engineering, National Taiwan University

Keywords:

Satisfiability, Other Foundations of Reasoning under Uncertainty, Other Foundations of Constraint Satisfaction, Constraint Satisfaction

Abstract

Stochastic Boolean Satisfiability (SSAT) is a logical formalism to model decision problems with uncertainty, such as Partially Observable Markov Decision Process (POMDP) for verification of probabilistic systems. 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 the 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. We demonstrate the potential applications of DSSAT to circuit synthesis of probabilistic and approximate design. Furthermore, to study the descriptive power of DSSAT, we establish a polynomial-time reduction from Dec-POMDP to DSSAT. With the theoretical foundations paved in this work, we hope to encourage the development of DSSAT solvers for potential broad applications.

Downloads

Published

2021-05-18

How to Cite

Lee, N.-Z., & Jiang, J.-H. R. (2021). Dependency Stochastic Boolean Satisfiability: A Logical Formalism for NEXPTIME Decision Problems with Uncertainty. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5), 3877-3885. Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/16506

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization