[{"ec_funded":1,"month":"12","title":"A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","publisher":"AAAI Press","_id":"1166","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin"},{"full_name":"Davies, Jessica","first_name":"Jessica","last_name":"Davies","id":"378E0060-F248-11E8-B48F-1D18A9856A87"}],"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"year":"2016","day":"02","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."}],"date_updated":"2023-02-23T12:26:41Z","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5443"}],"link":[{"relation":"table_of_contents","url":"https://dl.acm.org/citation.cfm?id=3016355"}]},"citation":{"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.","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.","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.","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.","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.","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.","short":"K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232."},"intvolume":"      2016","volume":2016,"quality_controlled":"1","publist_id":"6191","date_published":"2016-12-02T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"language":[{"iso":"eng"}],"type":"conference","oa_version":"None","publication":"Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence","date_created":"2018-12-11T11:50:30Z","page":"3225 - 3232","conference":{"name":"AAAI: Conference on Artificial Intelligence","start_date":"2016-02-12","location":"Phoenix, AZ, USA","end_date":"2016-02-17"},"publication_status":"published"},{"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"full_name":"Davies, Jessica","first_name":"Jessica","id":"378E0060-F248-11E8-B48F-1D18A9856A87","last_name":"Davies"}],"_id":"5443","file":[{"content_type":"application/pdf","relation":"main_file","file_size":412379,"date_updated":"2020-07-14T12:46:57Z","file_name":"IST-2015-325-v2+1_main.pdf","date_created":"2018-12-12T11:53:05Z","file_id":"5466","creator":"system","checksum":"f0fa31ad8161ed655137e94012123ef9","access_level":"open_access"}],"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."}],"date_updated":"2023-02-21T16:24:05Z","year":"2015","day":"06","alternative_title":["IST Austria Technical Report"],"month":"11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","publisher":"IST Austria","publication_identifier":{"issn":["2664-1690"]},"oa":1,"title":"A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs","type":"technical_report","oa_version":"Published Version","date_published":"2015-11-06T00:00:00Z","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2015-325-v2-1","publication_status":"published","has_accepted_license":"1","page":"23","date_created":"2018-12-12T11:39:22Z","citation":{"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>","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>.","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. <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.","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>","short":"K. Chatterjee, M. Chmelik, J. Davies, A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs, IST Austria, 2015."},"related_material":{"record":[{"status":"public","relation":"later_version","id":"1166"}]},"pubrep_id":"362","file_date_updated":"2020-07-14T12:46:57Z","ddc":["000"]}]