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

Авторы

  • О.С. Заикин Институт динамики систем и теории управления имени В.М. Матросова СО РАН (ИДСТУ СО РАН) https://orcid.org/0000-0002-0145-5010
  • А.А. Семенов Институт динамики систем и теории управления имени В.М. Матросова СО РАН (ИДСТУ СО РАН)

Ключевые слова:

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

Аннотация

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

Авторы

О.С. Заикин

А.А. Семенов

Институт динамики систем и теории управления имени В.М. Матросова СО РАН (ИДСТУ СО РАН)
ул. Лермонтова, 134, 664033, Иркутск
• заведующий лабораторией

Библиографические ссылки

  1. Böhm M., Speckenmeyer E. A fast parallel SAT solver - efficient workload balancing // Annals of Mathematics and Artificial Intelligence. 1996. 17, N 3/4. 381-400.
  2. Hyvärinen A.E. J., Junttila T.A., Niemelä I. A distribution method for solving SAT in grids // Lecture Notes in Computer Science. Vol. 4121. Heidelberg: Springer, 2006. 430-435.
  3. Hyvärinen A.E. J., Junttila T.A., Niemelä I. Partitioning SAT instances for distributed solving // Lecture Notes in Computer Science. Vol. 6397. Heidelberg: Springer, 2010, 372-386.
  4. Hyvärinen A.E. J., Junttila T.A., Niemelä I. Grid-based SAT solving with iterative partitioning and clause learning // Lecture Notes in Computer Science. Vol. 6876. Heidelberg: Springer, 2011, 385-399.
  5. Hyvärinen A.E. J. Grid based propositional satisfiability solving. Ph.D. Thesis. Department of Information and Computer Science. Aalto (Finland): Aalto Univ. Press, 2011.
  6. Заикин О.С., Семенов А.А. Технология крупноблочного параллелизма в SAT-задачах // Проблемы управления. 2008. № 1. 43-50.
  7. Посыпкин М.А., Заикин О.С., Беспалов Д.В., Семенов А.А. Решение задач криптоанализа поточных шифров в распределенных вычислительных средах // Тр. Института системного анализа РАН. 2009. 46. 119-137.
  8. Semenov A., Zaikin O., Bespalov D., Posypkin M. Parallel logical cryptanalysis of the generator A5/1 in BNB-Grid system // Lecture Notes in Computer Science. Vol. 6873. Heidelberg: Springer, 2011, 473-483.
  9. Semenov A., Zaikin O., Bespalov D., Posypkin M. Parallel algorithms for SAT in application to inversion problems of some discrete functions (arXiv: 1102.3563 [cs.DC]; Cornell Univ. Library), 2011 (http://arxiv.org/abs/1102.3563).
  10. Семенов А.А., Заикин О.С. Алгоритмы построения декомпозиционных множеств для крупноблочного распараллеливания SAT-задач // Известия Иркутского гос. ун-та. Серия «Математика». 2012. № 4. 79-94.
  11. Metropolis N., Ulam S. The Monte Carlo method // J. of the American Statistical Association. 1949. 44, N 247. 335-341.
  12. Заикин О.С., Семенов А.А., Посыпкин М.А. Процедуры построения декомпозиционных множеств для распределенного решения SAT-задач в проекте добровольных вычислений SAT@home // Управление большими системами. Вып. 43. М.: Ин-т проблем управления РАН, 2013. 138-156.
  13. Canniére C.D. Trivium: A stream cipher construction inspired by block cipher design principles // Lecture Notes in Computer Science. Vol. 4176. Heidelberg: Springer, 2006, 171-186.
  14. Zhang H., Bonacina M.P., Hsiang J. PSATO: a distributed propositional prover and its application to quasigroup problems // J. of Symbolic Computation. 1996. 21. 543-560.
  15. Heule M., Kullmann O., Wieringa S., Biere A. Cube and conquer: guiding CDCL SAT solvers by lookaheads // Lecture Notes in Computer Science. Vol. 7261. Heidelberg: Springer, 2011, 50-65.
  16. Mcdonald C., Charnes C., Pieprzyk J. Attacking Bivium with MiniSat. Technical Report 2007/040. ECRYPT Stream Cipher Project, 2007 (http://eprint.iacr.org/2007/129).
  17. Eibach T., Pilz E., Völkel G. Attacking Bivium using SAT solvers // Lecture Notes in Computer Science. Vol. 4996. Heidelberg: Springer, 2008. 63-76.
  18. Soos M., Nohl K., Castelluccia C. Extending SAT solvers to cryptographic problems // Lecture Notes in Computer Science. Vol. 5584. Heidelberg: Springer, 2009. 244-257.
  19. Soos M. Grain of salt - an automated way to test stream ciphers through sat solvers // Proc. of the Workshop on Tools for Cryptanalysis. Egham: Univ. of London, 2010. 131-144.
  20. Ермаков С.М. Метод Монте-Карло и смежные вопросы. М.: Наука, 1971.
  21. Феллер В. Введение в теорию вероятностей и ее приложения. 2. М.: Мир, 1984.
  22. Glover F., Laguna M. Tabu search. Norwell: Klüwer, 1997.
  23. Пападимитриу Х., Стайглиц К. Комбинаторная оптимизация. Алгоритмы и сложность. М.: Мир, 1984.
  24. Järvisalo M., Junttila T.A. Limitations of restricted branching in clause learning // Constraints. 2009. 14, N 3. 325-356.
  25. Заикин О.С. Реализация процедур прогнозирования трудоемкости параллельного решения SAT-задач // Вестник Уфимского гос. авиационного техн. ун-та. 2010. 14, № 4. 210-220.
  26. Заикин О.С., Отпущенников И.В., Семенов А.А. Параллельные алгоритмы решения проблемы выполнимости в применении к оптимизационным задачам с булевыми ограничениями // Вычислительные методы и программирование: Новые вычислительные технологии. 2011. 12, № 1. 205-212.
  27. Eén N., Sörensson N. An extensible SAT-solver // Lecture Notes in Computer Science. Vol. 2919. Heidelberg: Springer, 2003. 502-518.
  28. Гришагин В.А., Свистунов А.Н. Параллельное программирование на основе MPI. Изд-во Нижегородского гос. ун-та им. Н.И. Лобачевского, 2005.
  29. Отпущенников И.В., Семенов А.А. Технология трансляции комбинаторных проблем в булевы уравнения // Прикладная дискретная математика. 2011. № 1. 96-115.
  30. Massacci F., Marraro L. Logical cryptanalysis as a SAT problem // J. of Automated Reasoning. 2000. 24, N 1/2. 165-203.
  31. Maximov A., Biryukov A. Two trivial attacks on Trivium // Lecture Notes in Computer Science. Vol. 4876. Heidelberg: Springer, 2007. 36-55.
  32. Вычислительный кластер «Академик В.М. Матросов» [Электронный ресурс] // Иркутский суперкомпьютерный центр Сибирского отделения РАН (http://hpc.icc.ru/hardware/matrosov.php).
  33. Dowling W., Gallier J. Linear-time algorithms for testing the satisfiability of propositional Horn formulae // J. of Logic Programming. 1984. 1, N 3. 267-284.
  34. Semenov A., Zaikin O. On estimating total time to solve SAT in distributed computing environments: application to the SAT@home project (arXiv: 1308.0761 [cs.AI]; Cornell Univ. Library), 2013.

Загрузки

Опубликован

23-01-2014

Как цитировать

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

Выпуск

Раздел

Раздел 1. Вычислительные методы и приложения

Наиболее читаемые статьи этого автора (авторов)