Статья посвящена проблеме преобразования алгоритмических описаний дискретных функций в эквациональные описания, имеющие вид булевых уравнений. Основу развиваемого в работе аппарата составляют процедуры пропозиционального кодирования программ для двоичной машины с произвольным доступом. На базе этих процедур строятся преобразования высокоуровневых описаний алгоритмов вычисления дискретных функций в булевы уравнения.

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