Formally Verified SAT-Based AI Planning

TL;DR

This paper introduces a formally verified SAT encoding for classical AI planning, ensuring correctness through Isabelle/HOL, and demonstrates its practical applicability and limitations on standard benchmarks.

Contribution

It provides the first formally verified SAT encoding for AI planning using Isabelle/HOL, enhancing reliability and serving as a benchmark reference.

Findings

Verified encoding can handle reasonably sized benchmarks

The verified encoding exposes flaws in a state-of-the-art SAT planner

Demonstrates practical use of formal verification in AI planning

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.