A Study of the Power of Heuristic-based Pruning via SAT Planning. Johnson, C., Bercher, P., & Gretton, C. In Proceedings of the 14th Workshop on Heuristics and Search for Domain-independent Planning (HSDIP 2022), 2022. This paper has also been accepted at KEPS 2022.![A Study of the Power of Heuristic-based Pruning via SAT Planning [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Paper ![A Study of the Power of Heuristic-based Pruning via SAT Planning [link]](https://bibbase.org/img/filetypes/link.svg "link")
Presentation Openreview abstract bibtex 1 download Planning as SAT (satisfiability) is the method of representing a horizon-bounded planning problem as a Boolean SAT problem, and using a SAT decision procedure to solve that problem. Representations are direct, thus a solution plan can be obtained directly from a satisfying valuation. By querying a SAT solver over a series of horizon lengths, up to a completeness threshold, this approach can be the basis of a complete planning procedure. SAT planning algorithms have been theoretically contrasted with IDA∗ search, a heuristic state-based search algorithm, where a theoretical exponential separation is demonstrated in favour of the SAT approach. Here a nominated heuristic is implemented in SAT with the query formulae encoding heuristic information. We make two practical contributions related to this background. First, we provide to the best of our knowledge the first practical implementation of a theoretical SAT encoding of the h-2 heuristic. Second, we empirically evaluate SAT-based pruning by implementing heuristics h-max and h-2.
@InProceedings{Johnson2022aSATPruning,
author = {Christopher Johnson and Pascal Bercher and Charles Gretton},
booktitle = {Proceedings of the 14th Workshop on Heuristics and Search for Domain-independent Planning (HSDIP 2022)},
title = {A Study of the Power of Heuristic-based Pruning via SAT Planning},
year = {2022},
abstract = {Planning as SAT (satisfiability) is the method of representing a horizon-bounded planning problem as a Boolean SAT problem, and using a SAT decision procedure to solve that problem. Representations are direct, thus a solution plan can be obtained directly from a satisfying valuation. By querying a SAT solver over a series of horizon lengths, up to a completeness threshold, this approach can be the basis of a complete planning procedure. SAT planning algorithms have been theoretically contrasted with IDA∗ search, a heuristic state-based search algorithm, where a theoretical exponential separation is demonstrated in favour of the SAT approach. Here a nominated heuristic is implemented in SAT with the query formulae encoding heuristic information. We make two practical contributions related to this background. First, we provide to the best of our knowledge the first practical implementation of a theoretical SAT encoding of the h-2 heuristic. Second, we empirically evaluate SAT-based pruning by implementing heuristics h-max and h-2.},
note = {This paper has also been accepted at KEPS 2022.},
url_Paper = {https://bercher.net/publications/2022/Johnson2022SATBasedHeuristicPruning.pdf},
url_presentation = {https://www.youtube.com/watch?v=HFntrSAyszU},
url_openReview = {https://openreview.net/forum?id=c2-QShxGZt},
keywords = {workshop}
}
Downloads: 1
{"_id":"LoAvgspGJhoyooJBA","bibbaseid":"johnson-bercher-gretton-astudyofthepowerofheuristicbasedpruningviasatplanning-2022","author_short":["Johnson, C.","Bercher, P.","Gretton, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Christopher"],"propositions":[],"lastnames":["Johnson"],"suffixes":[]},{"firstnames":["Pascal"],"propositions":[],"lastnames":["Bercher"],"suffixes":[]},{"firstnames":["Charles"],"propositions":[],"lastnames":["Gretton"],"suffixes":[]}],"booktitle":"Proceedings of the 14th Workshop on Heuristics and Search for Domain-independent Planning (HSDIP 2022)","title":"A Study of the Power of Heuristic-based Pruning via SAT Planning","year":"2022","abstract":"Planning as SAT (satisfiability) is the method of representing a horizon-bounded planning problem as a Boolean SAT problem, and using a SAT decision procedure to solve that problem. Representations are direct, thus a solution plan can be obtained directly from a satisfying valuation. By querying a SAT solver over a series of horizon lengths, up to a completeness threshold, this approach can be the basis of a complete planning procedure. SAT planning algorithms have been theoretically contrasted with IDA∗ search, a heuristic state-based search algorithm, where a theoretical exponential separation is demonstrated in favour of the SAT approach. Here a nominated heuristic is implemented in SAT with the query formulae encoding heuristic information. We make two practical contributions related to this background. First, we provide to the best of our knowledge the first practical implementation of a theoretical SAT encoding of the h-2 heuristic. Second, we empirically evaluate SAT-based pruning by implementing heuristics h-max and h-2.","note":"This paper has also been accepted at KEPS 2022.","url_paper":"https://bercher.net/publications/2022/Johnson2022SATBasedHeuristicPruning.pdf","url_presentation":"https://www.youtube.com/watch?v=HFntrSAyszU","url_openreview":"https://openreview.net/forum?id=c2-QShxGZt","keywords":"workshop","bibtex":"@InProceedings{Johnson2022aSATPruning,\n author = {Christopher Johnson and Pascal Bercher and Charles Gretton},\n booktitle = {Proceedings of the 14th Workshop on Heuristics and Search for Domain-independent Planning (HSDIP 2022)},\n title = {A Study of the Power of Heuristic-based Pruning via SAT Planning},\n year = {2022},\n abstract = {Planning as SAT (satisfiability) is the method of representing a horizon-bounded planning problem as a Boolean SAT problem, and using a SAT decision procedure to solve that problem. Representations are direct, thus a solution plan can be obtained directly from a satisfying valuation. By querying a SAT solver over a series of horizon lengths, up to a completeness threshold, this approach can be the basis of a complete planning procedure. SAT planning algorithms have been theoretically contrasted with IDA∗ search, a heuristic state-based search algorithm, where a theoretical exponential separation is demonstrated in favour of the SAT approach. Here a nominated heuristic is implemented in SAT with the query formulae encoding heuristic information. We make two practical contributions related to this background. First, we provide to the best of our knowledge the first practical implementation of a theoretical SAT encoding of the h-2 heuristic. Second, we empirically evaluate SAT-based pruning by implementing heuristics h-max and h-2.},\n note = {This paper has also been accepted at KEPS 2022.},\n url_Paper = {https://bercher.net/publications/2022/Johnson2022SATBasedHeuristicPruning.pdf},\n url_presentation = {https://www.youtube.com/watch?v=HFntrSAyszU},\n url_openReview = {https://openreview.net/forum?id=c2-QShxGZt},\n keywords = {workshop}\n}\n\n","author_short":["Johnson, C.","Bercher, P.","Gretton, C."],"key":"Johnson2022aSATPruning","id":"Johnson2022aSATPruning","bibbaseid":"johnson-bercher-gretton-astudyofthepowerofheuristicbasedpruningviasatplanning-2022","role":"author","urls":{" paper":"https://bercher.net/publications/2022/Johnson2022SATBasedHeuristicPruning.pdf"," presentation":"https://www.youtube.com/watch?v=HFntrSAyszU"," openreview":"https://openreview.net/forum?id=c2-QShxGZt"},"keyword":["workshop"],"metadata":{"authorlinks":{}},"downloads":1},"bibtype":"inproceedings","biburl":"https://bercher.net/bibtex/bibliography.bib","dataSources":["jTtEZEw8NJc375xGA","bPpsmYWjffAy6QHP5","wYF8yPQT6a4TgShWe"],"keywords":["workshop"],"search_terms":["study","power","heuristic","based","pruning","via","sat","planning","johnson","bercher","gretton"],"title":"A Study of the Power of Heuristic-based Pruning via SAT Planning","year":2022,"downloads":1}