Булевы уравнения и проблема SAT

Материал из MachineLearning.

Содержание 1 Аннотация 2 Место дисциплины в учебном плане 3 Содержание дисциплины 4 Перечень разделов курса 5 Литература

Аннотация

Данный курс является обязательным односеместровым курсом для студентов II года обучения магистратуры. Курс читается в I семестре. Длительность курса 32 часа. В конце семестра сдается экзамен. Отвечает за курс кафедра ММП.

Авторы программы: Дьяконов Александр Геннадьевич и Гуров Сергей Исаевич.

Место дисциплины в учебном плане

В результате изучения дисциплины студент должен:

• знать теорию булевых алгебр и булевых функций, основные методы решения задачи выполнимости (SAT).
• уметь применять методы решений булевых уравнений к задачам синтеза управляющих систем, писать программы решения задач выполнимости конъюнктивных нормальных форм (КНФ) на основных языках программирования, применять методы упрощения КНФ.
• владеть навыками решения булевых уравнений различных типов, навыками программирования современных SAT-солверов и алгоритмов рекурсивного перебора пространства поиска.

Содержание дисциплины

Первую часть курса «Булевы уравнения и проблема SAT» составляет раздел, посвящённый теории и методам решения булевых уравнений. Рассматривается теория булевых алгебр, функций и уравнений и бесконечных и конечных булевых алгебрах. Вводится классификация булевых уравнений по типу задания алгебры (булева решётка, булево кольцо), её реализации (бесконечная – алгебра множеств, конечная алгебра n-мерных двоичных векторов, алгебра логических функций Линденбаума-Тарского), типу задачи (распознавание разрешимости уравнения, нахождения всех или по крайней мере одного решения), виду представления решения (таблицs истинности, представляющие формулы, представляющие соотношения), типу неизвестного (алгебраические – с заданием в виде ДНФ, КНФ или АНФ, функциональные). Обосновываются алгоритмы решения булевых уравнений различных типов. Водятся понятия производной и интеграла булевой функции, которые затем применяются для решения функциональных булевых уравнений. Рассматриваются вопросы синтеза управляющих систем, сводящиеся с решению булевых уравнений и их систем.

Во второй части курса рассматривается проблема выполнимости (SAT) на примере выполнимости конъюнктивной нормальной формы (КНФ). Изучаются два типа алгоритмов: неполные (которые не перебирают всё пространство булевых наборов) и полные. Вводится классификация неполных алгоритмов как алгоритмов оптимизации чёрного ящика (метаэвристик), рассматриваются приложения таких алгоритмов в различных областях современной математики. Изучается основной полный алгоритм решения задачи SAT – DPLL, а также его обобщения и модификации. Рассматривается задача полного рекурсивного перебора пространства поиска, методы её решения, упрощения, а также приложения задачи. На примере показываются методы программирования алгоритмов для решения задачи выполнимости: SAT-солверов, методы оценки их эффективности, примеры работы. Часть курса посвящена задаче эффективного умножения скобок КНФ (при её упрощении или преобразовании в дизъюнктивную нормальную форму – ДНФ). Рассмотрены методы прямого перемножения, а также методы, основанные на синтезе ДНФ с малым числом нулей. Описаны приложения рассмотренных методов, их обобщения и модификации.

Перечень разделов курса

Введение. Цели и задачи курса, его структура. Методы контроля знаний. Организационные вопросы.

Булева алгебра. Аксиоматическое задание. Алгебраические системы. Алгебры множеств. Изоморфизмы булевых алгебр. Теорема Стоуна.

Алгебраические решётки. Общие понятия. Дистрибутивные решётки. Булевы алгебры как решётки. Булевы кольца и структуры. Булевы многочлены и уравнения (общий случай). Канонические формы булевых многочленов: ДНФ, КНФ, АНФ. Уравнения в булевых алгебрах.

Алгебра булевых функций. Общая теория. Уравнения в алгебре булевых функций (БУ). Типы задач решения БУ: распознавание разрешимости уравнения, нахождения всех или по крайней мере одного решения. Виды представления решений (таблицы истинности, представляющие формулы, представляющие соотношения). Типы БУ: алгебраические, функциональные.

Алгоритмы решений БУ. Обоснования алгоритмов решений алгебраических БУ. Примеры. Решение функциональных БУ. Дополнительные вопросы теории булевых функций. Теория дифференцирования и интегрирования булевых функций. Обоснования алгоритмов решений функциональных БУ. Примеры.

Проектирование управляющих систем с использованием теории решений БУ.

Проблема выполнимости (ВЫП или SAT). Постановка проблемы. Основные приложения: функциональная эквивалентность программ, функциональная эквивалентность схем. Современные SAT-солверы, методы их тестирования. Классификация алгоритмов решения задачи выполнимости.

Неполные методы решения задачи выполнимости. Задача поиска максимального числа выполненных конъюнкций как задача глобальной оптимизации. Основные методы решения задачи глобальной оптимизации, метаэвристики: полный перебор, направленный поиск, генетические алгоритмы. Приложения.

Полные методы решения задачи выполнимости. Процедура DPLL – обобщение процедуры Дэвиса (Davis) и Путнэма (Putnam). Дерево пространства поиска, рекурсивные процедуры обработки дерева. Конфликты (появления невыполняющихся клауз). Необходимые приписания: юниты, чистые литералы. Пример эффективной обработки дерева пространства поиска, приложение в программировании логических игр.

Расширения DPLL. Граф конфликтных клауз. Релевантное обучение (улучшение механизма сохранение клауз). Нехронологический перебор. Перезапуски. Эвристики расщепления.

Программирование SAT-солвера. Эффективность солвера. Предобработка конъюнктивной нормальной формы (КНФ). Хранение данных. Формат DIMACS. Пример работы DPLL-алгоритма.

Задача нельсоновского умножения. Задача эффективного перемножения скобок КНФ, приложения (в реализации булевых функций и анализе данных). Основные подходы к решению задачи: прямое перемножение, синтез дизъюнктивных нормальных форм (ДНФ) с малым числом нулей.

Прямое нельсоновское умножение. Кодирование конъюнкций. Умножение по формуле С.В. Яблонского.

Замена скобок КНФ эквивалентной ДНФ. Тестовый подход. Метод разложения по переменной. Обобщения на k-значный случай.

Литература

1. Близнюк В.Д., Холодный М.Ф. Декомпозиция булевых функций с применением аппарата булевых производных // Автоматика и телемеханика, № 5, 1984. - С. 105-112.
2. Бохманн Д. Булевское дифференциальное исчисление. Обзор // Труды АН СССР, Техническая кибернетика, т. 15, № 5, 1977. - С. 68-75.
3. Бохманн Д., Постхоф Х. Двоичные динамические системы. - М.: Энергоатомиздат, 1986.
4. Гуров С.И. Упорядоченные множества и универсальная алгебра (вводный курс): Учебн. пособие. - М.: Издательский отдел ф-та ВМиК МГУ, 2004. - 104 с. (Электронная версия находится на сайте ф-та ВМиК МГУ www.cs.msu.ru > Учебная работа > Материалы по учебным курсам).
5. Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. – М.: Мир, 1982. – 416с.
6. Журавлев Ю.И., Коган А.Ю. Алгоритм построения дизъюнктивной нормальной формы, эквивалентной произведению левых частей булевых уравнений нельсоновского типа // Ж. вычисл. матем. и матем. физ. – 1986. Т. 26. № 8. – С. 1243–1249.
7. Журавлев Ю.И., Платоненко И.М. Об экономном умножении булевых уравнений // Ж. вычисл. матем. и матем. физ. – 1984. Т. 24. № 1. – С. 164–166.
8. Закревский А.Д. Логические уравнения. - Минск: Наука и техника, 1975. - 96 с.
9. Закревский А.Д., Поттосин Ю.В., Черемисинова Л.Д. Логические основы проектирования дискретных устройств. - М.: ФИЗМАТЛИТ, 2007. - 592 с. ISBN 978-5-9221-0811-9
10. Катериночкина Н.Н., Королёва З.Е., Мадатян Х.А., Платоненко И.М. Методы решения булевых уравнений. - М.: ВЦ РАН, 1988. - 22 с.
11. Левченков В.С. Булевы уравнения: Учебное пособие для студентов. - М.: Издательский отдел ф-та ВМиК МГУ, 1999. - 56 с.
12. Левченков В.С. Булевы уравнения в алгебре логики и теории множеств // Вестник Московского ун-та., № 15, Вычислительная математика и кибернетика, 1999, № 3. - С. 17-20.
13. Люггер Д.Ф. Искусственный интеллект: стратегии и методы решения сложных проблем. – М.: Издательский дом «Вильямс», 2005. – 864 с.
14. Маевский О.В. Логические уравнения. - М.: ИКИ АН СССР, 1978. - 23 с. Рук. депронирована в ВИНИТИ, № 1816-79М.
15. Пушальский Г.И., Новосельцева Е.Ю. Цифровые устройства. - СПб.: Политехника, 1996. - 582 с.
16. Шалыто А.А. Логическое управление. Методы аппаратной и программной реализации. - СПб.: Наука, 2000. , 780 c
17. D. Du, J. Gu, and P,M. Pardalos, editors. Satisfiability Problem: Theory and Applications, volume 35. American Mathematical Society, 1997.
18. J. Gu, P.W. Purdom, J. Franco, and B.W. Wah: Algorithms for the Satisfiability(SAT) Problem: A Survey. In Discrete Mathematics and Theoretical Computer Science: Satisflability (SAT) Problem, vol. 35, pages 19-152 (1997).
19. Sean Luke Essentials of Metaheuristics (A Set of Undergraduate Lecture Notes) // Online Version 0.6 http://cs.gmu.edu/~sean/book/metaheuristics/
20. Inês Lynce and João P. Marques-Silva An overview of backtrack search satisfiability algorithms Annals of Mathematics and Artificial Intelligence 37: 307–326, 2003.
21. Rudeanu, S. Boolean Functions and Equations, Amsterdam-London-New York: North-Holland Publ. Co. \& American Elsevier, 1974.
22. http://satlive.org/ – сайт, посвящённый проблеме выполнимости.
23. http://www.satcompetition.org/ – сайт чемпионатов по разработке SAT-солверов.
24. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ – вся информация о солвере MiniSat.