SAT-решатели применили к криптоанализу алгоритмов

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

Задачи криптографического анализа можно свести к SAT-формулировкам и решить через хорошо изученный математический аппарат. Алгоритмы эффективно распараллеливаются на вычислительных кластерах, что ускоряет поиск криптографических свойств анализируемых алгоритмов.