Применение метода Монте-Карло к прогнозированию времени параллельного решения проблемы булевой выполнимости
Заикин О.С., Семенов А.А.

Рассматривается применение метода Монте-Карло к планированию решения сложных вариантов задачи о булевой выполнимости (SAT, Boolean Satisfiability) в пара ллельных вычислительных системах. Распараллеливание SAT-задачи является результатом выделения в множестве булевых переменных исходной конъюнктивной нормальной формы некоторого подмножества, называемого декомпозиционным множеством. Для декомпозиционных множеств можно естественным образом определить ряд параметров, характеризующих "качество" декомпозиции. Для оценки этих параметров предлагается использовать вычислительную схему метода Монте-Карло. В частности, данный метод применен для поиска декомпозиционного множества с наименьшим прогнозным временем решения исходной задачи. Реализована параллельная MPI-программа, с помощью которой на вычислительном кластере был получен прогноз времени решения задачи логического криптоанализа шифра Bivium. Успешно осуществлен логический криптоанализ нескольких ослабленных версий шифра Bivium, проведено сравнение реального времени криптоанализа с прогнозным.

Ключевые слова: задача выполнимости булевых формул, метод Монте-Карло, поиск с запретами, MPI, криптоанализ, шифр Bivium.

Название статьи, аннотация и ключевые слова на английском языке

  • Заикин О.С. – Институт динамики систем и теории управления СО РАН (ИДСТУ СО РАН), ул. Лермонтова, 134, 664033, Иркутск; науч. сотр., e-mail: zaikin.icc@gmail.com
  • Семенов А.А. – Институт динамики систем и теории управления СО РАН (ИДСТУ СО РАН), ул. Лермонтова, 134, 664033, Иркутск; зав. лабораторией, e-mail: biclop.rambler@yandex.ru