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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Булевы уравнения и проблема SAT)
Текущая версия (08:31, 29 октября 2010) (править) (отменить)
м (Перечень разделов курса)
 
(5 промежуточных версий не показаны.)
Строка 1: Строка 1:
-
== Булевы уравнения и проблема SAT ==
 
-
 
-
* Обязательный курс для студентов каф. [[ММП]] 3 курса, читается в 6-м семестре.
 
-
* Лекции – 32 часа, семинаров нет.
 
-
* Экзамен.
 
-
* За курс отвечает кафедра Математических методов прогнозирования.
 
-
* Авторы программы: академик РАН [[Журавлёв, Юрий Иванович|{{S|Ю. И. Журавлёв}}]], доцент [[Дьяконов, Александр Геннадиевич|{{S|А. Г. Дьяконов}}]].
 
-
* Лектор 2007/08 уч. года: доцент А.Г. Дьяконов.
 
-
 
== Аннотация ==
== Аннотация ==
Данный курс является обязательным односеместровым курсом для студентов II года обучения магистратуры.
Данный курс является обязательным односеместровым курсом для студентов II года обучения магистратуры.
Строка 15: Строка 6:
Авторы программы: [[Участник:Dj|Дьяконов Александр Геннадьевич]] и Гуров Сергей Исаевич.
Авторы программы: [[Участник:Dj|Дьяконов Александр Геннадьевич]] и Гуров Сергей Исаевич.
-
== Содержание курса ==
+
== Место дисциплины в учебном плане ==
-
Лекции, 6 семестр
+
В результате изучения дисциплины студент должен:
-
=== Введение ===
+
* '''знать''' теорию булевых алгебр и булевых функций, основные методы решения задачи выполнимости (SAT).
-
1.1. Введение. Задача распознавания образов с прецедентной информацией (напоминание постановки, введение терминологии, обозначений). Направления исследований в теории распознавания: синтез алгоритмов, оценка надёжности обучения, анализ конфигураций точек в признаковых пространствах.
+
* '''уметь''' применять методы решений булевых уравнений к задачам синтеза управляющих систем, писать программы решения задач выполнимости конъюнктивных нормальных форм (КНФ) на основных языках программирования, применять методы упрощения КНФ.
-
1.2. Алгебраический подход к проблеме распознавания.
+
* '''владеть''' навыками решения булевых уравнений различных типов, навыками программирования современных SAT-солверов и алгоритмов рекурсивного перебора пространства поиска.
-
1.3. Пример анализа конфигураций точек в признаковых пространствах: получение критерия разделимости точек.
+
 
-
=== Алгоритмы вычисления оценок (АВО), алгебраические замыкания ===
+
== Содержание дисциплины ==
-
2.1. Модель АВО (введение, основные обозначения, примеры, общие принципы).
+
Первую часть курса «Булевы уравнения и проблема SAT» составляет раздел, посвящённый теории и методам решения булевых уравнений. Рассматривается теория булевых алгебр, функций и уравнений и бесконечных и конечных булевых алгебрах. Вводится классификация булевых уравнений по типу задания алгебры (булева решётка, булево кольцо), её реализации (бесконечная – алгебра множеств, конечная алгебра n-мерных двоичных векторов, алгебра логических функций Линденбаума-Тарского), типу задачи (распознавание разрешимости уравнения, нахождения всех или по крайней мере одного решения), виду представления решения (таблицs истинности, представляющие формулы, представляющие соотношения), типу неизвестного (алгебраические – с заданием в виде ДНФ, КНФ или АНФ, функциональные). Обосновываются алгоритмы решения булевых уравнений различных типов. Водятся понятия производной и интеграла булевой функции, которые затем применяются для решения функциональных булевых уравнений. Рассматриваются вопросы синтеза управляющих систем, сводящиеся с решению булевых уравнений и их систем.
-
2.2. Линейное и алгебраическое замыкание модели алгоритмов распознавания.
+
 
-
2.3. Техника представления алгоритмов из линейного замыкания АВО.
+
Во второй части курса рассматривается проблема выполнимости (SAT) на примере выполнимости конъюнктивной нормальной формы (КНФ). Изучаются два типа алгоритмов: неполные (которые не перебирают всё пространство булевых наборов) и полные. Вводится классификация неполных алгоритмов как алгоритмов оптимизации чёрного ящика (метаэвристик), рассматриваются приложения таких алгоритмов в различных областях современной математики. Изучается основной полный алгоритм решения задачи SAT – DPLL, а также его обобщения и модификации. Рассматривается задача полного рекурсивного перебора пространства поиска, методы её решения, упрощения, а также приложения задачи. На примере показываются методы программирования алгоритмов для решения задачи выполнимости: SAT-солверов, методы оценки их эффективности, примеры работы. Часть курса посвящена задаче эффективного умножения скобок КНФ (при её упрощении или преобразовании в дизъюнктивную нормальную форму – ДНФ). Рассмотрены методы прямого перемножения, а также методы, основанные на синтезе ДНФ с малым числом нулей. Описаны приложения рассмотренных методов, их обобщения и модификации.
-
2.4. Функция близости (определение, примеры, общие принципы). Сведение к задачам с определённой функцией близости.
+
 
-
=== Корректность, операторы разметки ===
+
== Перечень разделов курса ==
-
3.1. Операторы разметки. Матрицы оценок операторов. Теорема о реализации любых матриц (для любой матрицы из описанного класса существует соответствующая задача распознавания).
+
'''Введение.''' Цели и задачи курса, его структура. Методы контроля знаний. Организационные вопросы.
-
3.2. Корректность (определение). Критерий корректности (теорема Ю.И. Журавлёва).
+
 
-
3.3. Оценка степени корректного алгоритма.
+
'''Булева алгебра.''' Аксиоматическое задание. Алгебраические системы. Алгебры множеств. Изоморфизмы булевых алгебр. Теорема Стоуна.
-
3.4. Построение корректных алгоритмов распознавания (метод Ю.И. Журавлёва – И.В. Исаева).
+
 
-
=== Метрики алгебраических замыканий модели АВО ===
+
'''Алгебраические решётки.''' Общие понятия. Дистрибутивные решётки. Булевы алгебры как решётки. Булевы кольца и структуры. Булевы многочлены и уравнения (общий случай). Канонические формы булевых многочленов: ДНФ, КНФ, АНФ. Уравнения в булевых алгебрах.
-
4.1. Метрики алгебраических замыканий, метрические критерии корректности.
+
 
-
4.2. Обзор (без доказательства) некоторых результатов теории жёсткой интерполяции.
+
'''Алгебра булевых функций. Общая теория.''' Уравнения в алгебре булевых функций (БУ). Типы задач решения БУ: распознавание разрешимости уравнения, нахождения всех или по крайней мере одного решения. Виды представления решений (таблицы истинности, представляющие формулы, представляющие соотношения). Типы БУ: алгебраические, функциональные.
-
4.3. Анализ некоторых классов точечных конфигураций (включая задания для самостоятельной работы).
+
 
-
=== Решающие правила, квазикорректность ===
+
'''Алгоритмы решений БУ.''' Обоснования алгоритмов решений алгебраических БУ. Примеры. Решение функциональных БУ. Дополнительные вопросы теории булевых функций. Теория дифференцирования и интегрирования булевых функций. Обоснования алгоритмов решений функциональных БУ. Примеры.
-
5.1. Решающие правила.
+
 
-
5.2. Критерии квазикорректности (корректности относительно семейства решающих правил). Обзор (без доказательств) некоторых современных результатов.
+
'''Проектирование управляющих систем с использованием теории решений БУ.'''
-
5.3. Пополнение стандартной алгебры над АВО.
+
 
-
=== Логические алгоритмы распознавания ===
+
'''Проблема выполнимости (ВЫП или SAT).''' Постановка проблемы. Основные приложения: функциональная эквивалентность программ, функциональная эквивалентность схем. Современные SAT-солверы, методы их тестирования. Классификация алгоритмов решения задачи выполнимости.
-
6.1. Логические алгоритмы распознавания (напоминания, краткий обзор, основные определения и обозначения).
+
 
-
6.2. Алгоритмы, основанные на синтезе ДНФ. Задача синтеза ДНФ по перечню нулевых наборов (обзор некоторых методов). Формула С.В. Яблонского. Методы Ю.И. Журавлёва, А.Ю. Когана.
+
'''Неполные методы решения задачи выполнимости.''' Задача поиска максимального числа выполненных конъюнкций как задача глобальной оптимизации. Основные методы решения задачи глобальной оптимизации, метаэвристики: полный перебор, направленный поиск, генетические алгоритмы. Приложения.
-
=== Синтез ДНФ по перечню нулевых наборов ===
+
 
-
7.1. Тестовый подход к задаче ДНФ-реализации. Оценка сложности. Построение тупиковых ДНФ. Построение ДНФ специального вида. Построение явных ДНФ-формул.
+
 
-
7.2. Построение ДНФ последовательным умножением. Умножение ДНФ. Обобщение метода С.В. Яблонского. Эффективная реализация метода Нельсона.
+
'''Полные методы решения задачи выполнимости.''' Процедура DPLL – обобщение процедуры Дэвиса (Davis) и Путнэма (Putnam). Дерево пространства поиска, рекурсивные процедуры обработки дерева. Конфликты (появления невыполняющихся клауз). Необходимые приписания: юниты, чистые литералы. Пример эффективной обработки дерева пространства поиска, приложение в программировании логических игр.
-
7.3. ДНФ-реализация функций k-значной логики. Различные определения ДНФ в k-значном случае. Кодировки.
+
 
 +
'''Расширения DPLL.''' Граф конфликтных клауз. Релевантное обучение (улучшение механизма сохранение клауз). Нехронологический перебор. Перезапуски. Эвристики расщепления.
 +
 
 +
'''Программирование SAT-солвера.''' Эффективность солвера. Предобработка конъюнктивной нормальной формы (КНФ). Хранение данных. Формат DIMACS. Пример работы DPLL-алгоритма.
 +
 
 +
'''Задача нельсоновского умножения.''' Задача эффективного перемножения скобок КНФ, приложения (в реализации булевых функций и анализе данных). Основные подходы к решению задачи: прямое перемножение, синтез дизъюнктивных нормальных форм (ДНФ) с малым числом нулей.
 +
 
 +
'''Прямое нельсоновское умножение.''' Кодирование конъюнкций. Умножение по формуле С.В. Яблонского.
 +
 
 +
'''Замена скобок КНФ эквивалентной ДНФ.''' Тестовый подход. Метод разложения по переменной. Обобщения на k-значный случай.
== Литература ==
== Литература ==
-
# Дьяконов А.Г. Алгебра над алгоритмами вычисления оценок: Учебное пособие.– М.: Издательский отдел ф-та ВМиК МГУ им. М.В. Ломоносова, 2006. – 72с. (ISBN 5-89407-252-2)
 
-
# Журавлёв Ю.И. Избранные научные труды. – М.: «Магистр», 1998.– 420с.
 
-
# Черников С.Н. Линейные неравенства. М. Наука. 1968. 488 с.
 
-
# Дискретная математика и математические вопросы кибернетики / Под ред. С.В. Яблонского и О.Б. Лупанова. – М.: Наука, 1974. – 312с.
 
-
# Дюкова Е.В. Дискретные (логические) процедуры распознавания: принципы конструирования, сложность реализации и основные модели / Учебное пособие для студентов математических факультетов педвузов. – М.: Прометей, 2003. – С. 29. (ISBN 5-70420-1092-9)
 
 +
# Близнюк В.Д., Холодный М.Ф. Декомпозиция булевых функций с применением аппарата булевых производных // Автоматика и телемеханика, № 5, 1984. - С. 105-112.
 +
# Бохманн Д. Булевское дифференциальное исчисление. Обзор // Труды АН СССР, Техническая кибернетика, т. 15, № 5, 1977. - С. 68-75.
 +
# Бохманн Д., Постхоф Х. Двоичные динамические системы. - М.: Энергоатомиздат, 1986.
 +
# Гуров С.И. Упорядоченные множества и универсальная алгебра (вводный курс): Учебн. пособие. - М.: Издательский отдел ф-та ВМиК МГУ, 2004. - 104 с. (Электронная версия находится на сайте ф-та ВМиК МГУ www.cs.msu.ru > Учебная работа > Материалы по учебным курсам).
 +
# Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. – М.: Мир, 1982. – 416с.
 +
# Журавлев Ю.И., Коган А.Ю. Алгоритм построения дизъюнктивной нормальной формы, эквивалентной произведению левых частей булевых уравнений нельсоновского типа // Ж. вычисл. матем. и матем. физ. – 1986. Т. 26. № 8. – С. 1243–1249.
 +
# Журавлев Ю.И., Платоненко И.М. Об экономном умножении булевых уравнений // Ж. вычисл. матем. и матем. физ. – 1984. Т. 24. № 1. – С. 164–166.
 +
# Закревский А.Д. Логические уравнения. - Минск: Наука и техника, 1975. - 96 с.
 +
# Закревский А.Д., Поттосин Ю.В., Черемисинова Л.Д. Логические основы проектирования дискретных устройств. - М.: ФИЗМАТЛИТ, 2007. - 592 с. ISBN 978-5-9221-0811-9
 +
# Катериночкина Н.Н., Королёва З.Е., Мадатян Х.А., Платоненко И.М. Методы решения булевых уравнений. - М.: ВЦ РАН, 1988. - 22 с.
 +
# Левченков В.С. Булевы уравнения: Учебное пособие для студентов. - М.: Издательский отдел ф-та ВМиК МГУ, 1999. - 56 с.
 +
# Левченков В.С. Булевы уравнения в алгебре логики и теории множеств // Вестник Московского ун-та., № 15, Вычислительная математика и кибернетика, 1999, № 3. - С. 17-20.
 +
# Люггер Д.Ф. Искусственный интеллект: стратегии и методы решения сложных проблем. – М.: Издательский дом «Вильямс», 2005. – 864 с.
 +
# Маевский О.В. Логические уравнения. - М.: ИКИ АН СССР, 1978. - 23 с. Рук. депронирована в ВИНИТИ, № 1816-79М.
 +
# Пушальский Г.И., Новосельцева Е.Ю. Цифровые устройства. - СПб.: Политехника, 1996. - 582 с.
 +
# Шалыто А.А. Логическое управление. Методы аппаратной и программной реализации. - СПб.: Наука, 2000. , 780 c
 +
# D. Du, J. Gu, and P,M. Pardalos, editors. Satisfiability Problem: Theory and Applications, volume 35. American Mathematical Society, 1997.
 +
# 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).
 +
# Sean Luke Essentials of Metaheuristics (A Set of Undergraduate Lecture Notes) // Online Version 0.6 http://cs.gmu.edu/~sean/book/metaheuristics/
 +
# 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.
 +
# Rudeanu, S. Boolean Functions and Equations, Amsterdam-London-New York: North-Holland Publ. Co. \& American Elsevier, 1974.
 +
# http://satlive.org/ – сайт, посвящённый проблеме выполнимости.
 +
# http://www.satcompetition.org/ – сайт чемпионатов по разработке SAT-солверов.
 +
# http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ – вся информация о солвере MiniSat.
[[Категория:Учебные курсы]]
[[Категория:Учебные курсы]]

Текущая версия

Содержание

Аннотация

Данный курс является обязательным односеместровым курсом для студентов 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.
Личные инструменты