Certified Unsolvability for SAT Planning with Property Directed Reachability

Eriksson, Salomé and Helmert, Malte. (2020) Certified Unsolvability for SAT Planning with Property Directed Reachability. In: Proceedings of the Thirtieth International Conference on Automated Planning and Scheduling (ICAPS 2020), 30. pp. 90-100.

[img] PDF - Accepted Version

Official URL: https://edoc.unibas.ch/78716/

Downloads: Statistics Overview


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 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.
Faculties and Departments:05 Faculty of Science > Departement Mathematik und Informatik > Informatik > Artificial Intelligence (Helmert)
UniBasel Contributors:Eriksson, Salomé and Helmert, Malte
Item Type:Conference or Workshop Item, refereed
Conference or workshop item Subtype:Conference Paper
Publisher:AAAI Press
Note:Publication type according to Uni Basel Research Database: Conference paper
Related URLs:
edoc DOI:
Last Modified:02 Oct 2020 13:09
Deposited On:02 Oct 2020 13:08

Repository Staff Only: item control page