Листинг 11.7. Алгоритм SATplan. Задача планирования преобразуется в высказывание в форме CNF, в котором подтверждается истинность цели на фиксированном временном этапе Т, а аксиомы добавляются на каждом временном этапе вплоть до т. (Подробные сведения о преобразовании приведены в тексте главы.) Если алгоритм проверки выполнимости находит модель, то план извлекается путем поиска тех пропозициональных символов, которые относятся к действиям и которым в модели присвоено значение true. Если модель не существует, то процесс повторяется после передвижения цели на один этап дальше

Следующая проблема состоит в том, как закодировать описания действий в пропозициональной логике. Наиболее прямолинейный подход состоит в том, чтобы было предусмотрено по одному пропозициональному символу на каждое проявление действия; например, символявляется истинным, если самолет Ρ1 вылетает из аэропорта SFO в аэропорт JFK во время 0. Как и в главе 7, мы запишем пропозициональные версии аксиом состояния-преемника, разработанных для ситуационного исчисления в главе 10. Например, имеет место следующее: