В работе приводятся алгоритмы построения декомпозиционных множеств, используемых для крупноблочного распараллеливания SAT-задач и их последующего решения в распределенных вычислительных средах. В основе предлагаемых алгоритмов лежит вычислительная схема метода Монте-Карло.

1. Handbook of Satisfiability / A. Biere, V. Heule, H. van Maaren, T. Walsh. — IOS Press, 2009. – 980 p.

2. Up-to-date links for the SATisfiability problem [Electronic recource]: www.satlive.org

3. Schubert T. PaMiraXT: Parallel SAT Solving with Threads and Message Passing / T. Schubert, M. Lewis, B. Becker // Journal on Satisfiability, Boolean Modeling and Computation. – 2009. – Vol. 6. – P. 203–222.

4. Hamadi Y. ManySAT: a Parallel SAT Solver / Y. Hamadi, S. Jabbour, L. Sais // Journal on Satisfiability, Boolean Modeling and Computation. – 2009. – Vol. 6. – P. 245–262.

5. Ignatiev A. DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions / A. Ignatiev, A. Semenov // LNCS. – 2011. – Vol. 6695. – P. 76–89.

6. Schulz S. Parallel SAT Solving on Peer-to-Peer Desktop Grids / S. Schulz, W. Blochinger // Journal Of Grid Computing. – 2010. – Vol. 8, N 3. – P. 443–471.

7. Hyvarinen A. Grid-Based SAT Solving with Iterative Partitioning and Clause Learning / A. Hyvarinen, I. Niemela, T. Junttila // LNCS. – 2011. – Vol. 6876. – P. 385–399.

8. Posypkin M. Using BOINC desktop grid to solve large scale SAT problems / M. Posypkin, A. Semenov, O. Zaikin // Computer Science Journal. — 2012. – Vol. 13, N 1. – P. 25–34.

9. Davis M. A machine program for theorem proving / M. Davis, G. Logemann, D. Loveland // Communication of the ACM. – 1962. – Vol. 5, issue 7. – P. 394–397.

10. Marques-Silva J. P. GRASP: A search algorithm for propositional satisfiability / J. P. Marques-Silva, K. A. Sakallah // IEEE Transactions on Computers. – 1999. – Vol. 48, N 5. – P. 506–521.

11. Metropolis N. The Monte Carlo method / N. Metropolis, S. Ulam // J. Amer. statistical assoc. – 1946. – Vol. 44, № 247. – P. 335–341.

12. Ермаков С. М. Метод Монте-Карло и смежные вопросы / С. М. Ермаков. – М. : Наука, 1971. – 327 с.

13. Стрекаловский А. С. Элементы невыпуклой оптимизации / А. С. Стрекаловский. – Новосибирск : Наука, 2003. 355 с.

14. Цейтин Г. С. О сложности вывода в исчислении высказываний / Г. С. Цейтин // Записки научных семинаров ЛОМИ АН СССР. — 1968. — Т. 8. — C. 234–259.

15. Jarvisalo M. Limitations of restricted branching in clause learning / M. Jarvisalo, T. Junttila // Constraints. — 2009. — Vol. 14, № 3. — pp. 325–356.

16. Семенов А. А. Декомпозиционные представления логических уравнений в задачах обращения дискретных функций / А. А. Семенов // Изв. РАН. Теория и системы управления. – 2009. – № 5. – С. 47–61.

17. Dowling W. Linear-time algorithms for testing the satisfiability of propositional Horn formulae / W. Dowling, J. Gallier // Journal of Logic Programming. – 1984. – Vol. 1, N 3. – P. 267–284.

18. Пападимитриу Х. Комбинаторная оптимизация / Х. Пападимитриу, К. Стайглиц. – М. : Мир, 1985. – 510 с.

19. Glover F. Tabu Search / F. Glover, M. Laguna. – Dordrecht : Kluwer Acad. Publ., 1997.

20. Kirkpatrick S. Optimization by simulated annealing / S. Kirkpatrick, C. D. Gelatt, M. P. Vecchi // Science. – 1983. – Vol. 220. – P. 671–680.

21. Кластер Blackford ИДСТУ СО РАН: http://hpc.icc.ru/hardware/blackford.php

22. Biryukov A. Real time cryptanalysis of A5/1 on a PC / A. Biryukov, A. Shamir, D. Wagner // LNCS. – 2001. – Vol. 1978. – P. 1–18.

23. Parallel logical cryptanalysis of the generator A5/1 in BNB-Grid system / A. Semenov, O. Zaikin, D. Bespalov, M. Posypkin // LNCS. – 2011. – Vol. 6873. – P. 473–483.