Planning for Hybrid Systems via Satisfiability Modulo Theories
- Submitting institution
-
King's College London
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 119707265
- Type
- D - Journal article
- DOI
-
10.1613/jair.1.11751
- Title of journal
- Journal Artificial Intelligence Research
- Article number
- -
- First page
- 253
- Volume
- 67
- Issue
- -
- ISSN
- 1076-9757
- Open access status
- Compliant
- Month of publication
- February
- Year of publication
- 2020
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper presents SMTPlan, the first encoding of expressive planning problems to SMT. Theoretical validation of the encoding as well as extensive experimentation on a set of benchmarks problems are provided. This work advances the state of the art in AI planning for nonlinear problems. It has instigated new research and is still serving as the baseline for state-of-the-art (e.g, Say et al. IJCAI-17; Fernández-González AAAI-17; Leofante iFM-18). The software has been used by international research groups, such as the Melbourne University and Fondazione Bruno Kessler. A tutorial on SMTPlan was presented in at the AAAI-16 conference.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -