totSAT - Totally-Ordered Hierarchical Planning Through SAT
Abstract
In this paper, we propose a novel SAT-based planning approach for hierarchical planning by introducing the SAT-based planner totSAT for the class of totally-ordered HTN planning problems. We use the same general approach as SAT planning for classical planning does: bound the problem, translate the problem into a formula, and if the formula is not satisfiable, increase the bound. In HTN planning, a suitable bound is the maximum depth of decomposition. We show how totally-ordered HTN planning problems can be translated into a SAT formula, given this bound. Furthermore, we have conducted an extensive empirical evaluation to compare our new planner against state-of-the-art HTN planners. It shows that our technique outperforms any of these systems.
Cite
Text
Behnke et al. "totSAT - Totally-Ordered Hierarchical Planning Through SAT." AAAI Conference on Artificial Intelligence, 2018. doi:10.1609/AAAI.V32I1.12083Markdown
[Behnke et al. "totSAT - Totally-Ordered Hierarchical Planning Through SAT." AAAI Conference on Artificial Intelligence, 2018.](https://mlanthology.org/aaai/2018/behnke2018aaai-totsat/) doi:10.1609/AAAI.V32I1.12083BibTeX
@inproceedings{behnke2018aaai-totsat,
title = {{totSAT - Totally-Ordered Hierarchical Planning Through SAT}},
author = {Behnke, Gregor and Höller, Daniel and Biundo, Susanne},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2018},
pages = {6110-6118},
doi = {10.1609/AAAI.V32I1.12083},
url = {https://mlanthology.org/aaai/2018/behnke2018aaai-totsat/}
}