Алгоритмы решения проблемы булевой выполнимости (SAT) в применении к комбинаторным задачам

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