KIT | KIT-Bibliothek | Impressum | Datenschutz

PASAR - Planning as Satisfiability with Abstraction Refinement

Froleyks, Nils 1; Balyo, Tomáš 1; Schreiber, Dominik ORCID iD icon 1
1 Karlsruher Institut für Technologie (KIT)


One of the classical approaches to automated planning is the reduction to propositional satisfiability (SAT). Recently, it has been shown that incremental SAT solving can increase the capabilities of several modern encodings for SAT-based planning. In this paper, we present a further improvement to SAT-based planning by introducing a new algorithm named PASAR based on the principles of counterexample guided abstraction refinement (CEGAR). As an abstraction of the original problem, we use a simplified encoding where interference between actions is generally allowed. Abstract plans are converted into actual plans where possible or otherwise used as a counterexample to refine the abstraction. Using benchmark domains from recent International Planning Competitions, we compare our approach to different state-of-the-art planners and find that, in particular, combining PASAR with forward state-space search techniques leads to promising results.

Zitationen: 4
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2019
Sprache Englisch
Identifikator ISBN: 978-1-57735-808-4
KITopen-ID: 1000097226
Erschienen in Proceedings of the 12th Annual Symposium on Combinatorial Search (SoCs 2019), Napa, CA, July 16-17, 2019
Veranstaltung 12th Annual Symposium on Combinatorial Search (SoCs 2019), Napa, CA, USA, 16.07.2019 – 17.07.2019
Verlag AAAI Press
Seiten 70-78
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page