ПЛАНИРОВАНИЕ С ПОМОЩЬЮ ПРОПОЗИЦИОНАЛЬНОЙ ЛОГИКИ
Как было описано в главе 10, планирование может осуществляться по принципу доказательства некоторой теоремы в рамках ситуационного исчисления. В подобной теореме утверждается, что при наличии начального состояния и аксиом состояния-преемника, которые описывают результаты действий, цель будет истинной в ситуации, которая является результатом некоторой последовательности действий. В такой ранний период развития искусственного интеллекта, как 1969 год, данный подход считался слишком неэффективным для того, чтобы с его помощью можно было находить интересные планы. Проведенные в последнее время разработки в области эффективных алгоритмов формирования рассуждений для пропозициональной логики (см. главу 7) привели к возрождению интереса к планированию с помощью логических рассуждений.
Подход, принятый в данном разделе, основан на проверке выполнимости логического высказывания, а не на доказательстве теорем. Мы будем отыскивать модели для пропозициональных высказываний, которые выглядят примерно так:
Начальное состояние л Все возможные описания действий л Цель
Такое высказывание должно содержать пропозициональные символы, соответствующие каждому возможному проявлению действия; модель, в которой выполняется это высказывание, должна присваивать значение true действиям, являющимся частью правильного плана, и false — другим действиям. Присваивание, которое соответствует неправильному плану, не будет моделью, поскольку окажется несовместимым с утверждением, что цель истинна. Если задача планирования неразрешима, то данное высказывание будет невыполнимым.
Описание задач планирования в пропозициональной логике
Процесс, который будет здесь применяться для перевода задач Strips на язык пропозициональной логики, представляет собой (так сказать) классический пример цикла представления знаний: мы начнем с множества аксиом, которое на первый взгляд кажется приемлемым, обнаружим, что эти аксиомы допускают появление фиктивных, не предусмотренных моделей, а затем запишем дополнительные аксиомы.
Начнем с очень простой задачи воздушной транспортировки. В начальном состоянии (время 0) самолет Рх находится в аэропорту SFO, а самолет Р2 — в аэропорту JFK. Задача состоит в том, чтобы Р1 находился в JFK, а Р2 — в SFO; иными словами, самолеты должны поменяться местами. Прежде всего, потребуются отдельные пропозициональные символы для формирования утверждений о каждом временном этапе. Для обозначения временного этапа будут использоваться верхние индексы, как и в главе 7. Поэтому начальное состояние можно записать следующим образом:
At(PllSFO)° Л At(P2,JFK)°
(Напомним, что At (Plt SFO)0 — это атомарный символ.) Поскольку в пропозициональной логике не принято предположение о замкнутом мире, необходимо также определить высказывания, которые не являются истинными в начальном состоянии. Если же некоторые высказывания в начальном состоянии не известны, они могут оставаться неопределенными (предположение об открытом мире). В данном примере зададим следующее:
—iAt (Pi, JFK) 0 Л -iAt (P2,SFO)°
Сама цель должна быть связана с конкретным временным этапом. Поскольку мы не знаем заранее, какое количество этапов потребуется для достижения цели, то можно попытаться сформулировать утверждение, что цель истинна в начальном состоянии, во время т=0. Это означает, что мы вводим утверждение At(Plt JFK)0 л At (Р2, SFO) °. Если эта попытка окажется неудачной, повторим ее снова во время Т=1 и т.д. до тех пор, пока не достигнем осуществимого плана с минимальной длиной. Для каждого значения т база знаний будет включать только высказывания, покрывающие временнь/е этапы от 0 вплоть до Т. Чтобы обеспечить завершение работы алгоритма, можно наложить произвольный верхний предел,
шах- Этот алгоритм приведен в листинге 11.7. Альтернативный подход, позволяющий избежать использования многочисленных попыток решения, обсуждается в упр. 11.17.
Листинг 11.7. Алгоритм SATplan. Задача планирования преобразуется в высказывание в форме CNF, в котором подтверждается истинность цели на фиксированном временном этапе Т, а аксиомы добавляются на каждом временном этапе вплоть до т. (Подробные сведения о преобразовании приведены в тексте главы.) Если алгоритм проверки выполнимости находит модель, то план извлекается путем поиска тех пропозициональных символов, которые относятся к действиям и которым в модели присвоено значение true. Если модель не существует, то процесс повторяется после передвижения цели на один этап дальше
function SATplan(problem, Ттах) returns решение solution или индикатор неудачи failure inputs: problem, задача планирования
Ттах, верхний предел длины плана
for Г = 0 tO Тщах <*0
cnf, mapping <— Translate-To-SAT {problem, T) assignment <— SAT-Solver ( cnf)
if присваивание assignment не является неопределенным then return Extract-Solution(assignment, mapping) return failure
Следующая проблема состоит в том, как закодировать описания действий в пропозициональной логике. Наиболее прямолинейный подход состоит в том, чтобы было предусмотрено по одному пропозициональному символу на каждое проявление действия; например, символ Fly(P1, SFO, JFK)0 является истинным, если самолет р1 вылетает из аэропорта SFO в аэропорт JFK во время 0. Как и в главе 7, мы запишем пропозициональные версии аксиом состояния-преемника, разработанных для ситуационного исчисления в главе 10. Например, имеет место следующее:
At(P\, JFK)1 (At (Pi, JFK) 0 л (Fly(P1,JFK,SFO)° A A t (P1, JFK) 0 ) )
v (Fly(Plf SFO, JFK)0 A At (Pi, SFO) 0 ) (11.1)
Это означает, что самолет Рх должен находиться в аэропорту JFK во время 1, если он был в JFK во время 0 и не улетел или если он был в аэропорту SFO во время 0 и прилетел в аэропорт JFK. Необходимо иметь по одной такой аксиоме для каждого самолета, аэропорта и временного этапа. Более того, каждый дополнительный аэропорт добавляет еще один способ путешествия из каждого конкретного аэропорта или в этот аэропорт и поэтому вносит еще больше дизъюнктов в правую часть каждой аксиомы.
После подготовки всех этих аксиом можно вызвать алгоритм проверки выполнимости, чтобы найти план. Это должен быть план, который достигает цели во время Т=1, а именно план, в котором эти два самолета меняются местами. Теперь предположим, что база знаний представляет собой следующее высказывание:
Начальное состояние л Аксиомы состояния-преемника л Цель1 (11.2)
в котором утверждается, что цель истинна во время т=1. Читатель может проверить, что утверждение, в котором символы
Fly(Plf SFO, JFK)0 и Fly(P2,JFK,SFO)°
являются истинными, а все другие символы действий являются ложными, представляет собой модель этой базы знаний. До сих пор все идет хорошо. Но есть ли другие возможные модели, которые способен вернуть этот алгоритм проверки выполнимости? Безусловно, да. Являются ли все эти другие модели удовлетворительными планами? К сожалению, нет. Рассмотрим довольно глупый план, заданный с помощью указанных символов действий:
Fly{PlfSFO,JFK)° и Fly(P1,JFK,SFO)° и Fly{P2/JFKlSFO)°
Этот план глуп потому, что самолет Р1 вначале находится в аэропорту SFO, поэтому действие Fly{Plf JFK, SFO)0 является неосуществимым. Тем не менее этот план действительно представляет собой модель высказывания из уравнения 11.2! Иными словами, он согласуется со всем, чтобы сказано до сих пор об этой задаче. Чтобы понять, чем может быть вызвано появление такого плана, мы должны проанализировать более тщательно, что сказано в аксиомах состояния-преемника (таких как уравнение 11.1) о действиях, предусловия которых не выполнены. Аксиомы правильно предсказывают, что ничего не произойдет при попытке выполнить подобное действие (см. упр. 11.15), но в них ничего не сказано, что такое действие не может быть выполнено! Чтобы предотвратить выработку планов с недопустимыми действиями, мы должны добавить аксиомы предусловий (precondition axiom), которые указывают, что для совершения любого действия требуется, чтобы были выполнены его предусловия6. Например, требуется указать следующее:
Fly(P1,JFK,SFO)° => At(PlfJFK)°
Поскольку указано, что в начальном состоянии символ At (Рг, JFK)0 является ложным, эта аксиома гарантирует, что в каждой модели символу Fly{P1, JFK, SFO)0 также будет присвоено ложное значение. После введения аксиом предусловия существует одна и только одна модель, которая удовлетворяет всем аксиомам, если цель должна быть достигнута во время 1, а именно модель, в которой самолет Рг летит в аэропорт JFK, а самолет Р2 — в аэропорт SFO. Обратите внимание на то, что это решение обеспечивает выполнение двух параллельных действий, как и при использовании алгоритма Graphplan или POP.
Неожиданности возникают после добавления третьего аэропорта, LAX. Теперь для каждого самолета имеются два действия, которые являются допустимыми в каждом состоянии. После применения алгоритма проверки выполнимости мы обнаружим, что модель с символами Fly(Plt SFO, JFK)0, а также Fly (Р2, JFK, SFO)0 и Fly (P2, JFK, LAX)0 удовлетворяет всем аксиомам. Это означает, что аксиомы состояния-преемника и аксиомы предусловия разрешают самолету вылететь в два аэропорта назначения одновременно! Предусловия для двух полетов самолета Р2 выполнены в начальном состоянии; аксиомы состояния-преемника указывают, что самолет Р2 должен находиться и в аэропорту SFO, и в аэропорту LAX во время 1, поэтому цель выполнена. Очевидно, что необходимо ввести дополнительные аксиомы для устранения таких фиктивных решений. Один из подходов состоит в том, что требуется ввести аксиомы исключения действий (action exclusion axiom), которые предотвращают одновременное выполнение несовместимых действий. Например, можно принудительно ввести полное исключение, добавив все возможные аксиомы в такой форме:
-(Fly(P2,JFK, SFO)0 A Fly(P2lJFK,LAX)°)
Эти аксиомы гарантируют, что никакие два действия не могут происходить одновременно. Они устранят все фиктивные планы, но приведут также к полному упорядочению каждого плана. В результате гибкость частично упорядоченных планов будет потеряна; кроме того, в результате увеличения количества временных этапов в плане может увеличиться продолжительность вычислений.
Вместо полного исключения можно потребовать только частичного исключения, т.е. предотвращения одновременных действий, только если они мешают друг другу. Применяемые при этом условия являются аналогичными условиям для взаимно исключающих действий: два действия не могут происходить одновременно, если одно из них отрицает предусловие или результат другого. Например, не могут происходить одновременно действия Fly (Р2, JFK, SFO)0 и Fly(P2, JFK, LAX) °, поскольку каждое из них отрицает предусловие другого; с другой стороны, действия Fly (Рх, SFO, JFK)0 и Fly{P2, JFK, SFO)0 могут осуществляться одновременно, поскольку в них два самолета не мешают друг другу. Частичное исключение позволяет устранять фиктивные планы, не вводя принудительно полное упорядочение.
Аксиомы исключения иногда выглядят как довольно слепой инструмент. Поэтому вместо формирования утверждения о том, что ни один самолет не может вылетать в два аэропорта одновременно, можно просто выдвинуть требование, чтобы ни один объект не мог находиться в двух местах одновременно:
Vp,x,y, txy=> -n(At{p,x)t A At(p,y)t)
Из этого факта, применяемого в сочетании с аксиомами состояния-преемника, следует, что самолет не может вылететь в два аэропорта одновременно. Факты, подобные этому, называются ограничениями состояния (state constraint). Безусловно, в пропозициональной логике необходимо будет записать все базовые экземпляры каждого ограничения состояния. Для задачи с аэропортами этого ограничения состояния будет достаточно, чтобы исключить все фиктивные планы. Ограничения состояния часто являются гораздо более компактными по сравнению с аксиомами исключения действия, но их не всегда можно легко вывести из первоначального описания задачи на языке Strips.
Подводя итог, отметим, что планирование в форме доказательства выполнимости предусматривает поиск моделей для высказывания, включающего описание начального состояния, цели, аксиом состояния-преемника, аксиом предусловий, а также либо аксиом исключения действия, либо аксиом ограничения состояния. Можно показать, что эта коллекция аксиом является достаточной, в том смысле, что при их использовании больше не возникают какие-либо фиктивные "решения". Любая модель, в которой выполняется такое пропозициональное высказывание, будет представлять собой действительный план для первоначальной задачи; это означает, что любая линеаризация этого плана будет представлять собой допустимую последовательность действий, которая позволяет достичь цели.