Сатплан
Satplan (более известный как Planning as Satisfiability) — это метод автоматизированного планирования . Он преобразует экземпляр задачи планирования в экземпляр задачи булевой выполнимости , которая затем решается с использованием метода установления выполнимости, такого как алгоритм DPLL или WalkSAT .
При заданном экземпляре задачи планирования с заданным начальным состоянием, заданным набором действий, целью и длиной горизонта генерируется формула, которая является выполнимой тогда и только тогда, когда существует план с заданной длиной горизонта. Это похоже на моделирование машин Тьюринга с проблемой выполнимости в доказательстве теоремы Кука . План может быть найден путем проверки выполнимости формул для различных длин горизонта. Самый простой способ сделать это — последовательно перебрать длины горизонта, 0, 1, 2 и т. д.
Смотрите также
Ссылки
- HA Kautz и B. Selman (1992). Планирование как выполнимость. В трудах Десятой Европейской конференции по искусственному интеллекту (ECAI'92) , страницы 359–363.
- HA Kautz и B. Selman (1996). Раздвигая границы: планирование, пропозициональная логика и стохастический поиск. В трудах Тринадцатой национальной конференции по искусственному интеллекту (AAAI'96) , страницы 1194–1201.
- J. Rintanen (2009). Планирование и SAT. В A. Biere, H. van Maaren, M. Heule и Toby Walsh, Eds., Справочник по выполнимости , страницы 483–504, IOS Press.
 | Эта статья по информатике — заглушка . Вы можете помочь Википедии, расширив ее. |
