---
OA_place: repository
OA_type: green
_id: '1166'
abstract:
- lang: eng
  text: 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.
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
  Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307:
  Graph Games), and Microsoft faculty fellows award.'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
- first_name: Jessica
  full_name: Davies, Jessica
  id: 378E0060-F248-11E8-B48F-1D18A9856A87
  last_name: Davies
citation:
  ama: '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>'
  apa: '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>'
  chicago: 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>.
  ieee: 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.
  ista: '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.'
  mla: 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>.
  short: K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI
    Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.
conference:
  end_date: 2016-02-17
  location: Phoenix, AZ, United States
  name: 'AAAI: Conference on Artificial Intelligence'
  start_date: 2016-02-12
corr_author: '1'
date_created: 2018-12-11T11:50:30Z
date_published: 2016-12-02T00:00:00Z
date_updated: 2025-06-25T11:52:14Z
day: '02'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1609/aaai.v30i1.10422
ec_funded: 1
external_id:
  arxiv:
  - '1511.08456'
intvolume: '      2016'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.48550/arXiv.1511.08456
month: '12'
oa: 1
oa_version: Preprint
page: 3225 - 3232
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence
publication_status: published
publisher: AAAI Press
publist_id: '6191'
quality_controlled: '1'
related_material:
  link:
  - relation: table_of_contents
    url: https://dl.acm.org/citation.cfm?id=3016355
  record:
  - id: '5443'
    relation: earlier_version
    status: public
status: public
title: A symbolic SAT based algorithm for almost sure reachability with small strategies
  in POMDPs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2016
year: '2016'
...