1. Lee C. Y. Representation of Switching Circuits by Binary-Decision Programs // Bell Systems Technical Journal. 1959. Vol. 38. P. 985–999. 2. Akers S. B. Binary Decision Diagrams // IEEE Transactions on Computers. 1978. Vol. 27. № 6. P. 509–516. 3. Bryant R. E. Graph-Based Algorithms for Boolean Function Manipulation // IEEE Transactions on Computers. 1986. Vol. 35. № 8. P. 677–691. 4. Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: МЦНМО, 2002. 416 с. 5. Ubar R. Test Generation for Digital Circuits Using Alternative Graphs (in Russian) // Proc. Tallinn Technical University. 1976. № 409. P. 75–81. 6. Яблонский С. В. Введение в дискретную математику. М.: Наука, 1986. 384 с. 7. Семенов А. А., Беспалов Д. В. Технологии решения многомерных задач логического поиска // Вестн. Томск. гос. ун-та. 2005. Приложение. № 14. С. 61–73. 8. Meinel Ch., Theobald T. Algorithms and Data Structures in VLSI-Design: OBDDFoundations and Applications. Berlin: Springer-Verlag, 1998. 267 p. 9. Катленд Н. Вычислимость. Введение в теорию рекурсивных функций. М.: Мир, 1983. 256 с. 10. Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. М.: Мир, 1982. 416 с. 11. Cook S. A. The Complexity of Theorem-Proving Procedures // Proc. 3rd Ann. ACM Symp. on Theory of Computing, ACM. Ohio, 1971. P. 151–159. [Перевод: Кук С. А. Сложность процедур вывода теорем. Кибернетический сборник. Новая серия. Вып. 12. М.: Мир, 1975. С. 5–15] 12. Karp R. M., Lipton R. J. Some Connections between Nonuniform and Uniform Complexity Classes // Proc. of the 12th ACM Symposium on Theory of Computing. 1980. P. 302–309. 13. Fortune S. J. A Sweepline Algorithm for Voronoi Diagrams // Algorithmica. 1987. № 2. P. 153–174. 14. Игнатьев А. С., Семенов А. А., Хмельнов А. Е. Решение систем логических уравнений с использованием BDD // Вестн. Томск. гос. ун-та. 2006. Приложение. № 17. С. 25–29. 15. Menezes A., Van Oorschot P., Vanstone S. Handbook of Applied Cryptography. CRC Press, 1996. 657 p. 16. Семенов А. А. Логико-эвристический подход в криптоанализе генераторов двоичных последовательностей // Тр. междунар. науч. конф. ПАВТ’07. Челябинск: Изд-во ЮУрГУ, 2007. Т. 1. С. 170–180. 17. Алферов А. П., Зубов А. Ю., Кузьмин А. С., Черемушкин А. В. Основы криптографии. М.: Гелиос АРВ, 2002. 480 с. 18. Shiple T. R., Hojati R., Sangiovanni-Vincentelli A. L., Brayton R. K. Heuristic Minimization of BDDs, Using Don’t Cares // University of California, Berkeley. Technical Report No. UCB/ERL M93/58. 1993.

In the paper, the authors consider a new property of a hybrid SAT+ROBDD-derivation. This property consists in a convergence with respect to the number of paths to a terminal vertex 1 in a ROBDD which represents database of conflicts accumulated during the process of non-chronological DPLL.

In the paper, we study algorithmic properties of ROBDD considered in the role of Boolean constraints in the hybrid (SAT + ROBDD) logical derivation. We suggest ROBDD-analogs for the basic algorithmic procedures used in DPLL-derivation such as variable assignment, unit clause, clause learning, and the techniques of delayed computations. A new algorithm intended for ROBDD reordering is proposed. Computational complexity of all the considered algorithms is provided

The report is supposed to consider the possibility of using binary decision diagrams (BDD) for the discrete function inversion in the parallel high-performance computing systems. We describe the architecture of a fundamentally new SAT-solver. The BDD-technology reducing the usage of memory which in turn keeps the search history lies in the basis of the solver. As testing problems we consider cryptanalysis of a number of key stream generators.

В работе рассматривается возможность применения двоичных диаграмм решений (BDD) в задачах обращения дискретных функций на параллельных вычислительных системах. Описывается архитектура принципиально нового решателя SAT-задач. Основу данного решателя составляет базирующаяся на BDD технология уменьшения объема памяти, используемой для хранения истории поиска. В качестве тестовой рассматривается задача криптоанализа генератора ключевого потока известной системы поточного шифрования А5/1.

This paper is a continuation of a series of papers devoted to problems of reversing of discrete functions belonging to class that has intersections with different areas of mathematical cybernetics. In particular the functions used in modern cryptosystems as ciphering transformations belong to the given class. In the paper some distinctive moments concerning the solving of considered functions reversing problems on multiprocessing computing systems are discussed