Exploiting Solution Order Graphs and Path Decomposition Trees for More Efficient HTN Plan Verification via SAT Solving. Lin, S., Behnke, G., & Bercher, P. In Proceedings of the 5th ICAPS Workshop on Hierarchical Planning (HPlan 2022), pages 24–28, 2022.
![Exploiting Solution Order Graphs and Path Decomposition Trees for More Efficient HTN Plan Verification via SAT Solving [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Paper Poster ![Exploiting Solution Order Graphs and Path Decomposition Trees for More Efficient HTN Plan Verification via SAT Solving [link]](https://bibbase.org/img/filetypes/link.svg "link")
Presentation abstract bibtex 18 downloads
Paper Poster Presentation abstract bibtex 18 downloads The research on the plan verification problem has drawn increasing attention in the last few years. It can serve as an approach for validating a planning domain by viewing an input plan as a test case which is supposed to be a solution to a planning problem in the domain which is to be validated. In this paper, we study the plan verification problem in the context of Hierarchical Task Network (HTN) planning. Concretely, we will develop an SAT-based approach via exploiting the data structures solution order graphs and path decomposition trees employed by the state-of-the-art SAT-based HTN planner which transforms an HTN plan verification problem into an SAT formula. Additionally, for the purpose of completeness, we will also reimplement the old SAT-based plan verifier within an outdated planning system called PANDA-3 and integrate it into the new version called PANDA-pi.
@InProceedings{Lin2022SATviaSOGs,
author = {Songtuan Lin and Gregor Behnke and Pascal Bercher},
booktitle = {Proceedings of the 5th ICAPS Workshop on Hierarchical Planning (HPlan 2022)},
title = {Exploiting Solution Order Graphs and Path Decomposition Trees for More Efficient HTN Plan Verification via SAT Solving},
year = {2022},
pages = {24--28},
abstract = {The research on the plan verification problem has drawn increasing attention in the last few years. It can serve as an approach for validating a planning domain by viewing an input plan as a test case which is supposed to be a solution to a planning problem in the domain which is to be validated. In this paper, we study the plan verification problem in the context of Hierarchical Task Network (HTN) planning. Concretely, we will develop an SAT-based approach via exploiting the data structures solution order graphs and path decomposition trees employed by the state-of-the-art SAT-based HTN planner which transforms an HTN plan verification problem into an SAT formula. Additionally, for the purpose of completeness, we will also reimplement the old SAT-based plan verifier within an outdated planning system called PANDA-3 and integrate it into the new version called PANDA-pi.},
url_Paper = {https://bercher.net/publications/2022/Lin2022SATbasedVerification.pdf},
url_Poster = {https://bercher.net/publications/2022/Lin2022SATbasedVerificationPoster.pdf},
url_presentation = {https://youtu.be/DbDTuY7dOxM},
keywords = {workshop}
}Downloads: 18
{"_id":"bYkTjP56ravYiEYvR","bibbaseid":"lin-behnke-bercher-exploitingsolutionordergraphsandpathdecompositiontreesformoreefficienthtnplanverificationviasatsolving-2022","author_short":["Lin, S.","Behnke, G.","Bercher, P."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Songtuan"],"propositions":[],"lastnames":["Lin"],"suffixes":[]},{"firstnames":["Gregor"],"propositions":[],"lastnames":["Behnke"],"suffixes":[]},{"firstnames":["Pascal"],"propositions":[],"lastnames":["Bercher"],"suffixes":[]}],"booktitle":"Proceedings of the 5th ICAPS Workshop on Hierarchical Planning (HPlan 2022)","title":"Exploiting Solution Order Graphs and Path Decomposition Trees for More Efficient HTN Plan Verification via SAT Solving","year":"2022","pages":"24–28","abstract":"The research on the plan verification problem has drawn increasing attention in the last few years. It can serve as an approach for validating a planning domain by viewing an input plan as a test case which is supposed to be a solution to a planning problem in the domain which is to be validated. In this paper, we study the plan verification problem in the context of Hierarchical Task Network (HTN) planning. Concretely, we will develop an SAT-based approach via exploiting the data structures solution order graphs and path decomposition trees employed by the state-of-the-art SAT-based HTN planner which transforms an HTN plan verification problem into an SAT formula. Additionally, for the purpose of completeness, we will also reimplement the old SAT-based plan verifier within an outdated planning system called PANDA-3 and integrate it into the new version called PANDA-pi.","url_paper":"https://bercher.net/publications/2022/Lin2022SATbasedVerification.pdf","url_poster":"https://bercher.net/publications/2022/Lin2022SATbasedVerificationPoster.pdf","url_presentation":"https://youtu.be/DbDTuY7dOxM","keywords":"workshop","bibtex":"@InProceedings{Lin2022SATviaSOGs,\n author = {Songtuan Lin and Gregor Behnke and Pascal Bercher},\n booktitle = {Proceedings of the 5th ICAPS Workshop on Hierarchical Planning (HPlan 2022)},\n title = {Exploiting Solution Order Graphs and Path Decomposition Trees for More Efficient HTN Plan Verification via SAT Solving},\n year = {2022},\n pages = {24--28},\n abstract = {The research on the plan verification problem has drawn increasing attention in the last few years. It can serve as an approach for validating a planning domain by viewing an input plan as a test case which is supposed to be a solution to a planning problem in the domain which is to be validated. In this paper, we study the plan verification problem in the context of Hierarchical Task Network (HTN) planning. Concretely, we will develop an SAT-based approach via exploiting the data structures solution order graphs and path decomposition trees employed by the state-of-the-art SAT-based HTN planner which transforms an HTN plan verification problem into an SAT formula. Additionally, for the purpose of completeness, we will also reimplement the old SAT-based plan verifier within an outdated planning system called PANDA-3 and integrate it into the new version called PANDA-pi.},\n url_Paper = {https://bercher.net/publications/2022/Lin2022SATbasedVerification.pdf},\n url_Poster = {https://bercher.net/publications/2022/Lin2022SATbasedVerificationPoster.pdf},\n url_presentation = {https://youtu.be/DbDTuY7dOxM},\n keywords = {workshop}\n}\n\n","author_short":["Lin, S.","Behnke, G.","Bercher, P."],"key":"Lin2022SATviaSOGs","id":"Lin2022SATviaSOGs","bibbaseid":"lin-behnke-bercher-exploitingsolutionordergraphsandpathdecompositiontreesformoreefficienthtnplanverificationviasatsolving-2022","role":"author","urls":{" paper":"https://bercher.net/publications/2022/Lin2022SATbasedVerification.pdf"," poster":"https://bercher.net/publications/2022/Lin2022SATbasedVerificationPoster.pdf"," presentation":"https://youtu.be/DbDTuY7dOxM"},"keyword":["workshop"],"metadata":{"authorlinks":{}},"downloads":18},"bibtype":"inproceedings","biburl":"https://bercher.net/bibtex/bibliography.bib","dataSources":["jTtEZEw8NJc375xGA","WvkzCyK6mKXCp2WFz","KEAqQQoqfNcS7jcf2","8ouDAAtyyeSzYbpbz","T9LQLt3D2MDhrCfjh","rta5EvLvgMEDFTyZk","bPpsmYWjffAy6QHP5","wYF8yPQT6a4TgShWe"],"keywords":["workshop"],"search_terms":["exploiting","solution","order","graphs","path","decomposition","trees","more","efficient","htn","plan","verification","via","sat","solving","lin","behnke","bercher"],"title":"Exploiting Solution Order Graphs and Path Decomposition Trees for More Efficient HTN Plan Verification via SAT Solving","year":2022,"downloads":18}