[{"_id":"5443","pubrep_id":"362","status":"public","type":"technical_report","ddc":[],"creator":{"id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","login":"dernst"},"date_updated":"2023-02-21T16:24:05Z","file_date_updated":"2020-07-14T12:46:57Z","department":[{"_id":"KrCh","tree":[{"_id":"ResearchGroups"},{"_id":"IST"}]}],"oa_version":"Published Version","abstract":[{"lang":"eng"}],"month":"11","alternative_title":[],"language":[{}],"file":[{"checksum":"f0fa31ad8161ed655137e94012123ef9","file_id":"5466","access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T11:53:05Z","file_name":"IST-2015-325-v2+1_main.pdf","creator":"system","date_updated":"2020-07-14T12:46:57Z","file_size":412379}],"publication_status":"published","publication_identifier":{"issn":[]},"related_material":{"record":[{"relation":"later_version","status":"public","id":"1166"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Chatterjee, K., Chmelik, M., & Davies, J. (2015). A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. IST Austria. https://doi.org/10.15479/AT:IST-2015-325-v2-1","short":"K. Chatterjee, M. Chmelik, J. Davies, A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs, IST Austria, 2015.","ieee":"K. Chatterjee, M. Chmelik, and J. Davies, A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. IST Austria, 2015.","mla":"Chatterjee, Krishnendu, et al. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria, 2015, doi:10.15479/AT:IST-2015-325-v2-1.","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.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-325-v2-1."},"dini_type":"doc-type:other","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jessica","id":"378E0060-F248-11E8-B48F-1D18A9856A87","last_name":"Davies"}],"oa":1,"dc":{"title":["A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs","IST Austria Technical Report"],"subject":["ddc:000"],"creator":["Chatterjee, Krishnendu","Chmelik, Martin","Davies, Jessica"],"language":["eng"],"rights":["info:eu-repo/semantics/openAccess"],"type":["info:eu-repo/semantics/other","doc-type:other","text","http://purl.org/coar/resource_type/c_1843"],"publisher":["IST Austria"],"date":["2015"],"description":["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."],"identifier":["https://research-explorer.ista.ac.at/record/5443","https://research-explorer.ista.ac.at/download/5443/5466"],"relation":["info:eu-repo/semantics/altIdentifier/doi/10.15479/AT:IST-2015-325-v2-1","info:eu-repo/semantics/altIdentifier/issn/2664-1690"],"source":["Chatterjee K, Chmelik M, Davies J. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria; 2015. doi:10.15479/AT:IST-2015-325-v2-1"]},"day":"06","has_accepted_license":"1","date_created":"2018-12-12T11:39:22Z","date_published":"2015-11-06T00:00:00Z","page":"23","uri_base":"https://research-explorer.ista.ac.at"}]