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

K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.

Download
No fulltext has been uploaded. References only!
Conference Paper | Published | English
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.
Publishing Year
Date Published
2016-12-02
Proceedings Title
Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence
Volume
2016
Page
3225 - 3232
Conference
AAAI: Conference on Artificial Intelligence
Conference Location
Phoenix, AZ, USA
Conference Date
2016-02-12 – 2016-02-17
IST-REx-ID

Cite this

Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. Vol 2016. AAAI Press; 2016:3225-3232.
Chatterjee, K., Chmelik, M., & Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (Vol. 2016, pp. 3225–3232). Phoenix, AZ, USA: AAAI Press.
Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016:3225–32. AAAI Press, 2016.
K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps,” in Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ, USA, 2016, vol. 2016, pp. 3225–3232.
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.
Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, vol. 2016, AAAI Press, 2016, pp. 3225–32.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar