Задача булевой выполнимости (SAT) заключается в поиске набора значений переменных, при которых логическая формула принимает значение «истина». Для автоматизации этого процесса применяются специализированные программные средства — SAT-решатели.
Алгоритмы, лежащие в основе SAT-решателей, обладают высокой степенью распараллеливания. Это позволяет эффективно задействовать вычислительные кластеры для решения сложных задач.
В криптоанализе многие задачи сводятся к формату SAT. Такой подход дает возможность использовать развитый математический аппарат для доказательства или оценки криптографических свойств алгоритмов.
Ведущий аналитик компании «Актив» Марина Скоробогатова представила обзор методов, позволяющих применять SAT-решатели для анализа криптографических систем.
