### Abstract

We present an executable formally verified SAT encoding of classical AI planning that is based on the encodings by Kautz and Selman and the one by Rintanen et al. The encoding was experimentally tested and shown to be usable for reasonably sized standard AI 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. The formalisation in this submission was described in an independent publication.

### License

BSD License

### Topics

- Computer science/Artificial intelligence

### Session Verified_SAT_Based_AI_Planning

- List_Supplement
- Map_Supplement
- CNF_Supplement
- CNF_Semantics_Supplement
- State_Variable_Representation
- STRIPS_Representation
- STRIPS_Semantics
- SAS_Plus_Representation
- SAS_Plus_Semantics
- SAS_Plus_STRIPS
- SAT_Plan_Base
- SAT_Plan_Extensions
- SAT_Solve_SAS_Plus
- AST_SAS_Plus_Equivalence
- Set2_Join_RBT
- Solve_SASP

### Depends on

- AI Planning Languages Semantics
- List Index
- Propositional Proof Systems

## Cite

×

Verified_SAT_Based_AI_Planning-AFP

    @article{Verified_SAT_Based_AI_Planning-AFP,
      author  = {Mohammad Abdulaziz and Friedrich Kurz},
      title   = {Verified SAT-Based AI Planning},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Nov 13, 2020 : Isabelle2020
- Nov 3, 2020 : Isabelle2020