The article i s devotedto converting combinatorial problems into the problems of solving Boolean equations.Some theoretical results are presented as the basis of technology for propositional encodingof algorithms calculating discrete functions. Software system Transalg implementing thetechnology is described. Examples of using the Transalg for translating cryptoanalysis algorithmsto SAT-problem are presented. The technics for translating 0-1-ILP optimizationalgorithms into SAT are considered too.
Download file
Counter downloads: 81
- Title Technology for translating combinatorialproblems into boolean equations
- Headline Technology for translating combinatorialproblems into boolean equations
- Publesher
Tomsk State University - Issue Prikladnaya Diskretnaya Matematika - Applied Discrete Mathematics 1(11)
- Date:
- DOI
Keywords
cryptoanalysis, propositional encoding, Boolean equations, discrete functions, пропозициональное кодирование, булевы уравнения, криптоанализ, дискретные функцииAuthors
References
Ganai M. and Gupta A. SAT-based scalable formal verification solutions. Springer, 2007. 326 p.
http://minisat.se/MiniSat+.html
Системная компьютерная биология / под ред. Н. А. Колчанова, С.С.Гончарова, В. А. Лихошвая, В. А. Иванисенко. Новосибирск: Изд-во СО РАН, 2008. 767 c.
EenN. and Sorensson N. Translating Pseudo-Boolean Constraints into SAT // J. Satisfiab., Bool. Model. Comp. 2006. V.2. P. 1-25.
http://miplib.zib.deMIPLIB-Mixed Integer Problem Library.
Schneier B. Applied Cryptography, Second Edition: Protocols, Algorithms, and Source Code in C. John Wiley and Sons, 1996. 758 p.
Massacci F. and Marraro L. Logical Cryptoanalysis as a SAT Problem: the Encoding of the Data Encryption Standard. Preprint. Dipartimento di Imformatica e Sistemistica, Universita di Roma "La Sapienza", 1999.
http://embedded.eecs.berkeley.edu/pubs/downloads/espresso
http://www.cril.univ-artois.fr/PB10/
Rueppel R. Correlation immunity and the summation generator // LNCS. 1986. V. 218. P. 260-272.
Посыпкин М. А, Заикин О. С., Беспалов Д. В., Семёнов А. А. Решение задач криптоанализа поточных шифров в распределенных вычислительных средах // Труды ИСА РАН. 2009. Т. 46. С. 119-137.
Massacci F. andMarraro L. Logical Cryptanalysis as a SAT Problem // J. Autom. Reas. 2000. V. 24. No. 1-2. P. 165-203.
Семёнов А. А., Заикин О. С., Беспалов Д. В., Ушаков А. А. SAT-подход в криптоанализе некоторых систем поточного шифрования // Вычислительные технологии. 2008. Т. 13. №6. С. 134-150.
Ахо А., Сети Р., Ульман Дж. Компиляторы. Принципы, технологии, инструменты. М.; СПб.; Киев: Вильямс, 2001. 768 с.
Menezes A., Oorschot P., and VanstoneS. Handbook of Applied Cryptography. CRC Press, 1996. 657 p.
Cook S. A. and MitchelG. Finding hard instances of the satisfiability problem: A survey // DIMACS Ser. Discr. Mathem. Theoret. Comp. Scie. 1997. V.35. P. 1-17.
Семёнов А. А. О преобразованиях Цейтина в логических уравнениях // Прикладная дискретная математика. 2009. №4. С. 28-50.
Shepherdson J. C. and Sturgis H. E. Computability of recursive functions // J. Assoc. Comp. Machinery. 1963. V. 10. P. 217-255.
Катленд Н. Вычислимость. Введение в теорию рекурсивных функций. М.: Мир, 1983. 256 с.
Цейтин Г. С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР. 1968. Т. 8. С. 234-259.
Prestwich S. CNF encodings. In Handbook of Satisfiability / eds. A. Biere, M. Heule, H. van Maaren, T. Walsh. IOS Press, 2009. P. 75-97.
Cook S. A. The complexity of theorem-proving procedures // Proc. 3rd Ann. ACM Symp. on Theory of Computing (STOC 71). ACM. 1971. P. 151-159.
GareyM. R. and Johnson S. Computers and intractability: A guide to the theory of NPcompleteness. W. H. Freeman, 1979. 340 p.
Семёнов А. А. Трансляция алгоритмов вычисления дискретных функций в выражения пропозициональной логики // Прикладные алгоритмы в дискретном анализе. Сер. Дискретный анализ и информатика. 2008. Вып. 2. С. 70-98.
Rudeanu S. Boolean functions and equations. Amsterdam; London: North-Holland Publishing Company, 1974. 442 p.
Technology for translating combinatorialproblems into boolean equations | Prikladnaya Diskretnaya Matematika - Applied Discrete Mathematics. 2011. № 1(11).
Download full-text version
Download fileCounter downloads: 197