КАРТОЧКА ПРОЕКТА ФУНДАМЕНТАЛЬНЫХ И ПОИСКОВЫХ НАУЧНЫХ ИССЛЕДОВАНИЙ,
ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ

Информация подготовлена на основании данных из Информационно-аналитической системы РНФ, содержательная часть представлена в авторской редакции. Все права принадлежат авторам, использование или перепечатка материалов допустима только с предварительного согласия авторов.

 

ОБЩИЕ СВЕДЕНИЯ

---

Номер проекта 22-21-00834

НазваниеРазработка эвристик для повышения эффективности современных алгоритмов решения проблемы максимальной выполнимости (MaxSAT)

Руководитель Кочемазов Степан Евгеньевич,

Организация финансирования, регион федеральное государственное бюджетное учреждение науки Институт динамики систем и теории управления имени В.М. Матросова Сибирского отделения Российской академии наук , Иркутская обл

Конкурс №64 - Конкурс 2021 года «Проведение фундаментальных научных исследований и поисковых научных исследований малыми отдельными научными группами»

Область знания, основной код классификатора 01 - Математика, информатика и науки о системах; 01-114 - Дискретная математика и математическая кибернетика

Ключевые слова проблема булевой выполнимости, проблема максимальной выполнимости, эвристики, решатели

Код ГРНТИ27.41.41

---

 

ИНФОРМАЦИЯ ИЗ ЗАЯВКИ

---

Аннотация
Современные алгоритмы решения проблемы булевой выполнимости (SAT) считаются одной из историй успеха в современной Computer Science. Если 20 лет назад они были применимы лишь к небольшим задачам с сотнями переменных и дизъюнктов, то сегодня SAT-решатели успешно справляются с проблемами, кодировка которых включает сотни тысяч переменных и миллионы дизъюнктов. Это позволило многим смежным областям, в которых постановка задачи позволяет естественным образом выразить её через двоичную логику, в свою очередь пережить активную фазу развития. Одна из таких областей связана с т.н. проблемой максимальной выполнимости (MaxSAT). Более конкретно, MaxSAT представляет собой оптимизационное обобщение SAT. Интерес к MaxSAT обуславливается тем, что большинство практических задач значительно более естественным образом формулируются именно в оптимизационном контексте, например, "найти кратчайший путь между двумя точками", чем в качестве задачи поиска ("найти путь между двумя точками длиной не более K или доказать, что он не существует"). При этом, в отличие от эвристических и жадных алгоритмов, современные MaxSAT-решатели позволяют найти точное решение для сформулированной задачи и доказать, что оно является точным. Алгоритмы решения MaxSAT как правило используют сложные итеративные схемы, на каждом этапе которых промежуточная задача кодируется в SAT, и поиск её решения осуществляется при помощи SAT-решателя (обычно на основе Conflict-Driven Clause Learning(CDCL) - концепции). В рамках настоящего проекта предполагается исследовать и улучшить эффективность CDCL-решателей, применяемых в контексте MaxSAT-алгоритмов путем разработки специализированных эвристик для них. Актуальность данного направления исследований обуславливается тем, что большинство современных алгоритмов решения MaxSAT опираются на применение CDCL-решателей MiniSAT и Glucose разработанных более, чем 8 лет назад. Несмотря на значительный прогресс именно в CDCL-решателях SAT, который можно наблюдать по результатам ежегодных соревнований соответствующих алгоритмов за эти 8 лет, результаты недавних исследований показывают, что в контексте решения MaxSAT наработки в области CDCL за недавние годы не дают никакого преимущества по сравнению с проверенными временем алгоритмами. В рамках проекта планируется разработать на основе современных CDCL-эвристик в MaxSAT-контексте новые эвристики специальным образом спроектированные для того, чтобы увеличивать эффективность применения SAT-решателей внутри MaxSAT-алгоритмов, а также модифицировать MaxSAT-алгоритмы таким образом, чтобы максимально эффективно задействовать особенности современных CDCL-алгоритмов. Именно эти новые эвристики и алгоритмы, а также полученные с их использованием результаты, и составят основную научную новизну проекта.

---

 

ОТЧЁТНЫЕ МАТЕРИАЛЫ

---