Application of the Monte Carlo method for estimating the total time of solving the SAT problem in parallel

Authors

  • O.S. Zaikin
  • A.A. Semenov

Keywords:

Boolean satisfiability problem (SAT)
Monte Carlo method
tabu search
MPI
cryptanalysis
Bivium cipher

Abstract

The application of the Monte Carlo method to plan the solving process for hard examples of the Boolean satisfiability problem (SAT) on parallel computing systems is discussed. The parallelization of the SAT problem is reached as a result of choosing the subset of the set of variables of an original CNF (Conjunctive Normal Form). This set is called a decomposition set. For such sets, we can naturally define a number of parameters to measure the «quality» of decomposition. In order to evaluate these parameters, we use the computational scheme based on the Monte Carlo method. In particular, this method is used to search for the decomposition set with minimal predicted time of solving the original problem. Using the implemented parallel MPI-program, it is possible to obtain a prediction of time required to perform the logical cryptanalysis of the Bivium cipher on a computing cluster. We successfully performed the logical cryptanalysis of several weakened versions of the Bivium cipher. The computing cost of such a cryptanalysis is in agreement with the predicted one.

New computational technologies

Downloads

Published

2014-01-23

Issue

Vol. 15 (2014): Issue 1.

Section

Section 1. Numerical methods and applications

Author Biographies

O.S. Zaikin

Matrosov Institute for System Dynamics and Control Theory of SB RAS (IDSTU SB RAS)
• Researcher

A.A. Semenov

Matrosov Institute for System Dynamics and Control Theory of SB RAS (IDSTU SB RAS)
• Head of Laboratory

References

  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.