SibylSat is an incremental SAT-based planner for totally-ordered HTN planning problems based on a fork of the Lilotane planner. Like lilotane and other current SAT-based solver, SibylSat adheres to a standard procedure of alternating between expanding the search space, encoding it into a SAT formula, and invoking a SAT solver to find a solution plan. However, it differ from the other SAT-based planner in that it uses a greedy best first search to explore the search space instead of the usual breadth-first search. More details about the planner can be found in the ECAI paper.
SibylSat operates on totally-ordered HTN planning problems given as HDDL files [2]. The provided HTN domain may be recursive or non-recursive.
In short, SibylSat supports exactly the HDDL specification from the International Planning Competition (IPC) 2020 provided in [3] and [4]. It handles type systems, STRIPS-style actions with positive and negative conditions, method preconditions, equality and "sort-of" constraints, and universal quantifications in preconditions and effects. SibylSat cannot handle conditional effects, existential quantifications, or any other extended formalisms going beyond the mentioned concepts.
SibylSat outputs a plan in accordance to [5]. Basically everything in between "==>" and "<==" is the found plan, and everything inside that plan in front of the word root is the sequence of classical actions to execute.
SibylSat use both pandaPigrounder and pandaPiParser which require the following dependancies:
g++(C++17 support)makeflex(version 2.6 or higher)bison(versions 3.5.1 and 3.7.2 are known to work)zipzlib1g-devgengetopt(tested with version 2.23)
You can build SibylSat like this:
make
The SAT solver to link SibylSat with can be set with the IPASIRSOLVER variable in the makefile. Valid values are cadical, cryptominisat, glucose4, lingeling, and riss.
Note that the Makefile in the base directory is only supposed to be used for building SibylSat as an IPASIR application.
SibylSat can be run inside a Docker container to avoid manual dependency management. This allows you to compile and run SibylSat in a controlled environment with all necessary dependencies and submodules pre-installed.
To build the Docker image, run the following command in the root directory of the SibylSat repository:
docker build -t sibylsat .This command builds a Docker image called sibylsat, which contains all the required dependencies and the cloned SibylSat repository.
Once the Docker image is built, you can start the container and enter the Bash shell by running:
docker run -it sibylsatThis command starts the container and drops you into an interactive Bash shell inside the Docker environment, directly inside the sibylsat repository.. From here, you can manually run SibylSat using the instructions provided in Usage sections.
To exit the Docker container, you can simply type exit in the terminal. This will stop the container and return you to your host environment.
SibylSat uses the HDDL file format.
Execute the planner executable like this:
./sibylsat path/to/domain.hddl path/to/problem.hddl [options]By default, the executable is launched with the best sibylsat configuration. In particular, some options had been added for the sibylsat planner such as:
-mutex=<0|1>: Filter possible effects of abstract tasks using mutexes. Very useful to sibylsat to find better abstract plans. Default is 1.-macroActions=<0|1>: Join consecutive actions in subtasks methods into a single macro action. Default is 1.-optimal=<0|1>: Use the technique proposed in [6] to find optimal solution for TOHTN problems. Note that you must link SibylSat with a MaxSat solver beforehand (setting the IPASIR solver to uwrmaxsat in makefile and then runmakeagain) Default is 0.
Some useful parameters as well:
-h: Print all available options.-v=<verb>: Verbosity of the planner. Use 0 if you absolutely only care about the plan. Use 1 for warnings, 2 for general information, 3 for verbose output and 4 for full debug messages.-wp: If a plan is found, write it into plan.txt.-wf: Write the generated formula to./f.cnf. As SibylSat works incrementally, the formula will consist of all clauses added during program execution. Additionally, when the program exits, the assumptions used in the final SAT call will be added to the formula as well.
SibylSat includes benchmark sets from the totally-ordered HTN IPC 2020 and IPC 2023. These benchmarks are included as submodules in the Benchmarks folder. To obtain the benchmarks, you will need to initialize the submodules as follows:
git submodule update --init --recursiveThe IPC 2020 benchmarks are located in Benchmarks/ipc2020-domains, and the IPC 2023 benchmarks are located in Benchmarks/ipc2023-domains.
You can navigate into these directories to explore the respective benchmarks. Some benchmarks are identical between the two sets but are maintained separately for clarity about their origin. Only the total-order benchmarks can be used with SibylSat.
The code of SibylSat is published under the GNU GPLv3. Consult the LICENSE file for details.
The planner uses pandaPIparser and pandaPIgrounder [2] which are 3-Clause BSD licensed.
Note that depending on the SAT solver compiled into the planner, usage and redistribution rights may be subject to their licensing. Specifically: CaDiCaL, Cryptominisat, Lingeling and Riss are Free Software while Glucose technically is not.
SibylSat is based on a fork of the Lilotane planner developed by Dominik Schreiber dominik.schreiber@kit.edu [1]. SibylSat itself is developed by Gaspard Quenard gaspard.quenard@univ-grenoble-alpes.fr
If you use SibylSat in academic work, please cite [0]. If you use SibylSat to find optimal solution (using parameter -optimal), please cite [6].
[0] Quenard, G., Pellier, D., & Fiorino, H. (2024). SibylSat: Using SAT as an Oracle to Perform a Greedy Search on TOHTN Planning. In27th European Conference on Artificial Intelligence, volume 392, 4157–4164.
[1] Schreiber, D. (2021). Lilotane: A Lifted SAT-based Approach to Hierarchical Planning. In Journal of Artificial Intelligence Research (JAIR) 2021 (70), pp. 1117-1181.
[2] Behnke, G., Höller, D., Schmid, A., Bercher, P., & Biundo, S. (2020). On Succinct Groundings of HTN Planning Problems. In AAAI (pp. 9775-9784).
[3] Höller, D., Behnke, G., Bercher, P., Biundo, S., Fiorino, H., Pellier, D., & Alford, R. (2020). HDDL: An Extension to PDDL for Expressing Hierarchical Planning Problems. In AAAI (pp. 9883-9891).
[4] Behnke, G. et al. (2020). HDDL - Addendum. Universität Freiburg.
[5] Behnke, G. et al. (2020). Plan verification. Universität Freiburg.
[6] Quenard, G., Pellier, D., & Fiorino, H. (2025). SibylSatOpt: a MaxSAT-based Greedy Optimal Search for TOHTN Planning. In Proceedings of the International Conference on Automated Planning and Scheduling. Vol. 35. No. 1. 2025.