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