[ Министерство образования и науки Российской Федерации
УДК 004.4’242
ГРНТИ 20.01.01, 28.23.29
Инв. № 310275
УТВЕРЖДЕНО:
Исполнитель:
федеральное государственное бюджетное образовательное учреждение высшего профессионального
образования «Санкт-Петербургский национальный
исследовательский университет информационных
технологий, механики и оптики»
Ректор ФГБОУ ВПО «СПбНИУ ИТМО»
/ В.Н. Васильев/ М.П.
НАУЧНО-ТЕХНИЧЕСКИЙ
ОТЧЕТ о выполнении 4 этапа Государственного контракта № 16.740.11.0455 от 13 мая 2011 г. и Дополнению от 25 октября 2011 г. № 1 Исполнитель: федеральное государственное бюджетное образовательное учреждение высшего профессионального образования «Санкт-Петербургский национальный исследовательский университет информационных технологий, механики и оптики»Программа (мероприятие): Федеральная целевая программа «Научные и научнопедагогические кадры инновационной России» на 2009–2013 гг., в рамках реализации мероприятия № 1.2.1 Проведение научных исследований научными группами под руководством докторов наук.
Проект: Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для построения управляющих конечных автоматов Руководитель проекта: Шалыто Анатолий Абрамович Санкт-Петербург 2012 г.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для построения управляющих конечных автоматов Промежуточный отчет за IV этап
СПИСОК ОСНОВНЫХ ИСПОЛНИТЕЛЕЙ
по Государственному контракту 16.740.11.0455 от 13 мая 2011 на выполнение поисковых научно-исследовательских работ для государственных нужд Организация-Исполнитель: федеральное государственное бюджетное образовательное учреждение высшего профессионального образования «Санкт-Петербургский национальный исследовательский университет информационных технологий, механики и оптики».Руководитель темы:
А.А. Шалыто доктор технических наук, профессор Исполнители темы:
доктор технических наук, В.Г. Парфенов профессор Г.А. Корнеев кандидат технических наук, доцент А.С. Станкевич кандидат технических наук, доцент Ф.Н. Царев без ученой степени, без ученого звания М.В. Буздалов без ученой степени, без ученого звания В.И. Ульянцев без ученой степени, без ученого звания Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для без ученой степени, без ученого звания без ученой степени, без ученого звания Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
РЕФЕРАТ
Отчет 91 с., 1 ч., 7 рис., 1 табл., 20 источн., 3 прил.Ключевые слова: задача о выполнимости булевой формулы, управляющие автоматы, КНФ-формула.
В отчете представлены результаты исследований, выполненных по 4 этапу Государственного контракта № 16.740.11.0455 «Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для построения управляющих конечных автоматов» (шифр «2011-1.2.1-113-002») от мая 2011 по направлению «Проведение научных исследований научными группами под руководством докторов наук в области информатики» в рамках мероприятия 1.2. «Проведение научных исследований научными группами под руководством докторов наук», мероприятия 1.2 «Проведение научных исследований научными группами под руководством докторов наук и кандидатов наук», направления 1 «Стимулирование закрепления молодежи в сфере науки, образования и высоких технологий»
инновационной России» на 2009–2013 годы.
Цель работы – разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для построения управляющих конечных автоматов В Государственном контракте методы, использованные при выполнении отдельных видов работ (этапов), не предусмотрены.
инструментарий:
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036527.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036528.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036529.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036530.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036531.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036532.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036533.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036534.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036535.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036536.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036537.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036538.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036539.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036540.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036541.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036542.
Компьютер Aquarius Elt E50 S46. Инв. номер. 110104.7.0036543.
При выполнении патентных исследований и подготовке научно-технического отчета были использованы следующие нормативные документы:
• Постановление Правительства Российской Федерации от 4 мая 2005 г. № «О государственном учете результатов научно-исследовательских, опытноконструкторских и технологических работ гражданского назначения»;
• Гражданский кодекс РФ;
• ГОСТ 7.32-2001 «Система стандартов по информации, библиотечному и издательскому делу. Отчет о научно-исследовательской работе. Структура и правила оформления»;
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для № 16.740.11.0455 от 13 мая 2011 г. был создан научно-технический отчет, включающий выбор сторонней программы для решения задачи о выполнимости булевой формулы, план проведения экспериментальных исследований, подготовку заявки на регистрацию программы для ЭВМ, описание проведенных вычислительных экспериментов и анализ их результатов.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
ОГЛАВЛЕНИЕ
РЕФЕРАТОГЛАВЛЕНИЕ
ВВЕДЕНИЕ
ОСНОВНАЯ ЧАСТЬ – ЭКСПЕРИМЕНТАЛЬНОЕ ИССЛЕДОВАНИЕ
РАЗРАБОТАННОГО МЕТОДА МАШИННОГО ОБУЧЕНИЯ
1. ВЫБОР СТОРОННЕЙ ПРОГРАММЫ ДЛЯ РЕШЕНИЯ ЗАДАЧИ О
ВЫПОЛНИМОСТИ БУЛЕВОЙ ФОРМУЛЫ 1.1. АЛГОРИТМЫ РЕШЕНИЯ ЗАДАЧИ О ВЫПОЛНИМОСТИ БУЛЕВОЙ ФОРМУЛЫ................. 1.2. СОРЕВНОВАНИЯ СРЕДИ
ПРОГРАММ ДЛЯ РЕШЕНИЯ ЗАДАЧИ О
1.3. ВЫБОР СТОРОННЕЙ ПРОГРАММЫ ДЛЯ РЕШЕНИЯ ЗАДАЧИ О
ВЫПОЛНИМОСТИ БУЛЕВОЙ ФОРМУЛЫ1.3.1. Описание выбранных однопоточных программных средств.................. 1.3.2. Описание выбранных многопоточных программных средств................ 1.3.3. Выбор сторонней программы для решения задачи о выполнимости булевой формулы
ВЫВОДЫ ПО ГЛАВЕ 1
2. СОСТАВЛЕНИЕ ПЛАНА ПРОВЕДЕНИЯ ЭКСПЕРИМЕНТАЛЬНЫХ
ИССЛЕДОВАНИЙ3. ПОДГОТОВКА ЗАЯВКИ НА РЕГИСТРАЦИЮ ПРОГРАММЫ ДЛЯ ЭВМ.............. 4. ПРОВЕДЕНИЕ ВЫЧИСЛИТЕЛЬНЫХ ЭКСПЕРИМЕНТОВ
5. АНАЛИЗ РЕЗУЛЬТАТОВ ВЫЧИСЛИТЕЛЬНЫХ ЭКСПЕРИМЕНТОВ
5.1. АНАЛИЗ РЕЗУЛЬТАТОВ ПЕРВОГО ЭТАПА ВЫЧИСЛИТЕЛЬНЫХ
ЭКСПЕРИМЕНТОВРазработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
5.2. АНАЛИЗ РЕЗУЛЬТАТОВ ВТОРОГО ЭТАПА ВЫЧИСЛИТЕЛЬНЫХ
ЭКСПЕРИМЕНТОВВЫВОДЫ ПО ГЛАВЕ 5
6. ПОДГОТОВКА СТАТЬИ ДЛЯ ПУБЛИКАЦИИ В ЖУРНАЛЕ ИЗ
ПЕРЕЧНЯ ВАКЗАКЛЮЧЕНИЕ
СПИСОК ЛИТЕРАТУРЫ
ПРИЛОЖЕНИЕ А. КОПИЯ СОПРОВОДИТЕЛЬНОГО ПИСЬМА ЗАЯВКИ
НА РЕГИСТРАЦИЮ ПРОГРАММЫ ДЛЯ ЭВМ
ПРИЛОЖЕНИЕ Б. ПРОТОКОЛЫ ВЫЧИСЛИТЕЛЬНЫХ
ЭКСПЕРИМЕНТОВПРИЛОЖЕНИЕ В. КОПИЯ СПРАВКИ И ТЕКСТ СТАТЬИ
ВВЕДЕНИЕ
МУРАВЬИНЫЕ АЛГОРИТМЫ
УПРАВЛЯЮЩИЕ КОНЕЧНЫЕ АВТОМАТЫ
ПРЕДЛАГАЕМЫЙ МЕТОД ПОСТРОЕНИЯ УПРАВЛЯЮЩИХ
АВТОМАТОВ НА ОСНОВЕ МУРАВЬИНЫХ АЛГОРИТМОВЭКСПЕРИМЕНТАЛЬНОЕ ИССЛЕДОВАНИЕ
ЗАКЛЮЧЕНИЕ
ЛИТЕРАТУРА
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
ВВЕДЕНИЕ
«Экспериментальное исследование разработанного метода машинного обучения»машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для построения управляющих конечных автоматов», выполняемых в рамках государственного контракта, заключенного между Министерством образования и науки Российской Федерации и государственным образовательным учреждением высшего профессионального образования «Санкт-Петербургский государственный университет информационных технологий, механики и оптики» в соответствии с решением Конкурсной комиссии Министерства образования и науки Российской Федерации № 1 (протокол от 25.03.2011 № 3/0173100003711000031) по лоту шифр «2011-1.2.1-113-002» «Проведение научных исследований научными группами под руководством докторов наук в области информатики» в рамках федеральной целевой программы «Научные и научно-педагогические кадры инновационной России» на 2009–2013 годы, утвержденной постановлением Правительства Российской Федерации от 28 июля 2008 года № 568 «О федеральной целевой программе «Научные и научнопедагогические кадры инновационной России» на 2009–2013 годы».
Целями настоящего этапа являются:
1. Выбор сторонней программы для решения задачи о выполнимости булевой 2. Составление плана проведения экспериментальных исследований.
3. Подготовка заявки на регистрацию программы для ЭВМ.
4. Проведение вычислительных экспериментов.
5. Анализ результатов вычислительных экспериментов.
6. Подготовка статьи для публикации в журнале из перечня ВАК.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Выполнение работ настоящего этапа позволяет в дальнейшем разработать машинного обучения.
Отчет имеет следующую структуру. В первой главе проводится выбор сторонней программы для решения задачи о выполнимости булевой формулы. Описываются алгоритмы и основные сторонние средства решения задачи о выполнимости булевой формулы. Во второй главе приводится план проведения экспериментальных исследований.
В третьей главе приводится описание подготовленной заявки на регистрацию программы для ЭВМ. В четвертой главе приводится описание процесса проведения вычислительных экспериментов.
В пятой главе приводится анализ результатов вычислительных экспериментов. В шестой главе приводится описание подгоовленной статьи для публикации в журнале из перечня ВАК.
Основные главы снабжены выводами, кратко резюмирующими содержание главы. В заключении дается общая оценка работ по этапу.
Машинное обучение [2] – современный раздел информатики, посвященный созданию алгоритмов, которые обучают параметры некоторой модели на заранее подготовленных тестовых примерах, либо в процессе моделирования ее работы в некоторой внешней среде (обучение «на собственных ошибках»).
Задача о выполнимости булевой формулы – одна из задач, имеющих большое значение в информатике. Она состоит в том, чтобы по заданной булевой формуле найти такой набор значений входящих в нее переменных, что результат вычисления формулы – «истина». Эта задача относится к классу NP-полных задач, но для ее решения существует большое количество весьма эффективных на практике программных средств. Наиболее современные из этих программных средств, такие как zChaff [20], Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для MiniSat [12], CryptoMiniSat [10], Plingeling [7], способны обрабатывать формулы длиной в несколько миллионов символов, содержащие десятки и сотни тысяч переменных.
С использованием этих программных средств в настоящее время решаются такие задачи, как проверка эквивалентности формальных моделей программ, верификация моделей программ, формальная верификация микропроцессоров, генерация тестовых шаблонов, разводка печатных плат и т. д.
Автоматное программирование [3] – парадигма программирования, при использовании которой программу предлагается разрабатывать в виде совокупности автоматизированных объектов управления, каждый из которых содержит систему управления (взаимодействующие конечные автоматы) и объект управления.
Объект управления характеризуется множеством вычислительных состояний, а также двумя наборами функций: множеством предикатов, отображающих вычислительное состояние в логическое значение («истина» или «ложь»), и множеством действий, позволяющих изменять вычислительное состояние. Управляющий автомат определяется конечным множеством управляющих состояний, функцией переходов и функцией действий.
Исследования, проводимые в ряде университетов мира (например, в Стэнфордском университете), показывают, что модели, основанные на состояниях, целесообразно применять для построения систем со сложным поведением. Такие системы могут в ответ на одно и то же входное воздействие вырабатывать различные выходные воздействия в зависимости от предыстории работы.
Модели, основанные на состояниях, широко применяются в машинном обучении. Примером таких моделей являются Марковские цепи и скрытые Марковские модели [14]. Они могут применяться в таких задачах, как распознавание речи, и для них разработан ряд алгоритмов обучения. Область их применения ограничивается тем, что Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для эти модели имеют вероятностный характер. Наиболее близкими к ним моделями, имеющими детерминированный характер, являются конечные автоматы.
Важным достоинством автоматных программ является возможность их автоматической верификации [1], что является очень существенным свойством для систем с повышенными требованиями к надежности. Для этих систем важную роль играет влияние человеческого фактора на процесс разработки. Поэтому актуальной задачей является разработка методов машинного обучения для построения конечных автоматов.
Как правило, в машинном обучении конечные автоматы рассматриваются как распознаватели регулярных языков [4], или как преобразователи слов одного регулярного языка в слова другого. В случае построения управляющих автоматов обычно рассматриваются системы с малым числом входных переменных (одной или двумя), что существенно ограничивает область применения таких алгоритмов.
Кроме этого, большая часть существующих алгоритмов машинного обучения для конечных автоматов основана на принципе обучения «на собственных ошибках» и не являются достаточно эффективными для ряда задач, так как не позволяют эффективно учитывать знания человека. В свою очередь, алгоритмы, основанные на принципе обучения на примерах, обладают недостаточно высокой производительностью для использования на практике – они позволяют работать с автоматами, содержащими пятьдесять состояний, а суммарная длина обучающих примеров может составлять не более двухсот-трехсот событий. Построение автомата с помощью существующих алгоритмов может занимать от нескольких минут до нескольких дней.
Для устранения недостатков существующих методов разрабатывается метод машинного обучения, основанный на решении задачи о выполнимости булевой формулы. В качестве входных данных этот метод будет использовать сценарии работы – один из типов обучающих примеров (тестов). Предварительные исследования Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для показывают, что новый метод будет демонстрировать существенно более высокую производительность и сможет строить автоматы с десятками состояний, а размер входных данных сможет составлять тысячи событий.
Изложенное позволяет утверждать, что результаты выполнения научноисследовательской работы будут превышать мировой уровень разработок в рассматриваемой области.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
ОСНОВНАЯ ЧАСТЬ – ЭКСПЕРИМЕНТАЛЬНОЕ ИССЛЕДОВАНИЕ
РАЗРАБОТАННОГО МЕТОДА МАШИННОГО ОБУЧЕНИЯ
В основной части отчета изложены результаты выполнения следующих работ:1. Выбор сторонней программы для решения задачи о выполнимости булевой 2. Составление плана проведения экспериментальных исследований.
3. Подготовка заявки на регистрацию программы для ЭВМ.
4. Проведение вычислительных экспериментов.
5. Анализ результатов вычислительных экспериментов.
6. Подготовка статьи для публикации в журнале из перечня ВАК.
1. ВЫБОР СТОРОННЕЙ ПРОГРАММЫ ДЛЯ РЕШЕНИЯ ЗАДАЧИ О
ВЫПОЛНИМОСТИ БУЛЕВОЙ ФОРМУЛЫ
В настоящей главе проводится выбор сторонней программы для решения задачи о выполнимости булевой формулы. Описываюся основные алгоритмы решения задачи о выполнимости булевой формулы. Описываются проводимые соревнования среди программ для решения задачи о выполнимости булевой формулы. Затем производится выбор сторонних программ для проведения вычислительных экспериментов.
1.1. АЛГОРИТМЫ РЕШЕНИЯ ЗАДАЧИ О ВЫПОЛНИМОСТИ БУЛЕВОЙ ФОРМУЛЫ
Большинство программных средств для решения задачи о выполнимости булевой формулы основаны на алгоритме DPLL [11] и на его модернизированной версии – алгоритме CDCL [9]. Вкратце опишем данные алгоритмы.DPLL – алгоритм Дэвиса–Патнема–Логемана–Лавленда, разработанный ими в 1962 году. За основу взят алгоритм поиска с возвратом.
Основной алгоритм с возвратом начинается с выбора переменной, присвоения ей значения «истина», упрощения формулы и затем рекурсивной проверки упрощенной Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для формулы на выполнимость. Если упрощенная формула выполнима, то исходная формула тоже выполнима. Иначе, процедура повторяется, но выбранной переменной задается значение «ложь». Этот подход называется «правилом разбиения», так как он разбивает задачу на две более простые подзадачи. Шаг упрощения заключается в том, что из формулы удаляются все дизъюнкты, которые становятся истинными после присвоения выбранной переменной значения «истина» и удаления из оставшихся дизъюнктов всех вхождений этой переменной, которые становятся ложными.
Алгоритм DPLL позволяет улучшить основной алгоритм с возвратом за счет использования следующих правил на каждом шаге.
Рассмотрим метод распространения переменной. Если дизъюнкт содержит ровно одну переменную, которой еще не задали значение, этот дизъюнкт может принять значение «истина» только в случае присвоения переменной значения, которое сделает ее истинной («истина», если переменная входит в дизъюнкт без отрицания, и «ложь», если переменная входит с отрицанием). Таким образом, на данном шаге не требуется делать выбор переменной. На практике за этим следует каскад присвоений переменным значений, таким образом, существенно сокращается количество вариантов перебора.
переменная входит в дизъюнкты КНФ-формулы либо только без отрицаний, либо только с отрицаниями, она называется чистой. Чистым переменным всегда можно задать значение так, что все содержащие их дизъюнкты станут истинными. Таким образом, эти дизъюнкты не будут влиять на пространство вариантов, и их можно удалить.
Невыполнимость при данных конкретных значениях переменных определяется тем, что один из дизъюнктов становится пустым, то есть всем ее переменным задаются значения таким образом, что их вхождения (с отрицанием или без него) становятся Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для ложными. Выполнимость формулы констатируется тогда, когда или всем переменным заданы значения так, что не возникло пустых дизъюнктов, или если все дизъюнкты равны истине. Иллюстрация работы алгоритма DPLL приведена на рис. 1 (взята со страницы http://50-56-189-184.static.cloud-ips.com/wordpress/wp-content/uploads/2011/06/soos_summerschool.pdf).
Алгоритм CDCL (conflict-driven clause learning), основанный на DPLL, может содержать следующие модификации, описание к которым в настоящем отчете не приводится:
обучаемость новым дизъюнктам во время поиска с возвратом;
использование структуры конфликтов во время обучения;
использование ленивых структур данных для хранения формул;
низкую, не более чем полиномиальную вычислительную сложность использование периодического перезапуска алгоритма поиска с возвратом;
другие оптимизации, специфичные для определенных приложений.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
1.2. СОРЕВНОВАНИЯ СРЕДИ ПРОГРАММ ДЛЯ РЕШЕНИЯ ЗАДАЧИ О
ВЫПОЛНИМОСТИ БУЛЕВОЙ ФОРМУЛЫ
В последние годы был проведен ряд соревнований среди методов решения задачи о выполнимости булевой формулы [18]. Данные методы принимают на вход КНФ-формулу в формате DIMACS [17]. Опишем способы сравнения данных методов на соревнованиях.В соревнованиях методы сравнивались и ранжировались отдельно на тестовых наборах трех типов тестов – булевых КНФ-формул:
прикладные (application, industrial) – формулы, решения которых изготовленные (crafted, handmade, hard combinatorial) – специально подготовленные организаторами соревнований формулы;
случайные (random) – случайным образом полученные формулы.
На рис. 2 (взят со страницы http://baldur.iti.uka.de/sat-race-2010/downloads.html) приведены характеристики 100 прикладных КНФ-формул, которые были использованы для сравнения программ решения задачи о выполнимости булевой формулы на соревновании SAT Race 2010.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Рис. 2. Число переменных и дизъюнктов в КНФ-формулах, Также отдельно (для каждого типа набора тестов) методы решения задачи о выполнимости булевой формулы сравниваются в категориях «SAT+UNSAT», «SAT» и «UNSAT». Опишем смысл этих категорий:
SAT – сравнение производится по числу решенных за отведенное время (обычно 15 или 30 минут процессорного времени) КНФ-формул;
UNSAT – сравнение производится по числу КНФ-формул, для которых было верно предсказано отсутствие решения за отведенное время;
SAT+UNSAT – сравнение методов производится по сумме верно решенных Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Методы сортируются сначала по числу верно решенных формул, затем по среднему времени их решения. На рис. 3 (взят со страницы http://baldur.iti.uka.de/satrace-2010/downloads.html) приведено сравнение программ на обозначенных КНФформулах.
Рис. 3. Сравнение программ на соревновании SAT Race 2010 по числу На последнем соревновании SAT Challenge 2012 [16] также на обозначенных категориях тестов отдельно рассматривались и сравнивались методы с одним ядром решения (Single-Engine), с взаимодействующими ядрами решения (Interacting MultiEngine), с невзаимодействующими несколькими ядрами решения (Portfolio Approach), работающие на нескольких процессорах (Parallel).
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
1.3. ВЫБОР СТОРОННЕЙ ПРОГРАММЫ ДЛЯ РЕШЕНИЯ ЗАДАЧИ О
ВЫПОЛНИМОСТИ БУЛЕВОЙ ФОРМУЛЫ
В настоящем разделе проводится выбор сторонней программы для решения задачи о выполнимости булевой формулы. Описываются выбранные однопоточные и многопоточные программные средства.1.3.1. Описание выбранных однопоточных программных средств обозначенных соревнований.
Glucose – основан на реализации MiniSAT 2006-го года [19]. В реализацию внесено небольшое число изменений, целью ставилась победа лишь в категории UNSAT соревнования SAT Competition 2009. Введено расстояние между блоками литералов (LBD), что показало крайне высокую эффективность на соревнованиях SAT Competition 2009/2011 [18].
GlueMiniSAT использует алгоритм CDCL. К исходному алгоритму также добавлено LBD, но не исходная, а ограниченная версия – «прямой» LBD.
PrecoSAT – используется алгоритм CDCL с препроцессингом исходной формулы BCE (blocked clause elimination). Разрабатывался для 32-битной системы, что вызывает увеличение затрат по памяти на 64-битных системах.
Lingeling – основан на программе PrecoSAT. В отличие от предшественника в данном решении сделан упор на значительное уменьшение используемой оперативной памяти. Имеет свой сборщик мусора для уменьшения потребляемой памяти и общего прироста производительности. Разрабатывался с полной поддержкой 64-битных систем.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Clasp – в отличие от других решений, Clasp не основан на CDCL. Он построен по парадигме ASP (answer set programming). Главным отличием от других решений является отсутствие обучения «хорошим» дизъюнктам на этапе поиска с возвратом.
1.3.2. Описание выбранных многопоточных программных средств обозначенных соревнований.
Clasp MT – представляет собой многопоточную версию программы Clasp.
Plingeling – многопоточная версия Lingeling, реализована с использованием технологии PTreads. Поток-координатор поддерживает работу нескольких рабочих потоков. Данные потоки различаются лишь начальным случайным числом, которое задает последовательность, по которой описанный ранее алгоритм DPLL будет разбивать исходную формулу.
ManySAT – запускает в разных потоках различные модификации алгоритма CDCL на исходных данных. Как только какой-либо из потоков находит решение, выполнение оставшихся потоков прерывается.
QuteRSAT – основан на алгоритме DPLL без серьезных модификаций. Результаты исследований показывают, что немодифицированный алгоритм DPLL справляется с поставленными задачами гораздо хуже, чем модифицированный алгоритм CDCL.
Cryptominisat – создавался с целью исследования в области криптографического анализа. В отличие от большинства программных средств решений Cryptominisat не специализирован для решения узкого спектра задач. Распространяется по лицензии LGPL. Реализован на базе модернизированного алгоритма CDCL. Как и программное средство Lingeling, имеет свой сборщик мусора.
Ppfolio [15] – состоит из набора сторонних программных средств решения задачи о выполнимости булевой формулы. Ppfolio запускает в четырех потоках программные Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для средства TNM, Clasp, Cryptominisat, March_hi, а на всех оставшихся свободных ядрах запускается программа Plingeling.
1.3.3. Выбор сторонней программы для решения задачи о выполнимости Для проведения экспериментальных исследований были выбраны следующие однопоточные программные средства решения задачи о выполнимости булевой формулы:
Также использовались следующие многопоточные программные средства:
Отдельное исследование будет проведено с использованием программного средства CryptoMiniSAT, так как имеется возможность использовать данное программное средство в операционной системе Windows.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
ВЫВОДЫ ПО ГЛАВЕ
1. Описаны основные алгоритмы решения задачи о выполнимости булевой формулы.2. Описаны проводимые соревнования среди программ для решения задачи о выполнимости булевой формулы.
3. Произведен выбор сторонних программ для проведения вычислительных экспериментов и выбор основного программного средства CryptoMiniSAT.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
2. СОСТАВЛЕНИЕ ПЛАНА ПРОВЕДЕНИЯ ЭКСПЕРИМЕНТАЛЬНЫХ
ИССЛЕДОВАНИЙ
Экспериментальное исследование будет проведено в два этапа. Сначала будет проведено экспериментальное исследование построения автоматов с 5, 10, 15 и состояниями для входных данных (сценариев работы) различного размера – 250, 500, 750, 1000, 1250, 1500, 1750, 2000, 2250, 2500 элементов сценариев суммарно. Данное исследование будет проведено с использованием программного средства CryptoMiniSat экспериментального исследования:вероятность присутствия каждого из возможных переходов в искомом число различных входных событий равно двум;
число различных выходных воздействий равно двум;
число переменных равно двум;
наименьшее число выходных воздействий на переходе автомата равно наибольшее число выходных воздействий на переходе автомата равно на каждой комбинации числа состояний и размера входных данных помимо сочетаний (15, 250), (20, 250) и (20, 500) проводится 100 запусков;
параметры командной строки: «java -Xmx6G -Xss2G -jar».
Второй этап экспериментальных исследований проводится для сравнения обозначенных однопоточных и параллельных средств решения задачи о выполнимости булевой формулы. В отличие от первого этапа будут исследованы задачи построения автоматов с большим числом состояний, а суммарная длина сценариев работы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для фиксированного числа состояний искомого автомата варьироваться не будет. Опишем параметры данных экспериментальных исследований:
ограничение на время работы стороннего программного средства для решения одной задачи составляет 15 минут;
суммарная длина сценариев работы в 110 раз больше числа состояний длина каждого сценария не превышает 25;
используется одна переменная (переходы искомого автомата помечены «x»
для каждого программного средства и фиксированного числа состояний.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
3. ПОДГОТОВКА ЗАЯВКИ НА РЕГИСТРАЦИЮ ПРОГРАММЫ ДЛЯ ЭВМ
В процессе выполнения НИР подана заявка на регистрацию программы для ЭВМ «Программное средство для построения КНФ-формулы по графу совместимости вершин дерева сценариев работы программы». Копия сопроводительного письма заявки на регистрацию программы для ЭВМ приведена в приложении А.Программа предназначена для автоматического построения КНФ-формулы по графу совместимости. Входными данными программы является граф совместимости дерева сценариев работы программы и ожидаемое число состояний соответствующего сценариям работы управляющего автомата. Выходными данными алгоритма является КНФ-формула в формате DIMACS.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
4. ПРОВЕДЕНИЕ ВЫЧИСЛИТЕЛЬНЫХ ЭКСПЕРИМЕНТОВ
Первый этап экспериментальных исследований был проведен на компьютере с процессором Intel Core i5-2520M (2.5 GHz). На описанных входных данных программное средство CryptoMiniSat использовало до 3.5 гигабайт оперативной памяти для решения КНФ-формул, содержащих до 35 000 переменных и 9 дизъюнктов. Приложение Б содержит протоколы вычислительных экспериментов первого этапа.Второй этап экспериментальных исследований проводился на сервере компании Amazon [6], предоставляющий облачный сервер с микропроцессорной архитектурой Intel Xeon и процессором, обладающим восьмью ядрами. Общая продолжительность второго этапа исследований составила 89 часов. В распоряжении выбранных программ находилось около 70 гигабайт памяти оперативного запоминающего устройства и восемь выделенных ядер процессоров Intel Xeon 5550.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
5. АНАЛИЗ РЕЗУЛЬТАТОВ ВЫЧИСЛИТЕЛЬНЫХ ЭКСПЕРИМЕНТОВ
Настоящий раздел содержит анализ результатов вычислительных экспериментов.
5.1. АНАЛИЗ РЕЗУЛЬТАТОВ ПЕРВОГО ЭТАПА ВЫЧИСЛИТЕЛЬНЫХ
ЭКСПЕРИМЕНТОВ
На рис. 4 приведен график, показывающий зависимость времени работы программного средства CryptoMiniSat от параметров входных данных. На графике для каждой комбинации числа состояний искомого автомата и суммарной длины сценариев работы приведено медианное значение среди 100 вычислительных экспериментов, протоколы которых приведены в приложении Б.Рис. 4. Медианное время решения задачи в зависимости от Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Из приведенного графика видно, что предложенный алгоритм меньше чем за предложенных задач построения управляющих автоматов. Генетический алгоритм, Из Из приведенного графика видно, что предложенный алгоритм меньше чем за минуту работы персонального компьютера справляется с большинством предложенных задач построения управляющих автоматов. Генетический алгоритм, предложенный в [4] для решения аналогичной задачи, на задачах построения управляющих автоматов с пятью состояниями показал бы на порядок меньшую производительность, а на задачах построения автоматов с большим числом состояний производительность генетического алгоритма неприемлимо низка.
Отметим, что на приведенных задачах (от 5 до 20 состояний искомого автомата) алгоритм, используя программное средство CryptoMiniSat, всегда находит решение.
5.2. АНАЛИЗ РЕЗУЛЬТАТОВ ВТОРОГО ЭТАПА ВЫЧИСЛИТЕЛЬНЫХ
ЭКСПЕРИМЕНТОВ
экспериментов можно сделать вывод, что многопоточные алгоритмы справляются с поставленными задачами гораздо лучше, чем их однопоточные аналоги. В табл. приведены доли решенных задач для каждого сочетания программного средства и числа состояний искомого автомата.Таблица 1. Доля успешных запусков программных средств на задачах построения управляющих автоматов с большим числом состояний Число Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Проведем анализ не только части решенных задач, но и затраченного времени каждым из выбранных программных средств. На рис. 5 приведен график усредненного (по 10 запускам) времени работы шести многопоточных программных средств в зависимости от числа состояний искомого автомата (и, соответственно, размера входных данных). Маркеры исследований, в которых не были решены все 10 задач, обозначены заполненными фигурами.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Рис. 5. Время работы многопоточных программных средств в зависимости от числа состояний искомого автомата На рис. 6 приведен график усредненного (по 10 запускам) времени работы пяти однопоточных программных средств в зависимости от числа состояний искомого автомата (и, соответственно, размера входных данных).
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Рис. 6. Время работы однопоточных программных средств в зависимости от числа состояний искомого автомата На приведенных графиках можно наблюдать, что в среднем время работы растет с увеличением числа состояний искомого автомата и суммарной длины сценариев работы, поданых на вход предложенному алгоритму. Однако, специфика задачи и программных средств такова, что предугадать время решения конкретной задачи затруднительно.
На рис. 7 представлены для сравнения однопоточные и многопоточные экспериментов.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Рис. 7. Время работы лучших однопоточных и многопоточных программных средств в зависимости от числа состояний искомого Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
ВЫВОДЫ ПО ГЛАВЕ
1. Проведен анализ результатов первого этапа вычислительных экспериментов. Анализ показал, что программное средство CryptoMiniSAT успешно справляется с решением задач различной сложности. При этом число состояний искомого автомата варьировалось от 5 до 20.2. Проведен анализ результатов второго этапа вычислительных экспериментов. Анализ показал, что программное средство CryptoMiniSAT наравне с некоторыми другими многопоточными программными средствами справляется с решением задач с большим числом состояний (от 20 до 30). Таким образом, экспериментальные исследования показали обоснованность выбора данного программного средства.
3. Предложенный метод машинного обучения показал производительность во много раз большую, чем существующие методы машинного обучения.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
6. ПОДГОТОВКА СТАТЬИ ДЛЯ ПУБЛИКАЦИИ В ЖУРНАЛЕ ИЗ ПЕРЕЧНЯ ВАК
По результатам НИР в журнале «Научно-технический вестник информационных технологий, механики и оптики» 2012, № 6 будет опубликована статья. Копия справки и текст статьи приведены в приложении В.Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
ЗАКЛЮЧЕНИЕ
В результате исследований на четвертом этапе работ по контракту были выполнены следующие работы:выбрана сторонняя программа для решения задачи о выполнимости составлен план проведения экспериментальных исследований;
подготовлена заявка на регистрацию программы для ЭВМ;
проведены вычислительные эксперименты;
проведен анализ результатов вычислительных экспериментов;
подготовлена статья для публикации в журнале из перечня ВАК.
Таким образом, были решены все задачи четвертого этапа работ по контракту.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
СПИСОК ЛИТЕРАТУРЫ
1. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ. М.: МЦНМО, 2. Николенко С. И., Тулупьев А. Л. Самообучающиеся системы. М.: МЦНМО, 2009.3. Поликарпова Н. И., Шалыто А. А. Автоматное программирование. СПб: Питер, 4. Царев Ф. Н. Метод построения управляющих конечных автоматов на основе // Информационно-управляющие системы. 2010. № 5, с. 31 – 36.
5. Хопкрофт Дж., Мотвани Р., Ульман Дж. Введение в теорию автоматов, языков и вычислений. М.: Вильямс, 2002.
6. Amazon Electronic Cloud Computing. http://aws.amazon.com/ec2/.
7. Biere A. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1. 2010. FMV Reports Series, Institute for Formal Models and Verification.
Johannes Kepler University. Altenbergerstr. 69, 4040 Linz, Austria.
8. Bouchard C. Boolean Expression Solver. http://sourceforge.net/projects/bool-exprsolve/.
9. Marques-Silva J., Lynce I., Malik S. Conict-Driven Clause Learning SAT Solvers // Handbook of Satisability Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh (Eds.). IOS Press, 2009.
10. CryptoMiniSat SAT-solver. http://www.msoos.org/cryptominisat2.
11. Davis M., Logemann G., Loveland D. A machine program for theorem-proving //Commun. ACM. 1962. 7, pp. 394-397. http://doi.acm.org/10.1145/368273.368557.
12. Een N., Srensson N. An extensible SAT-solver. Chalmers University of Technology.
Sweden, 2003. http://minisat.se/downloads/MiniSat.pdf.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для 13. Presentation of SAT-Race results at the SAT'10 conference http://baldur.iti.uka.de/satrace-2010/downloads/SAT-Race-2010-Presentation.pdf.
14. Rabiner L. A tutorial on hidden Markov models and selected applications in speech recognition //Proceedings of the IEEE. 1989. № 2, pp.257–286.
15. Roussel O. Description of ppfolio, 2011. http://www.cril.univ-artois.fr/roussel/ppfolio/solver1.pdf.
16. SAT Challenge 2012. http://baldur.iti.kit.edu/SAT-Challenge-2012/results.html.
17. Satisfiability suggested format DIMACS. http://www.domagojbabic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf.
18. The international SAT Competitions web page. http://www.satcompetition.org/.
19. The MiniSAT page. http://minisat.se/MiniSat.html.
20. zChaff SAT-solver. http://www.princeton.edu/~chaff/zchaff.html.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
ПРИЛОЖЕНИЕ А. КОПИЯ СОПРОВОДИТЕЛЬНОГО ПИСЬМА ЗАЯВКИ НА
РЕГИСТРАЦИЮ ПРОГРАММЫ ДЛЯ ЭВМ
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы дляПРИЛОЖЕНИЕ Б. ПРОТОКОЛЫ ВЫЧИСЛИТЕЛЬНЫХ ЭКСПЕРИМЕНТОВ
Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 250.Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 750.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 1000.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 1250.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 1500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 1750.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 2000.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 2250.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 5; суммарная длина сценариев работы – 2500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 250.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 750.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 1000.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 1250.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 1500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 1750.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 2000.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 2250.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 10; суммарная длина сценариев работы – 2500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 15; суммарная длина сценариев работы – 500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 15; суммарная длина сценариев работы –750.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 15; суммарная длина сценариев работы –1000.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 15; суммарная длина сценариев работы –1250.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 15; суммарная длина сценариев работы –1500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 15; суммарная длина сценариев работы –1750.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 15; суммарная длина сценариев работы –2000.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 15; суммарная длина сценариев работы –2250.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 15; суммарная длина сценариев работы –2500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 20; суммарная длина сценариев работы –750.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 20; суммарная длина сценариев работы –1000.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 20; суммарная длина сценариев работы –1250.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 20; суммарная длина сценариев работы –1500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 20; суммарная длина сценариев работы –1750.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 20; суммарная длина сценариев работы –2000.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 20; суммарная длина сценариев работы –2250.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Параметры экспериментов: число состояний искомого автомата – 20; суммарная длина сценариев работы –2500.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для
ПРИЛОЖЕНИЕ В. КОПИЯ СПРАВКИ И ТЕКСТ СТАТЬИ
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы дляМЕТОД ПОСТРОЕНИЯ УПРАВЛЯЮЩИХ АВТОМАТОВ НА ОСНОВЕ
МУРАВЬИНЫХ АЛГОРИТМОВ
Предлагается метод построения управляющих конечных автоматов по выбранной функции приспособленности, основанный на применении муравьиных алгоритмов. Проводится его апробация на задаче об «Умном муравье». Показано, что метод обладает большей производительностью по сравнению с традиционным подходом к построению управляющих автоматов на основе генетических алгоритмов. Предлагаемый метод не требует реализации таких нетривиальных операторов как, например, скрещивание или мутация.Ключевые слова: конечные автоматы, муравьиные алгоритмы.
В последние годы для решения разнообразных задач все чаще применяется автоматное программирование [1]. В рамках этого подхода поведение программ описывается с помощью детерминированных конечных автоматов. При этом часто эвристическое построение автоматов затруднительно, поэтому для этой цели применяются различные эволюционные алгоритмы, такие как генетические алгоритмы [2–5] и эволюционные стратегии [2, 6].
При построении автоматов с помощью эволюционных алгоритмов вводится функция, называемая функцией приспособленности, отражающая то, насколько автомат близок к решению задачи. Таким образом, построение автомата для той или иной задачи сводится к построению автомата с наибольшим или наименьшим значением функции приспособленности. Отдельно отметим, что введение функции приспособленности не предполагает наличие эталонного автомата. Примерами задач, для которых можно найти решение, представленное управляющим автоматом, с помощью эволюционных алгоритмов, являются:
задача об «Умном муравье» [1, 3, 7];
задача о завоевании ресурсов [2];
задача о построении автомата на основе тестовых примеров [3, 8].
В начале работы эволюционный алгоритм генерирует некую начальную популяцию особей (в данном случае, конечных автоматов). Обычно, особи начальной популяции генерируются случайным образом. Далее, пока не будет выполнено условие останова, выполняются операции мутации, скрещивания и селекции. Операции мутации и скрещивания по некоторым правилам изменяют особи в текущей популяции. Операция селекции определяет, какие особи перейдут в следующую популяцию.
При построении конечных автоматов с помощью эволюционных алгоритмов требуется разрабатывать операции мутации и скрещивания. В настоящей работе предлагается новый метод построения управляющих автоматов, основанный на муравьином алгоритме [9], не требующий реализации обозначенных операций.
Вопрос сходимости муравьиных алгоритмов изучен на данный момент сравнительно слабо. Доказательство сходимости некоторых классов муравьиных алгоритмов можно найти в [10]. Вопрос о сходимости других типов муравьиных алгоритмов остается на данный момент открытым. Сходимость предложенного алгоритма построения автоматов в настоящей работе не изучается.
Муравьиные алгоритмы – группа алгоритмов оптимизации на графах, принцип работы которых основан на поведении муравьев, ищущих путь от муравейника до источника пищи. Примером задачи, которая может быть решена с помощью муравьиного алгоритма, является задача о коммивояжере [11].
В муравьиных алгоритмах решения строятся набором агентов-муравьев, использующих при выборе пути в графе некоторую стохастическую стратегию. Решения могут быть представлены как путями в графе, так и отдельными его вершинами. Каждому ребру графа (u, v) (u и v – вершины графа) сопоставлено некоторое действительное число u v, называемое значением феромона, и (необязательно) некоторое эвристическое расстояние. Значения феромона модифицируuv Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для ются муравьями в процессе поиска, в то время как эвристические расстояния задаются перед началом работы алгоритма и далее не изменяются.
Можно выделить три основных этапа работы муравьиного алгоритма, которые повторяются, пока не будет найдено допустимое решение или пока не выполнится условие останова. На первом этапе, назовем его ConstructSolutions, каждый муравей совершает переходы по ребрам графа, запоминая свой путь – последовательность ребер. Находясь в определенной вершине, каждый муравей определяет следующее ребро, исходя из эвристических расстояний и значений феромона на ребрах, инцидентных данной вершине. Определив ребро, муравей добавляет его к своему пути и переходит по этому ребру к следующей вершине.
На втором этапе – UpdatePheromones – значения феромона на всех ребрах графа изменяются. Значение феромона на ребре может увеличиться, если по этому ребру прошел муравей, или уменьшиться вследствие испарения. При испарении значения феромона на всех ребрах графа изменяются в заданное число раз. На третьем (необязательном) этапе – DaemonActions – применяется некоторая локальная оптимизация или другие действия, которые не могут быть выполнены отдельными муравьями.
Будем называть управляющим детерминированный конечный автомат (ДКА), на каждом переходе которого записаны событие и последовательность выходных воздействий. События поступают на вход автомата из внешней среды. При поступлении события автомат переходит в новое состояние и передает выходные воздействия объекту управления. Пример управляющего конечного автомата приведен на рис. 1.
Для данного автомата множество входных событий равно {F, N}, а множество выходных воздействий – {z1, z2}.
Стартовое состояние автомата на рис. 1 и на всех других рисунках в данной работе отмечено жирной линией.
Предлагаемый метод построения управляющих автоматов на основе муравьиных алгоритмов Рассмотрим задачу о построении управляющего конечного автомата [1] при фиксированном множестве входных событий, выходных воздействий и введенной функции приспособленности. Пусть задано число состояний N, множество входных событий Events и множество выходных воздействий Actions автомата. Задача состоит в поиске автомата с наибольшим значением функции приспособленности.
Рассмотрим представление конечного автомата в виде графа переходов. При этом подходе состояния автомата соответствуют вершинам графа, а переходы – его дугам. Рассмотрим множество всех автоматов с параметрами (N, Events, Actions). Любой автомат из выбранного множества как граф является подграфом полного недетерминированного конечного автомата (НКА) с теми же параметрами. Под полным НКА понимается автомат, в котором из каждого из N состояний по каждому входному событию из Events существует переход в каждое состояние с каждым выходным воздействием из Actions. Пример такого автомата с двумя состояниями приведен на рис. 2.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Задача оптимизации ДКА для муравьиного алгоритма может быть сформулирована следующим образом. Задано множество входных событий Events, множество выходных воздействий Actions и число состояний N. Также задана функция приспособленности, определенная на множестве всех ДКА с указанными параметрами, сопоставляющая автомату действительное число. На полном НКА с теми же параметрами требуется найти такой путь, что ДКА, составленный из ребер и вершин найденного пути, имеет наибольшую функцию приспособленности.
В начале работы алгоритма всем ребрам полного НКА приписывается некоторый одинаковый ненулевой вес – значение феромона в терминах муравьиных алгоритмов. В каждую вершину полного НКА помещается по муравью. Каждый муравей выбирает переходы из своего состояния по каждому входному символу, исходя из значений феромона на переходах. Выбор производится с помощью метода «рулетки» [12].
Заметим, что в отличие от классического муравьиного алгоритма, описанного в разделе «Муравьиные алгоритмы», каждый муравей строит переходы только из своего состояния, не перемещаясь в другие состояния (вершины).
По выбранным муравьями состояниям и переходам строится ДКА. Далее для ДКА вычисляется выбранная функция приспособленности. При этом запоминаются переходы, которые совершал автомат. К весам посещенных при вычислении функции приспособленности переходов НКА добавляются дополнительные веса, пропорциональные вычисленному значению. Отметим, что веса тех переходов, которые не были посещены при вычислении функции приспособленности, не изменяются, а сами переходы удаляются из ДКА. Также из ДКА удаляются непосещенные состояния.
На следующем этапе со всех ребер НКА «испаряется» феромон – веса всех ребер уменьшаются в одинаковое число раз.
Наконец, проверяются условия сходимости (достижения требуемого значения функции приспособленности) и стагнации. Под стагнацией понимается ситуация, при которой значение функции приспособленности лучшего автомата не увеличивается в течение некоторого фиксированного промежутка времени (числа шагов алгоритма). В таком случае алгоритм перезапускается. При достижении требуемого значения функции приспособленности алгоритм прекращает свою работу, выдавая лучший из построенных автоматов.
В рамках экспериментального исследования предлагаемый метод был протестирован на задаче об «Умном муравье» [1, 4, 7]. Для вычислений использовался персональный компьютер с процессором Intel Core i7 2600 с тактовой частотой 3,4 ГГц.
Опишем задачу об «Умном муравье». Задано квадратное тороидальное поле размером 3232 клетки. На поле вдоль заданной ломаной расположено 89 «яблок» – единиц еды, причем яблоки располагаются не в каждой клетке этой ломаной. В начале пути муравей находится в левой верхней клетке поля и «смотрит» на восток. Поле, начальное расположение муравья и расположение еды на поле показано на рис. 3. Белые клетки пусты, в черных клетках расположена еда, а серым цветом отмечены клетки ломаной, не содержащие еды.
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для Муравей видит одну клетку перед собой: он может определить, есть еда в следующей клетке или нет. У муравья есть 200 ходов. На каждом ходу он может выполнить одно из трех действий: повернуть налево, повернуть направо, перейти на одну клетку вперед. При этом если клетка, в которую перешел муравей, содержит еду, муравей съедает эту еду.
В данной задаче рассматриваются два входных события – N (в следующей клетке нет еды) и F (в следующей клетке есть еда) – а также три выходных воздействия: L (повернуть налево), R (повернуть направо) и M (перейти на одну клетку вперед).
Задача состоит в том, чтобы построить систему управления муравьем, которая позволит ему съесть всю еду за минимальное число шагов. В работе [4] предлагается решение данной задачи путем построения конечного автомата, управляющего муравьем, с помощью генетического программирования. В указанной работе был найден автомат, имеющий семь состояний и позволяющий муравью съесть всю еду за отведенное число шагов. Число вычислений функции приспособленности потребовавшихся для построения такого автомата – порядка сотен миллионов ( 1 6 0 1 0 6 и 2 5 0 1 0 6 для двух разных экспериментов).
Традиционно функция приспособленности автомата, управляющего умным муравьем, имеет вид [1]:
где fsm – конечный автомат, n – число съеденных яблок, а numberOfSteps – номер хода, на котором было съедено последнее яблоко.
При использовании функции приспособленности (1) предлагаемый муравьиный алгоритм не нашел оптимального решения задачи об «Умном муравье». В настоящей работе авторами предлагается использовать модифицированную функцию приспособленности, учитывающую число состояний автомата:
где M – число состояний НКА, в котором проводится поиск с помощью муравьиного алгоритма, а N – число состояний ДКА, посещенных при вычислении функции приспособленности. При использовании выражения (2), оптимизация проводится одновременно по числу съеденных яблок, числу потребовавшихся для этого шагов, а также по числу использованных состояний автомата.
Авторами было проведено 15 экспериментов по построению оптимального автомата. В каждом эксперименте были использованы следующие параметры алгоритма:
скорость испарения феромона – 0,5;
стагнационный параметр – 106;
Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для число состояний полного НКА – 12.
В каждом из экспериментов был получен автомат, имеющий семь состояний, который съедает всю еду за 189 ходов. Минимальное число вычислений функции приспособленности, потребовавшееся для построения оптимального автомата – 1, 6 5 1 0 6, максимальное – 6 0,1 6 1 0 6, среднее значение – 2 6, 4 9 1 0 6 (стандартное отклонение – 1 7, 4 5 1 0 6 ). При этом среднее время построения оптимального автомата составило примерно 32 мин. Диаграмма переходов одного из построенных автоматов приведена на рис. 4.
При этом отметим, что для построения такого автомата с помощью генетического программирования в работе [4] потребовалось в среднем 2 2 0 1 0 6 вычислений функции приспособленности. Таким образом, с помощью предложенного алгоритма удалось найти решение задачи об «Умном муравье» в 8,3 раза быстрее, чем при использовании генетического алгоритма.
Разработан метод построения управляющих конечных автоматов, основанный на муравьиных алгоритмах. Разработано программное средство на языке Java, реализующее предлагаемый метод. Метод был протестирован на задаче об «Умном муравье». При использовании модифицированной функции приспособленности, учитывающей число состояний автомата, удалось найти решение этой задачи в 8,3 раза быстрее, чем с помощью генетического алгоритма.
Преимущество предлагаемого подхода перед генетическим алгоритмом также состоит в том, что для решения каждой конкретной задачи не требуется определять функции мутации и скрещивания, что обычно является нетривиальной задачей.
Исследование поддержано в рамках Федеральной целевой программы «научные и научно-педагогические кадры инновационной России на 2009-2013 годы».
1. Поликарпова Н. И., Шалыто А. А. Автоматное программирование. – СПб: Питер, 2009. – 176 с.
2. Spears W. M., Gordon D. F. Evolving finite-state machine strategies for protecting resources // Proceedings of the International Symposium of Methodologies for Intelligent Systems 2000. ACM Special Interest Group on Artificial Intelligence. – SpringerVerlag, 2000. – P. 166–175.
3. Царев Ф. Н. Метод построения автоматов управления системами со сложным поведением на основе тестов с помощью генетического программирования // Материалы международной научной конференции «Компьютерные науки и информационные технологии». – Саратов: СГУ, 2009. – С. 216–219.
4. Царев Ф. Н., Шалыто А. А. Применение генетического программирования для генерации автомата в задаче об «Умном муравье» // Сборник трудов IV-ой Международной научно-практической конференции «Интегрированные модели и мягкие вычисления в искусственном интеллекте». – М.: ФИЗМАТЛИТ, 2007. – Т. 2. – С. 590–597.
5. Александров А. В., Казаков С. В., Сергушичев А. А., Царев Ф. Н., Шалыто А. А. Генерация конечных автоматов для Разработка метода машинного обучения на основе алгоритмов решения задачи о выполнимости булевой формулы для управления моделью беспилотного самолета. / Научно-технический вестник Санкт-Петербургского университета информационных технологий, механики и оптики, 2011, № 2 (72). С. 3–11.
6. Lucas S. M. Evolving finite state transducers: Some initial explorations. Genetic Programming // Lecture Notes in Computer Science. – Berlin: Springer, Heidelberg, 2003. – V. 2610. – P. 241–257.
7. Лобанов П. Г. Использование генетических алгоритмов для генерации конечных автоматов. Дисс. канд. тех. наук:
05.13.11. – СПбГУ ИТМО, 2008. – 114 с.
8. Егоров К. В., Царев Ф. Н. Совместное применение генетического программирования и верификации моделей для построения автоматов управления системами со сложным поведением // Сборник докладов конференции молодых ученых и специалистов «Информационные технологии и системы». – М.: ИППИ РАН, 2009. – С. 77–82.
9. Dorigo M. Optimization, Learning and Natural Algorithms // Ph. D. thesis. – Politecnico di Milano. Italy, 1992. – 140 p.
10. Dorigo M., Sttzle T. Ant Colony Optimization. – MIT Press, 2004. – 305 p.
11. Dorigo M., Gambardella L.M. Ant Colony System: A Cooperative Learning Approach to the Traveling Salesman Problem // IEEE Transactions on Evolutionary Computation. – 1997. – V. 1. – № 1. – P. 53–66.
12. Baker J.E. Reducing Bias and Inefficiency in the Selection Algorithm / In Proceedings of the Second International Conference on Genetic Algorithms and their Application, Hillsdale, New Jersey, USA: Lawrence Erlbaum Associates, 1987. P. 14–21.
«