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

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

Версия 08:21, 29 октября 2010 (править) Dj (Обсуждение | вклад) (→Булевы уравнения и проблема SAT) ← К предыдущему изменению		Версия 08:22, 29 октября 2010 (править) (отменить) Dj (Обсуждение | вклад) (→Содержание курса) К следующему изменению →
Строка 16:		Строка 16:
	== Содержание курса ==		== Содержание курса ==
-	Лекции, 6 семестр	+	В результате изучения дисциплины студент должен:
-	=== Введение ===	+	* '''знать''' теорию булевых алгебр и булевых функций, основные методы решения задачи выполнимости (SAT).
-	1.1. Введение. Задача распознавания образов с прецедентной информацией (напоминание постановки, введение терминологии, обозначений). Направления исследований в теории распознавания: синтез алгоритмов, оценка надёжности обучения, анализ конфигураций точек в признаковых пространствах.	+	* '''уметь''' применять методы решений булевых уравнений к задачам синтеза управляющих систем, писать программы решения задач выполнимости конъюнктивных нормальных форм (КНФ) на основных языках программирования, применять методы упрощения КНФ.
-	1.2. Алгебраический подход к проблеме распознавания.	+	* '''владеть''' навыками решения булевых уравнений различных типов, навыками программирования современных SAT-солверов и алгоритмов рекурсивного перебора пространства поиска.
-	1.3. Пример анализа конфигураций точек в признаковых пространствах: получение критерия разделимости точек.	+
-	=== Алгоритмы вычисления оценок (АВО), алгебраические замыкания ===	+
-	2.1. Модель АВО (введение, основные обозначения, примеры, общие принципы).	+
-	2.2. Линейное и алгебраическое замыкание модели алгоритмов распознавания.	+
-	2.3. Техника представления алгоритмов из линейного замыкания АВО.	+
-	2.4. Функция близости (определение, примеры, общие принципы). Сведение к задачам с определённой функцией близости.	+
-	=== Корректность, операторы разметки ===	+
-	3.1. Операторы разметки. Матрицы оценок операторов. Теорема о реализации любых матриц (для любой матрицы из описанного класса существует соответствующая задача распознавания).	+
-	3.2. Корректность (определение). Критерий корректности (теорема Ю.И. Журавлёва).	+
-	3.3. Оценка степени корректного алгоритма.	+
-	3.4. Построение корректных алгоритмов распознавания (метод Ю.И. Журавлёва – И.В. Исаева).	+
-	=== Метрики алгебраических замыканий модели АВО ===	+
-	4.1. Метрики алгебраических замыканий, метрические критерии корректности.	+
-	4.2. Обзор (без доказательства) некоторых результатов теории жёсткой интерполяции.	+
-	4.3. Анализ некоторых классов точечных конфигураций (включая задания для самостоятельной работы).	+
-	=== Решающие правила, квазикорректность ===	+
-	5.1. Решающие правила.	+
-	5.2. Критерии квазикорректности (корректности относительно семейства решающих правил). Обзор (без доказательств) некоторых современных результатов.	+
-	5.3. Пополнение стандартной алгебры над АВО.	+
-	=== Логические алгоритмы распознавания ===	+
-	6.1. Логические алгоритмы распознавания (напоминания, краткий обзор, основные определения и обозначения).	+
-	6.2. Алгоритмы, основанные на синтезе ДНФ. Задача синтеза ДНФ по перечню нулевых наборов (обзор некоторых методов). Формула С.В. Яблонского. Методы Ю.И. Журавлёва, А.Ю. Когана.	+
-	=== Синтез ДНФ по перечню нулевых наборов ===	+
-	7.1. Тестовый подход к задаче ДНФ-реализации. Оценка сложности. Построение тупиковых ДНФ. Построение ДНФ специального вида. Построение явных ДНФ-формул.	+
-	7.2. Построение ДНФ последовательным умножением. Умножение ДНФ. Обобщение метода С.В. Яблонского. Эффективная реализация метода Нельсона.	+
-	7.3. ДНФ-реализация функций k-значной логики. Различные определения ДНФ в k-значном случае. Кодировки.	+
	== Литература ==		== Литература ==

---

Версия 08:22, 29 октября 2010

Содержание 1 Булевы уравнения и проблема SAT 2 Аннотация 3 Содержание курса 4 Литература

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

• Обязательный курс для студентов каф. ММП 3 курса, читается в 6-м семестре.
• Лекции – 32 часа, семинаров нет.
• Экзамен.
• За курс отвечает кафедра Математических методов прогнозирования.
• Авторы программы: академик РАН Ю. И. Журавлёв, доцент А. Г. Дьяконов.
• Лектор 2007/08 уч. года: доцент А.Г. Дьяконов.

Аннотация

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

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

Содержание курса

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

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

Литература

1. Дьяконов А.Г. Алгебра над алгоритмами вычисления оценок: Учебное пособие.– М.: Издательский отдел ф-та ВМиК МГУ им. М.В. Ломоносова, 2006. – 72с. (ISBN 5-89407-252-2)
2. Журавлёв Ю.И. Избранные научные труды. – М.: «Магистр», 1998.– 420с.
3. Черников С.Н. Линейные неравенства. М. Наука. 1968. 488 с.
4. Дискретная математика и математические вопросы кибернетики / Под ред. С.В. Яблонского и О.Б. Лупанова. – М.: Наука, 1974. – 312с.
5. Дюкова Е.В. Дискретные (логические) процедуры распознавания: принципы конструирования, сложность реализации и основные модели / Учебное пособие для студентов математических факультетов педвузов. – М.: Прометей, 2003. – С. 29. (ISBN 5-70420-1092-9)