ГлавнаяАрхивТехнология трансляции комбинаторных проблем в булевы уравнения

Технология трансляции комбинаторных проблем в булевы уравнения | Прикладная дискретная математика. 2011. № 1(11).

Рассматриваются проблемы сведения некоторых комбинаторных задач к задачам поиска решений булевых уравнений. Приведены теоретические результаты, являющиеся базой технологии пропозиционального кодирования алгоритмов, вычисляющих дискретные функции. Описан программный комплекс Transalg - многофункциональный транслятор комбинаторных проблем в булевы уравнения. Приведены примеры использования комплекса Transalg для сведения задач криптоанализа к SAT-задачам. Рассмотрены основы техники трансляции оптимизационных задач 0-1-ЦЛП в SAT-задачи.
  • Title Технология трансляции комбинаторных проблем в булевы уравнения
  • Headline Технология трансляции комбинаторных проблем в булевы уравнения
  • Publesher Tomask State UniversityTomsk State University
  • Issue Прикладная дискретная математика 1(11)
  • Date:
  • DOI
Ключевые слова
cryptoanalysis, propositional encoding, Boolean equations, discrete functions, пропозициональное кодирование, булевы уравнения, криптоанализ, дискретные функции
Авторы
Ссылки
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.
Технология трансляции комбинаторных проблем в булевы уравнения | Прикладная дискретная математика. 2011. № 1(11).
Технология трансляции комбинаторных проблем в булевы уравнения | Прикладная дискретная математика. 2011. № 1(11).
Полнотекстовая версия