Formally Verified SAT-Based AI Planning
Abstract
We present an executable formally verified SAT encoding of ground classical AI planning problems. We use the theorem prover Isabelle/HOL to perform the verification. We experimentally test the verified encoding and show that it can be used for reasonably sized standard planning benchmarks. We also use it as a reference to test a state-of-the-art SAT-based planner, showing that it sometimes falsely claims that problems have no solutions of certain lengths.
Cite
Text
Abdulaziz and Kurz. "Formally Verified SAT-Based AI Planning." AAAI Conference on Artificial Intelligence, 2023. doi:10.1609/AAAI.V37I12.26714Markdown
[Abdulaziz and Kurz. "Formally Verified SAT-Based AI Planning." AAAI Conference on Artificial Intelligence, 2023.](https://mlanthology.org/aaai/2023/abdulaziz2023aaai-formally/) doi:10.1609/AAAI.V37I12.26714BibTeX
@inproceedings{abdulaziz2023aaai-formally,
title = {{Formally Verified SAT-Based AI Planning}},
author = {Abdulaziz, Mohammad and Kurz, Friedrich},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2023},
pages = {14665-14673},
doi = {10.1609/AAAI.V37I12.26714},
url = {https://mlanthology.org/aaai/2023/abdulaziz2023aaai-formally/}
}