• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Бинарная классификация как вспомогательный инструмент для решения SAT задач

ФИО студента: Мосин Василий Михайлович

Руководитель: Канович Макс Иосифович

Кампус/факультет: Факультет компьютерных наук

Программа: Науки о данных (Магистратура)

Год защиты: 2017

Проблема выполнимости булевых формул (англ. SAT – satisfiability problem) – классическая NP-полная задача, представляющая собой особый интерес как с научной, так и с практической точки зрения. В последнее время появляются статьи, посвященные применению машинного обучения в решении SAT задач. В данной работе предлагается использовать метод бинарной классификации в качестве вспомогательного инструмента при выполнении SAT-алгоритма DPLL для увеличения его производительности. Основная идея работы основывается на предположении о том, что если на каждом шаге ветвления DPLL алгоритма переменной ветвления присваивать значение, которое ведет к выполнимости исследуемой булевой формулы с наибольшей вероятностью, то время поиска решения должно сократиться. Для вычисления вероятностей выполнимости булевой формулы на каждой итерации работы DPLL алгоритма для двух различных значений переменной ветвления предлагается использовать метод бинарной классификации. В работе предварительно были обучены различные модели бинарных классификаторов, после чего наилучшая из них использовалась в алгоритме DPLL. Основным результатом, полученным в ходе исследования, является то, что применении бинарного классификатора при выборе значения переменной ветвления в DPLL алгоритме, предложенным в данной работе методом, действительно дает прирост производительности по времени. Однако, также было показано, что для различных критериев ветвления порог значения количества переменных в формуле, для которого применение классификатора имеет смысл, варьируется.

Выпускные квалификационные работы (ВКР) в НИУ ВШЭ выполняют все студенты в соответствии с университетским Положением и Правилами, определенными каждой образовательной программой.

Аннотации всех ВКР в обязательном порядке публикуются в свободном доступе на корпоративном портале НИУ ВШЭ.

Полный текст ВКР размещается в свободном доступе на портале НИУ ВШЭ только при наличии согласия студента – автора (правообладателя) работы либо, в случае выполнения работы коллективом студентов, при наличии согласия всех соавторов (правообладателей) работы. ВКР после размещения на портале НИУ ВШЭ приобретает статус электронной публикации.

ВКР являются объектами авторских прав, на их использование распространяются ограничения, предусмотренные законодательством Российской Федерации об интеллектуальной собственности.

В случае использования ВКР, в том числе путем цитирования, указание имени автора и источника заимствования обязательно.

Реестр дипломов НИУ ВШЭ