Formally Verified SAT-Based AI Planning
This work addresses the need for reliable and verifiable planning algorithms in AI, though it is incremental as it builds on existing SAT-based methods with formal verification.
The authors tackled the problem of ensuring correctness in SAT-based AI planning by developing a formally verified SAT encoding using Isabelle/HOL, and they experimentally validated it on standard benchmarks while uncovering errors in a state-of-the-art planner that sometimes falsely reported no solutions.
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.