Аннотация

В ходе доклада мы рассмотрим задачу SAT, её сложность и практическую важность. Погрузимся в идеологию и методы работы SAT-решателей и изучим передовые алгоритмы для решения этой задачи. Также мы обсудим, как эти алгоритмы применяются в реальной жизни.

Структура доклада:

• Введение в SAT: примеры SAT-задачи, идеология SAT-решателей, поиск нескольких решений, сложность SAT, доказательство для UNSAT, теорема о полноте и корректности метода резолюции, пример использования метода резолюции;
• Алгоритмы решения SAT: DPP/DPLL, Conflict-Driven Clause Learning (CDCL), SAT Competitions;
• Приложения SAT: проблема Хадвигера-Нельсона (1950), Equivalence Checking, задачи верификации, другие интересные приложения и полезные ссылки.

****Доклад подготовлен совместно с коллективом лаборатории "Дискретной оптимизации и формальных методов" университета ИТМО (CT Lab). Данный коллектив активно публикуется на ведущих конференция (A, A). В 2019 ими был разработан SAT-солвер, который стал победителем SAT Race сразу в двух категориях.

Запись

https://youtu.be/s8jbd_R8fcA

Презентация

Александр Андреев - Алгоритмы решения SAT - теоретические и практические аспекты (2024-05-22).pdf