Knowledge, Reasoning and Planning Seminar, MSc Spring Semester 2026
Spider with Axioms
Rewriting an existing domain in PDDL with axioms
Manuel Buser
University of Basel
Project Overview
Final presentation for the Knowledge, Reasoning and Planning seminar at the University of Basel (MSc Spring Semester 2026). The project compares two PDDL encodings of the same Solitaire planning problem.
If you want to know more about PDDL, here is the full report:
↓ Download the final report (PDF)Background
What is Spider Solitaire?
A single-player card game. Cards sit on a tableau of piles. The goal is to remove every card by building same-suit Ace-to-King runs.
Try it online at free-spider-solitaire.com.
Rules are described on en.wikipedia.org/wiki/Spider_(solitaire).
What is PDDL?
The Planning Domain Definition Language, a formal language for describing planning problems. Used by the International Planning Competition (IPC) and most academic planning research.
What did we do?
Took the
2018 IPC Spider domain
and rewrote it using PDDL derived predicates
(:derived-predicates) instead of eight zero-cost
propagation actions and four control flags. The two domains
describe the same problem.
The rewrite
What changes in the PDDL?
Click a row to expand the side-by-side. Each row shows the no-axioms original (red) next to the axiom-based replacement (green).
1
The :requirements line
conditional-effects, derived-predicates
Changes in the requirements section.
(:requirements
:typing
:conditional-effects
:action-costs
:negative-preconditions)(:requirements
:typing
:derived-predicates
:disjunctive-preconditions
:existential-preconditions
:action-costs
:negative-preconditions)
2
The move-to-card action
conditional effects, direct effects only
Every move in the no-axioms version plants propagation markers.
The axiom version drops those; the planner evaluates
movable and part-of-tableau at every
state from their derivation rules.
(:action move-to-card
:parameters (?c - card ?from - card_or_tableau
?to - card ?totableau - tableau)
:precondition
(and
(not (currently-updating-movable))
(not (currently-updating-unmovable))
(not (currently-collecting-deck))
(not (currently-updating-part-of-tableau))
(not (currently-dealing))
(movable ?c) (in-play ?c)
(clear ?to) (in-play ?to)
(part-of-tableau ?to ?totableau)
(CAN-BE-PLACED-ON ?c ?to)
(on ?c ?from))
:effect
(and
(not (on ?c ?from)) (on ?c ?to)
(not (clear ?to)) (clear ?from)
(when (not (CAN-CONTINUE-GROUP ?c ?from))
(and (currently-updating-movable)
(make-movable ?from)))
(when (not (CAN-CONTINUE-GROUP ?c ?to))
(and (currently-updating-unmovable)
(make-unmovable ?to)))
(currently-updating-part-of-tableau)
(make-part-of-tableau ?c ?totableau)
(increase (total-cost) 1)))(:action move-to-card
:parameters (?c - card ?from - card_or_tableau
?to - card ?totableau - tableau)
:precondition
(and
(not (currently-collecting-deck))
(not (currently-dealing))
(movable ?c) (in-play ?c)
(clear ?to) (in-play ?to)
(part-of-tableau ?to ?totableau)
(CAN-BE-PLACED-ON ?c ?to)
(on ?c ?from))
:effect
(and
(not (on ?c ?from)) (on ?c ?to)
(not (clear ?to)) (clear ?from)
(increase (total-cost) 1)))
3
Propagating movable
8 zero-cost actions, 1 derived predicate
The eight propagation actions on the left simulate a fixed-point evaluation. The axiom on the right defines the same fixed-point declaratively. The planner evaluates it at every state.
(:action make-movable-and-continue
:parameters (?c - card ?next - card)
:precondition
(and (currently-updating-movable)
(not (currently-collecting-deck))
(on ?next ?c)
(make-movable ?c)
(CAN-CONTINUE-GROUP ?next ?c))
:effect
(and (movable ?c)
(not (make-movable ?c))
(make-movable ?next)))
(:action make-movable-and-stop
:parameters (?c - card ?next - card) ...)
(:action make-movable-ignore-pile
:parameters (?c - card) ...)
(:action make-unmovable-and-continue ...)
(:action make-unmovable-and-stop-at-tableau ...)
(:action make-unmovable-and-stop-at-unmovable ...)
;; plus change-tableau-and-continue,
;; change-tableau-and-stop
;; 8 zero-cost actions in total,
;; plus 4 control fluents and 3 marker
;; predicates to gate them.(:derived (movable ?c - card)
(and
(in-play ?c)
(or
(clear ?c)
(exists (?above - card)
(and (on ?above ?c)
(movable ?above)
(CAN-CONTINUE-GROUP ?above ?c))))))
;; In words: a card is movable if it is
;; in play, and either it is clear, or
;; some movable card directly above it
;; continues its group.
;;
;; The recursion (movable ?above) is the
;; fixed-point the eight actions on the
;; left simulate by hand.
4
Transitive closure: part-of-tableau
propagation actions, 4-line axiom
Same shape as section 3, applied to "which tableau does this card belong to". The axiom is the standard one-rule definition of transitive closure.
(:action change-tableau-and-continue
:parameters (?c - card ?tbefore - tableau
?t - tableau ?next - card)
:precondition
(and (currently-updating-part-of-tableau)
(not (currently-collecting-deck))
(on ?next ?c)
(make-part-of-tableau ?c ?t)
(part-of-tableau ?c ?tbefore))
:effect
(and (not (part-of-tableau ?c ?tbefore))
(part-of-tableau ?c ?t)
(not (make-part-of-tableau ?c ?t))
(make-part-of-tableau ?next ?t)))
(:action change-tableau-and-stop
:parameters (?c - card ?tbefore - tableau
?t - tableau) ...)
;; The shown action is only one of two
;; change-tableau-* propagation actions.
;; The encoding also needs:
;; - a marker predicate
;; make-part-of-tableau
;; - a flag
;; currently-updating-part-of-tableau
;; - a precondition on every real action
;; that blocks moves until propagation
;; has finished(:derived (part-of-tableau
?c - card ?t - tableau)
(or
(on ?c ?t)
(exists (?y - card)
(and (on ?c ?y)
(part-of-tableau ?y ?t)))))
;; Card c is part of tableau t if it is
;; directly on t, or it is on some card y
;; that is already part of t.
;;
;; A four-line transitive closure.Live demo
Same instance, two encodings, one race
Both terminals run
fast-downward.py
on opt p09 with A*(blind()).
Streaming live from the server.
More on the planner is at
fast-downward.org.
Task
Instance opt_p09
Search A*(blind()), optimal, no heuristic guidance
Equivalence check both encodings must reach the same plan cost
comparison across the four reported metrics
Results
Measured impact across all instances
Fast Downward, 5 min / 4 GB budget per instance.
No-axioms encoding Axioms encoding
Across all instances the axioms encoding produces about half as many grounded actions.
Note: The Y-axis uses a log scale so the largest instances do not dominate the chart; on a log scale a 50% reduction looks like a smaller visual gap than it is.
No-axioms, A* + LM-cut heuristic Axioms, A* + hmax heuristic
Both find the same optimal cost on every solved instance. The axioms encoding reaches it 4 to 9 times quicker.