ВВЕДЕНИЕ 4
1. ИЗУЧЕНИЕ ИНСТРУМЕНТОВ ПЛАНИРОВАНИЯ SPIN И PDDL 5
1.1. SPIN 6
1.1.1. Поиск решения в Spin 7
1.2. PDDL 8
1.2.1. Поиск решения в PDDL 8
2. ИЗУЧЕНИЕ МЕТОДОВ РЕШЕНИЯ SAT-ЗАДАЧ DPLL И BDD 10
2.1. BDD 10
2.2. DPLL 12
3. ПЛАНИРОВАНИЕ И ВЫПОЛНИМОСТЬ 14
3.1. SATPlan 16
3.2. Символьная верификация на основе BDD 16
4. ЭКСПЕРИМЕНТАЛЬНОЕ СРАВНЕНИЕ ИНСТРУМЕНТОВ
ПЛАНИРОВАНИЯ И SAT-ПОДХОДОВ 17
4.1. Описание модели на Promela 17
4.2. Проведение эксперимента в SPIN 19
4.3. Описание модели на PDDL 20
4.4. Проведение эксперимента в PDDL 23
4.5. Проведение экспериментов в SATPlan: обедающие философы 24
4.6. Проведение экспериментов в SATPlan: Blocksworld 26
4.7. Экспериментальное сравнение PDDL и SATPlan на модели ханойской башни 28
4.8. Применение BDD-подхода в планировании Blocksworld 31
ЗАКЛЮЧЕНИЕ 34
СПИСОК ИСПОЛЬЗОВАННОЙ ЛИТЕРАТУРЫ 35
ПРИЛОЖЕНИЕ 1 37
ПРИЛОЖЕНИЕ 2 39
ПРИЛОЖЕНИЕ 3 41
ПРИЛОЖЕНИЕ 4
Планирование является, несомненно, важной составляющей жизни любого рационального человека. Планы определяют не только конечную цель, но и, что гораздо более важно, все промежуточные шаги на пути к её достижению. Но само составление планов может оказаться трудной задачей, особенно когда речь идёт о действительно сложных системах, а потому это дело в конечном итоге предоставили машинам. Это привело к возникновению термина «интеллектуальное планирование» и появлению специальных инструментов планирования. Однако, создав что-либо, человек редко останавливается на достигнутом – он совершенствует своё изобретение, и инструменты планирования не стали исключением. В связи с этим возникает вопрос: можно ли улучшить существующие системы планирования с помощью, в частности, известных подходов к решению задачи выполнимости SAT.
Актуальность данной работы обусловлена тем, что интеллектуальное планирование применяется во многих серьёзных областях, например, в сфере искусственного интеллекта, а значит, повышение эффективности первого способно значительным образом повлиять на второе.
В начале работы были поставлены следующие задачи: изучение инструментов планирования SPIN и PDDL и подходов к решению SATзадачи DPLL и BDD, их сравнение и исследование целесообразности модернизации указанных инструментов планирования с помощью названных подходов.
Целью работы является анализ потенциальной эффективности замещения внутренних алгоритмов SPIN и PDDL методами DPLL и BDD.
В процессе работы были изучены мануалы к инструментам планирования SPIN и PDDL, статьи по методам DPLL и BDD и их модернизациям и пр.
Подробный список можно найти в разделе литературы
В рамках данной работы был проведён обзор планировщиков PDDL и SPIN, а также существующих реализаций подходов DPLL и BDD и, дополнительно, системы SATPlan как примера SAT-планировщика. Нами были описаны модели на языках Promela и PDDL для проведения экспериментов по сравнению SATPlan, Spin и PDDL, а также библиотеки PBDD.
В ходе исследования и экспериментирования возникли определённые сложности, связанные с тем, что многие действительно готовые инструменты, реализующие SAT-подходы, использовали устаревшие (до 2006 г.) реализации алгоритмов DPLL и BDD, что является одним из недостатков данной работы.
По результатам экспериментальной части работы можно сделать выводы о том, что SAT-подходы достаточно эффективны и имеет смысл использовать комбинацию планировщиков и описанных выше подходов для повышения эффективности планирования в целом. Что касается более сложных моделей, для работы с ними выгоднее использовать более современные реализации SAT-решателей (как, например, DPLL, дополненный алгоритмами машинного обучения, описанную в [8]). Шагом в положительном направлении может также стать внедрение в готовые системы вроде SATPlan новых SAT-решателей, публикуемых, например, по итогам ежегодно проводимых соревнований SAT Competition.
