List of issues > Series «Mathematics». 2011. Vol. 1
Transformations of discrete functions calculation algorithms to boolean equations
The article is devoted to the problem of transforming algorithmic descriptions of discrete functions to their equational descriptions in the form of boolean equations. We propose an approach based on propositional encoding procedures for binary random access machine programs. These procedures are used to build transformations of high-level descriptions of discrete functions calculation algorithms to boolean equations.
1. Ахо А. Построение и анализ вычислительных алгоритмов / A. Axo, Дж. Хопкрофт, Дж. Ульман. - М. : Мир, 1979. - 536 с.
2. Гэри М. Вычислительные машины и труднорешаемые задачи / М. Гэри, Д. Джонсон. - М. : Мир, 1982. - 416 с.
3. Решение задач криптоанализа поточных шифров в распределенных вычислительных средах / М. А. Посыпкин, О. С. Заикин, Д. В. Беспалов, А. А. Семенов // Тр. ИСА РАН. - 2009. - Т. 46. - С. 119-137.
4. Семенов А. А. Трансляция алгоритмов вычисления дискретных функций в выражения пропозициональной логики / А. А. Семенов // Прикладные алгоритмы в дискретном анализе. - Иркутск : Изд-во ИГУ, 2008. - Вып. 2. - С. 70-98. - (Дискретный анализ и информатика).
5. Семенов А. А. О преобразованиях Цейтина в логических уравнениях / А. А. Семенов // Прикладная дискретная математика. - 2009. - № 4. - С. 28-50.
6. Системная компьютерная биология / под ред. Н. А. Колчанова, С. С. Гончарова, В. А. Лихошвая, В. А. Иванисенко. - Новосибирск : Изд.-во СО РАН, 2008. - 767 c.
7. SAT-подход в криптоанализе некоторых систем поточного шифрования / А. А. Семенов, О. С. Заикин, Д. В. Беспалов, А. А. Ушаков // Вычисл. технологии. - 2008. - Т. 13, № 6. - С. 134-150.
8. Цейтин Г. С. О сложности вывода в исчислении высказываний / Г. С. Цейтин // Зап. науч. семинаров ЛОМИ АН СССР. - 1968. - Т. 8. - С. 234-259.
9. Cook S. A. The complexity of theorem-proving procedures / S. A. Cook // Proc. 3rd Ann. ACM Symp. on Theory of Computing (STOC 71). - ACM, 1971. - P. 151-159.
10. Cook S. A. Finding hard instances of the satisfiability problem: A survey / S. A. Cook, G. Mitchel // DIMACS Series in Discrete Mathematics and Theoretical Computer Science. - 1997. - Vol. 35. - P. 1-17.
11. Menezes A. Handbook of Applied Cryptography / A. Menezes, P. Oorschot, S. Vanstone. - CRC Press, 1996. - 657 p.
12. Massacci F. Logical Cryptanalysis as a SAT Problem / F. Massacci, L. Marraro // Journal of Automated Reasoning. - 2000. - Vol. 24, N 1-2. - P. 165-203.
13. Prestwich S. CNF encodings // In Handbook of Satisfiability / S. Prestwich eds.: A. Biere, M.Heule, H. van Maaren, T. Walsh. - IOS Press, 2009. - P. 75-97.
14. URL: http://embedded.eecs.berkeley.edu/pubs/downloads/espresso