Satplan

Satplan (auch Planning as Satisfiability) ist ein Verfahren aus dem Gebiet der künstlichen Intelligenz. Dabei wird ein Planungsproblem in ein Erfüllbarkeitsproblem der Aussagenlogik (SAT) umgewandelt, das anschließend mit einem SAT-Verfahren wie dem DPLL-Algorithmus oder WalkSAT gelöst wird.

Verfahren

Bei Satplan werden der Anfangszustand, mögliche Aktionen, der Zielzustand und eine maximale Planungstiefe (Horizontlänge) in eine logische Formel überführt. Diese ist genau dann erfüllbar, wenn innerhalb der vorgegebenen Horizontlänge eine gültige Folge von Aktionen existiert, die vom Anfangszustand zum Zielzustand führt.

Um einen Plan zu finden, testet Satplan iterativ Formeln mit zunehmenden Horizontlängen. Dabei werden die Horizontlängen nacheinander (1, 2, 3, 4 usw.) überprüft, bis ein Plan gefunden wird. Für jeden Horizont wird eine entsprechende SAT-Formel generiert und von einem SAT-Solver überprüft. Ist die Formel erfüllbar, entspricht sie einem Plan dieser Horizontlänge. Ist sie nicht erfüllbar, wird mit der nächsten Horizontlänge fortgefahren. Obwohl dieser einfache Ansatz ineffizient sein kann, können fortgeschrittenere Suchstrategien die Leistung verbessern. Die grundlegende Idee bleibt aber dieselbe: die Planung auf Erfüllbarkeit reduzieren.

Literatur

• Henry Kautz, Bart Selman: Planning as satisfiability. In: Proceedings of the Tenth European Conference on Artificial Intelligence (ECAI'92). Wien August 1992, S. 359–363 (psu.edu [PDF]). 
• Henry Kautz, Bart Selman: Pushing the envelope: planning, propositional logic, and stochastic search. In: Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI'96). August 1996, S. 1194–1201 (aaai.org [PDF]). 
• J. Rintanen: Planning and SAT. In: A. Biere, H. van Maaren, M. Heule, Toby Walsh (Hrsg.): Handbook of Satisfiability. IOS Press, 2009, ISBN 978-1-58603-929-5, S. 483–504 (google.com).