Сатплан - Satplan

Satplan (более известный как «Планирование как удовлетворение») - это метод автоматизированного планирования . Он преобразует экземпляр задачи планирования в экземпляр задачи логической выполнимости , которая затем решается с использованием метода установления выполнимости, такого как алгоритм DPLL или WalkSAT .

Учитывая пример проблемы в планировании, с заданным начальным состоянием, заданным набором действий, целью и длиной горизонта, формула генерируется так, что формула является выполнимой тогда и только тогда, когда существует план с заданной длиной горизонта. . Это похоже на моделирование машин Тьюринга с проблемой выполнимости в доказательстве теоремы Кука . План можно найти, проверив выполнимость формул для разных длин горизонта. Самый простой способ сделать это - пройти по горизонтали последовательно, 0, 1, 2 и так далее.

Смотрите также

Ссылки