Сб самолет
Satplan (более известный как «Планирование как выполнимость») — это метод автоматизированного планирования . Он преобразует экземпляр задачи планирования в экземпляр булевой проблемы выполнимости , который затем решается с использованием метода установления выполнимости, такого как алгоритм DPLL или WalkSAT .
Для данного экземпляра задачи в планировании с заданным начальным состоянием, заданным набором действий, целью и длиной горизонта генерируется формула, так что формула выполнима тогда и только тогда, когда существует план с заданной длиной горизонта. . Это похоже на моделирование машин Тьюринга с проблемой выполнимости в доказательстве теоремы Кука . План можно найти, проверив выполнимость формул для различных длин горизонта. Самый простой способ сделать это — последовательно просмотреть длину горизонта: 0, 1, 2 и т. д.
См. также [ править ]
Ссылки [ править ]
- Х.А. Кауц и Б. Селман (1992). Планирование как осуществимость . В материалах Десятой Европейской конференции по искусственному интеллекту (ECAI'92) , страницы 359–363.
- Х.А. Кауц и Б. Селман (1996). Выход за рамки: планирование, логика высказываний и стохастический поиск . В материалах тринадцатой национальной конференции по искусственному интеллекту (AAAI'96) , страницы 1194–1201.
- Дж. Ринтанен (2009). Планирование и SAT . В: А. Бьер, Х. ван Маарен, М. Хойл и Тоби Уолш, ред., «Справочник по выполнимости» , страницы 483–504, IOS Press.
 | Эта по информатике статья незавершена . Вы можете помочь Википедии, расширив ее . |