KIT | KIT-Bibliothek | Impressum | Datenschutz

Lilotane : A Lifted SAT-based Approach to Hierarchical Planning

Schreiber, Dominik

One of the oldest and most popular approaches to automated planning is to encode the problem at hand into a propositional formula and use a Satisfiability (SAT) solver to find a solution. In all established SAT-based approaches for Hierarchical Task Network (HTN) planning, grounding the problem is necessary and oftentimes introduces a combinatorial blowup in terms of the number of actions and reductions to encode. Our contribution named Lilotane (Lifted Logic for Task Networks) eliminates this issue for Totally Ordered HTN planning by directly encoding the lifted representation of the problem at hand. We lazily instantiate the problem hierarchy layer by layer and use a novel SAT encoding which allows us to defer decisions regarding method arguments to the stage of SAT solving. We show the correctness of our encoding and compare it to the best performing prior SAT encoding in a worst-case analysis. Empirical evaluations confirm that Lilotane outperforms established SAT-based approaches, often by orders of magnitude, produces much smaller formulae on average, and compares favorably to other state-of-the-art HTN planners regarding robustness and plan quality. ... mehr

DOI: 10.1613/jair.1.12520
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Zeitschriftenaufsatz
Publikationsjahr 2021
Sprache Englisch
Identifikator ISSN: 1076-9757
KITopen-ID: 1000131098
Erschienen in Journal of artificial intelligence research
Verlag AI Access Foundation
Band 70
Seiten 1117–1181
Vorab online veröffentlicht am 17.03.2021
Schlagwörter satisfiability, planning, problem solving
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page