Satplan (better known as Planning as Satisfiability) is a method for
automated planning
Automated planning and scheduling, sometimes denoted as simply AI planning, is a branch of artificial intelligence that concerns the realization of strategy, strategies or action sequences, typically for execution by intelligent agents, autonomou ...
. It converts the planning problem instance into an instance of the
Boolean satisfiability problem (SAT), which is then solved using a method for establishing satisfiability such as the
DPLL algorithm or
WalkSAT.
The process encodes key elements of the planning problem—initial state, available actions, goal state, and a maximum plan length (horizon length)—into a logical formula. This formula is satisfiable ''if and only if'' a valid sequence of actions exists that transforms the initial state into the goal state within the given horizon. This concept is similar to
Cook's theorem, where
Turing machine
A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
computations are represented as SAT formulas.
To find a plan, Satplan iteratively tests formulas with increasing horizon lengths. It starts with a horizon length of 0 (no actions) and incrementally increases it (1, 2, 3, etc.). For each horizon, a corresponding SAT formula is generated and checked by a SAT solver. If satisfiable, the solver’s output reveals the action sequence. If unsatisfiable, the process continues until a valid plan is found. While this simple approach can be inefficient, more advanced search strategies can improve performance, but the fundamental idea remains the same: reducing planning to satisfiability.
See also
*
Graphplan
References
* H. A. Kautz and B. Selman (1992)
Planning as satisfiability In ''Proceedings of the Tenth European Conference on Artificial Intelligence (ECAI'92)'', pages 359–363.
* H. A. Kautz and B. Selman (1996)
Pushing the envelope: planning, propositional logic, and stochastic search In ''Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI'96)'', pages 1194–1201.
* J. Rintanen (2009)
Planning and SAT In A. Biere, H. van Maaren, M. Heule and Toby Walsh, Eds., ''Handbook of Satisfiability'', pages 483–504,
IOS Press. .
Automated planning and scheduling
{{comp-sci-stub