# Satplan

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Satplan
> Markdown URL: https://mediated.wiki/source/Satplan.md
> Source: https://en.wikipedia.org/wiki/Satplan
> Source revision: 1307696137
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

{{short description|Method for automated planning}}
'''Satplan''' (better known as Planning as Satisfiability) is a method for [automated planning](/source/automated_planning).<ref>{{Cite web |last=Jeevanandam |first=Nivash |date=2023-11-16 |title=Understanding planning using logic in AI |url=https://indiaai.gov.in/article/understanding-planning-using-logic-in-ai |access-date=2025-02-19 |website=IndiaAI |language=en}}</ref><ref>{{Cite web |last=Kautz |first=Henry |last2=Selman |first2=Bart |date=August 1992 |title=Planning as Satisfiability |url=https://info.microkeeper.com.au/products/rostering-software |archive-url=https://web.archive.org/web/20190125183149/http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.35.9443&rep=rep1&type=pdf |archive-date=2019-01-25 |website=[CiteSeerX](/source/CiteSeerX) |publisher=ECAI'92}}</ref> It converts the planning problem instance into an instance of the [Boolean satisfiability problem](/source/Boolean_satisfiability_problem) (SAT), which is then solved using a method for establishing satisfiability such as the [DPLL algorithm](/source/DPLL_algorithm) or [WalkSAT](/source/WalkSAT).

== Methodology ==
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](/source/Cook-Levin_theorem), where [Turing machine](/source/Turing_machine) computations are represented as SAT formulas.<ref>{{Cite journal |last=Robinson |first=Nathan |last2=Gretton |first2=Charles |date=2009-10-16 |title=SAT-Based Parallel Planning Using a Split Representation of Actions |journal=Proceedings of the International Conference on Automated Planning and Scheduling |volume=19 |pages=281–288 |doi=10.1609/icaps.v19i1.13368 |issn=2334-0843|doi-access=free }}</ref>

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.<ref name=":0">{{Cite web |title=Planning as Satisfiability: state of the art |url=https://users.aalto.fi/~rintanj1/satplan.html |access-date=2025-02-19 |website=users.aalto.fi}}</ref>

==See also==

* [Graphplan](/source/Graphplan)

==References==
{{Reflist}}
* H. A. Kautz and B. Selman (1992). [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.35.9443&rep=rep1&type=pdf 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). [https://www.researchgate.net/profile/Bart_Selman/publication/2471954_Pushing_the_Envelope_Planning_Propositional_Logic_and_Stochastic_Search/links/549673960cf29b9448241893/Pushing-the-Envelope-Planning-Propositional-Logic-and-Stochastic-Search.pdf 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). [https://books.google.com/books?id=YVSM3sxhBhcC&q=%22planning+and+SAT%22 Planning and SAT]. In A. Biere, H. van Maaren, M. Heule and Toby Walsh, Eds., ''Handbook of Satisfiability'', pages 483–504, [IOS Press](/source/IOS_Press). {{ISBN|978-1-58603-929-5}}.

Category:Automated planning and scheduling

{{comp-sci-stub}}

---
Adapted from the Wikipedia article [Satplan](https://en.wikipedia.org/wiki/Satplan) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Satplan?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.