Formally Verified SAT-Based AI Planning
Artificial Intelligence
2023-03-09 v5 Logic in Computer Science
Abstract
We present an executable formally verified SAT encoding of classical AI planning. 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
@article{arxiv.2010.14648,
title = {Formally Verified SAT-Based AI Planning},
author = {Mohammad Abdulaziz and Friedrich Kurz},
journal= {arXiv preprint arXiv:2010.14648},
year = {2023}
}