---
_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.
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.'
  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, USA: AAAI Press.'
  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.
  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,
    USA, 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.
  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, USA
  name: 'AAAI: Conference on Artificial Intelligence'
  start_date: 2016-02-12
date_created: 2018-12-11T11:50:30Z
date_published: 2016-12-02T00:00:00Z
date_updated: 2023-02-23T12:26:41Z
day: '02'
department:
- _id: KrCh
- _id: ToHe
ec_funded: 1
intvolume: '      2016'
language:
- iso: eng
month: '12'
oa_version: None
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 2016
year: '2016'
...
---
_id: '5443'
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 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.
alternative_title:
- IST Austria Technical Report
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. <i>A Symbolic SAT-Based Algorithm for Almost-Sure
    Reachability with Small Strategies in POMDPs</i>. IST Austria; 2015. doi:<a href="https://doi.org/10.15479/AT:IST-2015-325-v2-1">10.15479/AT:IST-2015-325-v2-1</a>
  apa: Chatterjee, K., Chmelik, M., &#38; Davies, J. (2015). <i>A symbolic SAT-based
    algorithm for almost-sure reachability with small strategies in POMDPs</i>. IST
    Austria. <a href="https://doi.org/10.15479/AT:IST-2015-325-v2-1">https://doi.org/10.15479/AT:IST-2015-325-v2-1</a>
  chicago: Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. <i>A Symbolic
    SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs</i>.
    IST Austria, 2015. <a href="https://doi.org/10.15479/AT:IST-2015-325-v2-1">https://doi.org/10.15479/AT:IST-2015-325-v2-1</a>.
  ieee: K. Chatterjee, M. Chmelik, and J. Davies, <i>A symbolic SAT-based algorithm
    for almost-sure reachability with small strategies in POMDPs</i>. IST Austria,
    2015.
  ista: Chatterjee K, Chmelik M, Davies J. 2015. A symbolic SAT-based algorithm for
    almost-sure reachability with small strategies in POMDPs, IST Austria, 23p.
  mla: Chatterjee, Krishnendu, et al. <i>A Symbolic SAT-Based Algorithm for Almost-Sure
    Reachability with Small Strategies in POMDPs</i>. IST Austria, 2015, doi:<a href="https://doi.org/10.15479/AT:IST-2015-325-v2-1">10.15479/AT:IST-2015-325-v2-1</a>.
  short: K. Chatterjee, M. Chmelik, J. Davies, A Symbolic SAT-Based Algorithm for
    Almost-Sure Reachability with Small Strategies in POMDPs, IST Austria, 2015.
date_created: 2018-12-12T11:39:22Z
date_published: 2015-11-06T00:00:00Z
date_updated: 2023-02-21T16:24:05Z
day: '06'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-325-v2-1
file:
- access_level: open_access
  checksum: f0fa31ad8161ed655137e94012123ef9
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:05Z
  date_updated: 2020-07-14T12:46:57Z
  file_id: '5466'
  file_name: IST-2015-325-v2+1_main.pdf
  file_size: 412379
  relation: main_file
file_date_updated: 2020-07-14T12:46:57Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: '23'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '362'
related_material:
  record:
  - id: '1166'
    relation: later_version
    status: public
status: public
title: A symbolic SAT-based algorithm for almost-sure reachability with small strategies
  in POMDPs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...