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