Certified Unsolvability for SAT Planning with Property Directed Reachability

Salomé Eriksson, Malte Helmert

PosterID: 46 PDF Slides Poster BibTeX

While classical planning systems can usually detect if a task is unsolvable, only recent research introduced a way to verify such a claim. These methods have already been applied to a variety of explicit and symbolic search algorithms, but so far no planning technique based on SAT has been covered with them. We fill this gap by showing how \emph{property directed reachability} can produce proofs while only minimally altering the framework by allowing to utilize certificates for unsolvable SAT queries within the proof. We additionally show that a variant of the algorithm that does not use SAT calls can produce proofs that fit into the existing framework without requiring any changes.

Session E2: Lifted Planning / Symbolic Planning / Submodularity
Canb 10/28/2020, 18:00 – 19:00
10/30/2020, 01:00 – 02:00
Paris 10/28/2020, 08:00 – 09:00
10/29/2020, 15:00 – 16:00
NYC 10/28/2020, 03:00 – 04:00
10/29/2020, 10:00 – 11:00
LA 10/28/2020, 00:00 – 01:00
10/29/2020, 07:00 – 08:00