Алгоритмы построения декомпозиционных множеств для крупноблочного распараллеливания SAT-задач
| Авторы: | А. А. Семенов, О. С. Заикин |
| Аннотация: | В работе приводятся алгоритмы построения декомпозиционных множеств, используемых для крупноблочного распараллеливания SAT-задач и их последующего решения в распределенных вычислительных средах. В основе предлагаемых алгоритмов лежит вычислительная схема метода Монте-Карло. |
| Ключевые слова: | метод Монте-Карло; дискретные функции; SAT-задачи; круп- ноблочный параллелизм |
| УДК: | 519.6 |
| Литература: |
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. |