Plan satelitarny

Satplan (lepiej znany jako Planning as Satisfiability) to metoda automatycznego planowania . Przekształca instancję problemu planowania w instancję problemu spełnialności Boole'a , który jest następnie rozwiązywany przy użyciu metody ustalania spełnialności, takiej jak algorytm DPLL lub WalkSAT .

Biorąc pod uwagę wystąpienie problemu w planowaniu, z zadanym stanem początkowym, danym zbiorem działań, celem i długością horyzontu, generowana jest formuła tak, że formuła jest spełnialna wtedy i tylko wtedy, gdy istnieje plan o danej długości horyzontu . Jest to podobne do symulacji maszyn Turinga z problemem spełnialności w dowodzie twierdzenia Cooka . Plan można znaleźć, testując spełnialność formuł dla różnych długości horyzontu. Najprostszym sposobem na to jest przejście przez kolejne długości horyzontu, 0, 1, 2 i tak dalej.

Zobacz też

• Grafplan

• HA Kautz i B. Selman (1992). Planowanie jako spełnialność . W Proceedings of the X European Conference on Artificial Intelligence (ECAI'92) , strony 359–363.
• HA Kautz i B. Selman (1996). Przesuwanie koperty: planowanie, logika zdań i wyszukiwanie stochastyczne . W Proceedings of the XIII National Conference on Artificial Intelligence (AAAI'96) , strony 1194–1201.
• J. Rintanena (2009). Planowanie i SAT . W A. Biere, H. van Maaren, M. Heule i Toby Walsh, red., Handbook of Satisfiability , strony 483–504, IOS Press.