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

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