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

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

Перейти к: навигация, поиск

Содержание

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