A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps Conference Paper

Author(s): Chatterjee, Krishnendu; Chmelík, Martin; Davies, Jessica
Title: A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps
Affiliation IST Austria
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 EXPTIMEcomplete, 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. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
Keywords: Standard model; Symbolic algorithms; Target state; Uncertain environments; nocv1; Efficient encoding; exponential reduction; memory strategies; probabilistic planning; engineering main heading: artificial intelligence
Conference Title: AAAI: Conference on Artificial Intelligence
Publisher: AAAI Press  
Date Published: 2016-12-02
Start Page: 3225
End Page: 3232
Notes: Technical Report: https://repository.ist.ac.at/362/
Open access: yes (repository)
IST Austria Authors
  1. Martin Chmelik
    23 Chmelik
Related IST Austria Work