{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T07:36:06Z","timestamp":1770708966720,"version":"3.49.0"},"reference-count":17,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2023,6,8]],"date-time":"2023-06-08T00:00:00Z","timestamp":1686182400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SAT"],"abstract":"<jats:p>OMTPlan is a Python platform for optimal planning in numeric domains via reductions to Satisfiability Modulo Theories (SMT) and Optimization Modulo Theories (OMT). Currently, OMTPlan supports the expressive power of PDDL2.1 level 2 and features procedures for both satisficing and optimal planning. OMTPlan provides an open, easy to extend, yet efficient implementation framework. These goals are achieved through a modular design and the extensive use of state-of-the-art systems for SMT\/OMT solving.<\/jats:p>","DOI":"10.3233\/sat-220001","type":"journal-article","created":{"date-parts":[[2023,6,9]],"date-time":"2023-06-09T10:32:13Z","timestamp":1686306733000},"page":"17-23","source":"Crossref","is-referenced-by-count":3,"title":["OMTPlan: A Tool for Optimal Planning Modulo Theories"],"prefix":"10.1177","volume":"14","author":[{"given":"Francesco","family":"Leofante","sequence":"first","affiliation":[{"name":"Department of Computing, Imperial College London, London SW7 2AZ, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2023,6,8]]},"reference":[{"key":"10.3233\/SAT-220001_ref1","unstructured":"C.\u00a0Barrett, P.\u00a0Fontaine and C.\u00a0Tinelli, The Satisfiability Modulo Theories Library, 2016."},{"key":"10.3233\/SAT-220001_ref2","unstructured":"C.W.\u00a0Barrett, R.\u00a0Sebastiani, S.A.\u00a0Seshia and C.\u00a0Tinelli, Satisfiability modulo theories, in: Handbook of Satisfiability, Vol.\u00a0185, IOS Press, 2009, pp.\u00a0825\u2013885."},{"key":"10.3233\/SAT-220001_ref3","doi-asserted-by":"crossref","unstructured":"F.\u00a0Bigarella, A.\u00a0Cimatti, A.\u00a0Griggio, A.\u00a0Irfan, M.\u00a0Jon\u00e1s, M.\u00a0Roveri, R.\u00a0Sebastiani and P.\u00a0Trentin, Optimization modulo non-linear arithmetic via incremental linearization, in: Proceedings of FroCoS\u201921, LNCS, Vol.\u00a012941, Springer, 2021, pp.\u00a0213\u2013231.","DOI":"10.1007\/978-3-030-86205-3_12"},{"key":"10.3233\/SAT-220001_ref4","doi-asserted-by":"crossref","unstructured":"N.\u00a0Bj\u00f8rner, A.\u00a0Phan and L.\u00a0Fleckenstein, \u03bdZ\u00a0\u2013 an optimizing SMT solver, in: Proceedings of TACAS\u201915, LNCS, Vol.\u00a09035, Springer, 2015, pp.\u00a0194\u2013199.","DOI":"10.1007\/978-3-662-46681-0_14"},{"key":"10.3233\/SAT-220001_ref5","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1613\/jair.1129","article-title":"PDDL2.1: An extension to PDDL for expressing temporal planning domains","volume":"20","author":"Fox","year":"2003","journal-title":"J. Artif. Intell. Res."},{"key":"10.3233\/SAT-220001_ref6","doi-asserted-by":"crossref","unstructured":"H.\u00a0Geffner and B.\u00a0Bonet, A Concise Introduction to Models and Methods for Automated Planning, Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan & Claypool Publishers, 2013.","DOI":"10.1007\/978-3-031-01564-9"},{"issue":"2","key":"10.3233\/SAT-220001_ref7","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","article-title":"A formal basis for the heuristic determination of minimum cost paths","volume":"4","author":"Hart","year":"1968","journal-title":"IEEE Trans. Syst. Sci. Cybern."},{"issue":"5\u20136","key":"10.3233\/SAT-220001_ref8","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/j.artint.2008.10.013","article-title":"Concise finite-domain representations for PDDL planning tasks","volume":"173","author":"Helmert","year":"2009","journal-title":"Artif. Intell."},{"key":"10.3233\/SAT-220001_ref9","doi-asserted-by":"crossref","unstructured":"F.\u00a0Ivankovic, P.\u00a0Haslum, S.\u00a0Thi\u00e9baux, V.\u00a0Shivashankar and D.S.\u00a0Nau, Optimal planning with global numerical state constraints, in: Proceedings ICAPS\u201914, 2014.","DOI":"10.1609\/icaps.v24i1.13648"},{"key":"10.3233\/SAT-220001_ref10","unstructured":"R.\u00a0Kuroiwa and C.\u00a0Beck, A branch-and-cut approach for a mixed integer linear programming compilation of optimal numeric planning, in: HSDP@ICAPS, 2021."},{"key":"10.3233\/SAT-220001_ref11","doi-asserted-by":"crossref","unstructured":"F.\u00a0Leofante, E.\u00a0Giunchiglia, E.\u00a0\u00c1brah\u00e1m and A.\u00a0Tacchella, Optimal planning modulo theories, in: Proceedings of IJCAI\u201920, 2020, pp.\u00a04128\u20134134.","DOI":"10.24963\/ijcai.2020\/571"},{"key":"10.3233\/SAT-220001_ref12","doi-asserted-by":"crossref","unstructured":"D.\u00a0Li, E.\u00a0Scala, P.\u00a0Haslum and S.\u00a0Bogomolov, Effect-abstraction based relaxation for linear numeric planning, in: Proceedings of IJCAI\u201918, 2018, pp.\u00a04787\u20134793.","DOI":"10.24963\/ijcai.2018\/665"},{"key":"10.3233\/SAT-220001_ref13","unstructured":"F.\u00a0Lin and Y.\u00a0Zhao, ASSAT: Computing answer sets of a logic program by SAT solvers, in: Proceedings of AAAI\u201902, 2002, pp.\u00a0112\u2013118."},{"key":"10.3233\/SAT-220001_ref14","doi-asserted-by":"crossref","unstructured":"C.\u00a0Piacentini, M.\u00a0Castro, A.\u00a0Cir\u00e9 and C.\u00a0Beck, Compiling optimal numeric planning to mixed integer linear programming, in: Proceedings of ICAPS\u201918, 2018, pp.\u00a0383\u2013387.","DOI":"10.1609\/icaps.v28i1.13919"},{"key":"10.3233\/SAT-220001_ref15","unstructured":"J.\u00a0Rintanen, Planning and SAT, in: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, Vol.\u00a0185, IOS Press, 2009, pp.\u00a0483\u2013504."},{"key":"10.3233\/SAT-220001_ref16","unstructured":"E.\u00a0Scala, P.\u00a0Haslum, S.\u00a0Thi\u00e9baux and M.\u00a0Ram\u00edrez, Interval-based relaxation for general numeric planning, in: Proceedings of ECAI\u201916, Vol.\u00a0285, IOS Press, 2016, pp.\u00a0655\u2013663."},{"issue":"2","key":"10.3233\/SAT-220001_ref17","doi-asserted-by":"publisher","first-page":"12:1","DOI":"10.1145\/2699915","article-title":"Optimization modulo theories with linear rational costs","volume":"16","author":"Sebastiani","year":"2015","journal-title":"ACM Trans. Comput. Log."}],"container-title":["Journal on Satisfiability, Boolean Modeling and Computation"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/SAT-220001","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T07:08:26Z","timestamp":1761548906000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/SAT-220001"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,8]]},"references-count":17,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,6,8]]}},"URL":"https:\/\/doi.org\/10.3233\/sat-220001","relation":{},"ISSN":["1574-0617"],"issn-type":[{"value":"1574-0617","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,8]]}}}