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. | |
| 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 |
Certified Unsolvability for SAT Planning with Property Directed Reachability
Salomé Eriksson, Malte Helmert
When Perfect Is Not Good Enough: On the Search Behaviour of Symbolic Heuristic Search
David Speck, Florian Geißer, Robert Mattmüller
Lifted Successor Generation Using Query Optimization Techniques
Augusto B. Corrêa, Florian Pommerening, Malte Helmert, Guillem Francès
Through the Lens of Sequence Submodularity
Sara Bernardini, Fabio Fagnani, Chiara Piacentini