Труды КНЦ вып.9 (ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИ вып. 10/2018(9))

свою эффективность на практике. Также известны работы, направленные на преодоление описанных ограничений, связанных с обработкой времени [11] и вещественных величин в Graphplan [12]. Более подробное введение в Graphplan и расширения метода Graphplan можно найти в [13]. Изложенное показывает, что методы интеллектуального планирования напрямую зависят от возможностей языков представления задач планирования. Помимо представления задач планирования на языках типа STRIPS и ADL планирование может осуществляться по принципу доказательства некоторой теоремы в рамках ситуационного исчисления. В подобной теореме утверждается, что при наличии начального состояния и аксиом состояния-преемника, которые описывают результаты действий, цель будет истинной в ситуации, которая является результатом некоторой последовательности действий. В ранний период развития искусственного интеллекта данный подход считался слишком неэффективным для того, чтобы с его помощью можно было находить интересные планы. Проведенные в последнее время разработки в области эффективных алгоритмов формирования рассуждений для пропозициональной логики привели к возрождению интереса к планированию с помощью логических рассуждений. Близкий подход основан на проверке выполнимости логического высказывания, а не на доказательстве теорем [13]. Планировщики, основанные на проверке выполнимости, способны обрабатывать крупные задачи планирования. В алгоритме SATplan [14] задача планирования преобразуется в пропозициональные аксиомы и после этого к ним применяется алгоритм проверки выполнимости для поиска модели, соответствующей действительному плану. Основная идея планирования как выполнимости - угадать длину плана, перевести задачу планирования в набор пропозициональных формул и попытаться решить возникающую проблему выполнимости (SAT). Если формулы не удовлетворяются, то длина плана увеличивается, и процесс повторяется. На сегодняшний день изучено множество различных схем кодирования, но основная идея в большинстве этих схем состоит в том, чтобы иметь пропозициональную переменную: a) для каждого возможного действия на каждом этапе; b) для каждого возможного утверждения на каждом шаге. Каждая переменная действия указывает на наличие или отсутствие действия на определенном этапе плана. Каждая переменная утверждения указывает, истинно ли это утверждение на этом этапе плана. Лучшие планировщики SAT и планировщики на основе Graphplan имеют очень схожие характеристики. Они значительно превосходят POCL-планировщики на большинстве тестовых примеров. Подобно планировщикам POCL и Graphplan, планировщики SAT могут быть расширены, для поддержки операторов с кванторами и т.п. Фактически это расширение влияет только на процесс перевода задачи, а не на механизм решения. Вещественные величины, представляют более серьезные трудности. Вольфман [15] обрабатывает вещественные величины, используя линейное программирование в сочетании с методами планирования SAT. Перечислим наиболее серьезные недостатки подхода представления задач планирования в виде задачи SAT. Во-первых, количество переменных и утверждений может быть очень большим, потому что все возможные действия и 26