A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs

Authors

  • Krishnendu Chatterjee IST Austria
  • Martin Chmelík IST Austria
  • Jessica Davies IST Austria

DOI:

https://doi.org/10.1609/aaai.v30i1.10422

Keywords:

POMDPs, SAT, Uncertainty in AI, Planning under Uncertainty

Abstract

POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIME-complete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach.

Downloads

Published

2016-03-05

How to Cite

Chatterjee, K., Chmelík, M., & Davies, J. (2016). A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. Proceedings of the AAAI Conference on Artificial Intelligence, 30(1). https://doi.org/10.1609/aaai.v30i1.10422

Issue

Section

Technical Papers: Reasoning under Uncertainty