SibylSat: Using SAT as an Oracle to Perform a Greedy Search on TOHTN Planning

TL;DR

SibylSat introduces a SAT-based greedy search method for totally-ordered HTN planning, leveraging heuristics from relaxed problem solving to improve efficiency and plan quality over existing approaches.

Contribution

It presents a novel SAT-based greedy search algorithm for TOHTN planning that outperforms existing SAT-based methods in speed and solution quality.

Findings

Outperforms existing SAT-based TOHTN planners in runtime

Produces higher quality plans on benchmark problems

Solves a larger number of problems successfully

Abstract

This paper presents SibylSat, a novel SAT-based method designed to efficiently solve totally-ordered HTN problems (TOHTN). In contrast to prevailing SAT-based HTN planners that employ a breadth-first search strategy, SibylSat adopts a greedy search approach, enabling it to identify promising decompositions for expansion. The selection process is facilitated by a heuristic derived from solving a relaxed problem, which is also expressed as a SAT problem. Our experimental evaluations demonstrate that SibylSat outperforms existing SAT-based TOHTN approaches in terms of both runtime and plan quality on most of the IPC benchmarks, while also solving a larger number of problems.