conference paper published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Martin Chmelik author 3624234E-F248-11E8-B48F-1D18A9856A87 Jessica Davies author 378E0060-F248-11E8-B48F-1D18A9856A87 KrCh department ToHe department AAAI: Conference on Artificial Intelligence Modern Graph Algorithmic Techniques in Formal Verification project Rigorous Systems Engineering project Quantitative Graph Games: Theory and Applications project 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. AAAI Press2016Phoenix, AZ, United States eng 1511.0845610.1609/aaai.v30i1.10422 20163225 - 3232 https://research-explorer.ista.ac.at/record/5443 https://dl.acm.org/citation.cfm?id=3016355 Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs. In: <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>. Vol 2016. AAAI Press; 2016:3225-3232. doi:<a href="https://doi.org/10.1609/aaai.v30i1.10422">10.1609/aaai.v30i1.10422</a> K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232. K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs,” in <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, Phoenix, AZ, United States, 2016, vol. 2016, pp. 3225–3232. Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in POMDPs.” <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, vol. 2016, AAAI Press, 2016, pp. 3225–32, doi:<a href="https://doi.org/10.1609/aaai.v30i1.10422">10.1609/aaai.v30i1.10422</a>. Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in POMDPs.” In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i>, 2016:3225–32. AAAI Press, 2016. <a href="https://doi.org/10.1609/aaai.v30i1.10422">https://doi.org/10.1609/aaai.v30i1.10422</a>. Chatterjee, K., Chmelik, M., &#38; Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs. In <i>Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence</i> (Vol. 2016, pp. 3225–3232). Phoenix, AZ, United States: AAAI Press. <a href="https://doi.org/10.1609/aaai.v30i1.10422">https://doi.org/10.1609/aaai.v30i1.10422</a> Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for almost sure reachability with small strategies in POMDPs. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2016, 3225–3232. 11662018-12-11T11:50:30Z2025-06-25T11:52:14Z