@inproceedings{1166,
  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.},
  author       = {Chatterjee, Krishnendu and Chmelik, Martin and Davies, Jessica},
  booktitle    = {Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence},
  location     = {Phoenix, AZ, USA},
  pages        = {3225 -- 3232},
  publisher    = {AAAI Press},
  title        = {{A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps}},
  volume       = {2016},
  year         = {2016},
}

@misc{5443,
  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.},
  author       = {Chatterjee, Krishnendu and Chmelik, Martin and Davies, Jessica},
  issn         = {2664-1690},
  pages        = {23},
  publisher    = {IST Austria},
  title        = {{A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs}},
  doi          = {10.15479/AT:IST-2015-325-v2-1},
  year         = {2015},
}