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

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

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

Булевы уравнения и проблема 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)