Г. Ярославцев (АФТУ)
Построение SAT-солверов и их использование

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

В докладе мы рассмотрим теоретические основы устройства SAT-солверов и обсудим некоторые детали их реализации. Мы проследим процесс развития алгоритмов и идей, используемых в современных солверах, в порядке их появления.

Доклад основан на лекции, прочитанной Даниэлем ле Берре на научной школе "Verification Technology, Systems & Applications 2009".