Satplan (better known as Planning as Satisfiability) is a method for
automated planning
Automation describes a wide range of technologies that reduce human intervention in processes, namely by predetermining decision criteria, subprocess relationships, and related actions, as well as embodying those predeterminations in machines ...
. It converts the planning problem instance into an instance of the
Boolean satisfiability problem
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
, which is then solved using a method for establishing satisfiability such as the
DPLL algorithm
In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solvi ...
or
WalkSAT In computer science, GSAT and WalkSAT are local search algorithms to solve Boolean satisfiability problems.
Both algorithms work on formulae in Boolean logic that are in, or have been converted into conjunctive normal form. They start by assigni ...
.
Given a problem instance in planning, with a given initial state, a given set of actions, a goal, and a horizon length, a formula is generated so that the formula is satisfiable if and only if there is a plan with the given horizon length. This is similar to simulation of
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 ...
s with the satisfiability problem in the proof of
Cook's theorem. A plan can be found by testing the satisfiability of the formulas for different horizon lengths. The simplest way of doing this is to go through horizon lengths sequentially, 0, 1, 2, and so on.
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