Code and experimental results of the JELIA 2025 paper "AxSAT - Bringing Axioms to SAT Planning"
| Creators |
|
|---|---|
| Contributors |
|
| Publication date | 11-07-2025 |
| Description |
The file code.zip contains an extended version of the Fast Downward planning system (http://fast-downward.org). The code for the SAT-based search can be found in "src/search/search_algorithms/sat_search.*". The scripts used to run the experiments can be found in "experiments/decoupling-sat/". Please check Fast Downward's webpage for detailed instructions on how to compile and run the planner. The Kissat SAT solver is needed for running the SAT-based configurations. We used Kissat in revision da2b0641996913cbc18c2e08cc3945367c395143, which is not part of the code.zip archive and can be downloaded here: https://github.com/arminbiere/kissat
Here is a short version for building the planner and running the SAT-based search with the sequential exists-step encoding:
./build.py -s[PATH-TO-KISSAT-LIB] --kissat
./fast-downward.py PROBLEM_FILE --search "sat(encoding=2)"
The latest version of the code is available at https://github.com/galvusdamor/decoupling-transformer-sat.
Benchmarks
The file benchmarks.tar.xz contains the PDDL benchmarks used in the experimental evaluation of the paper.
Experiment Data
The remaining files contain the raw experiment data and parsed values for the experiments in the paper. The file "experiment-data-raw.tar.xz" contains the raw data, including code, executables, and log files of all experiment runs. The file experiment-data-parsed.xz contains a "properties" file with all parsed values.
|
| Publisher | Zenodo |
| Organisations |
|
| Document type | Dataset |
| DOI | https://doi.org/10.5281/zenodo.15848555 |
| Permalink to this page | |
