Подробное описание документа

Васютин Р. Р., Ключарев П. Г.
   Разработка эвристики расщепления SAT-решателя для задач криптоанализа = SAT-Solver Splitting Heuristic Development for Cryptanalysis Purposes / Васютин Р. Р., Ключарев П. Г. // Наука, технологии и бизнес : материалы 6-ой Межвузовской конференции аспирантов, соискателей и молодых учёных, Москва, 16-18 апреля 2024 года / МГТУ им. Н. Э. Баумана (национальный исследовательский университет). - М., 2024. - С. 60-66.

Статья посвящена разработке SAT-решателя для задач криптоанализа. Описана и проанализирована структура типичного SAT-решателя и, в частности, различные эвристики расщепления. Разработана и реализована собственная эвристика расщепления с оптимизацией для задачи криптоанализа. Для тестирования разработанного SAT-решателя был выбран игрушечный блочный шифр CTC2 с гибким параметром длины ключа. Было проведено два вида экспериментов: сравнение времени решения задачи криптоанализа при фиксированной длине ключа и сравнение времени решения этой задачи при растущей длине ключа. В качестве оппонента был выбран известный решатель MiniSAT. Разработанный в данном исследовании SATрешатель выигрывает у MiniSAT во всех проведенных экспериментах согласно результатам тестирования.
Ключевые слова: SAT-решатель, MiniSAT, DPLL, CDCL, GSAT, криптоанализ, КНФ, CTC2