Методы и средства преобразования процедурных описаний дискретных функций в булевы уравнения
Диссертация
Одним из значимых достижений в исследовании комбинаторных проблем можно считать прогресс в решении систем логических (булевых) уравнений большой размерности. На сегодняшний день удается решать системы, содержащие сотни тысяч булевых переменных и уравнений (булевых ограничений). К булевым уравнениям эффективно сводятся многочисленные комбинаторные задачи. Процедура перехода от исходной постановки… Читать ещё >
Список литературы
- Prestwich S. D. CNF encodings. 1. Handbook of Satisfiability (editors: A. Biere, M. Heule, H. van Maaren, T. Walsh). 2009. Vol. 6. pp. 75−97.
- Marques-Silva J., Lynce I. Towards robust cnf encodings of cardinality constraints //In Thirteenth International Conference on Principles and Practice of Constraint Programming. Springer. Lecture Notes in Computer Science. 2007. Vol. 4741. pp. 483−497.
- Massacci F., Marraro L. Logical Cryptanalysis as a SAT Problem // Journal of Automated Reasoning. 2000. Vol. 24, no. 1−2. pp. 165−203.
- Massacci F., 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.
- Gent I. P., Lynce I. A sat encoding for the social golfer problem // In Workshop on Modelling and Solving Problems with Constraints, IJCAI'05. 2005.
- Gent I.P., Nightingale P. A new encoding of alldiffercnt into sat // In Third International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, CP'04. 2004.
- Опарин Г. А., Богданова В. Г., Сидоров И. А. Интеллектуальный решатель задач в булевых ограничениях в распределенной вычислительной среде // Информационные и математические технологии в науке и управлении: Иркутск: ИСЭМ РАН. 2007. С. 32−40.
- Опарин Г. А., Новопашин А. П. Булево моделирование планированиядействий в распределенных вычислительных системах // Известия РАН. Теория и системы управления. 2004. № 5. С. 105−108.
- Oparin G.A., Novopashin А. P. Boolean models and planning methods for parallel abstract programs // Automation and Remote Control. 2008. Vol. 69, no. 8. pp. 1423−1432.
- Опарин Г. А., Новопашин А. П. Булевы модели синтеза параллельных планов решения вычислительных задач // Вестник НГУ. Серия: Информационные технологии. 2008. Т. 6, № 1. С. 53−59.
- Gu J., Purdom P., Franco J., Wah B. W. Algorithms for the satisfiability problem. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2000.
- Een N., Sorrensson N. Translating Pseudo-Boolean Constraints into SAT // Journal on Satisfiability, Boolean Modeling and Computation. 2006. Vol. 2. pp. 1−25.
- Касьянов В. H., Поттосин И. В. Методы построения трансляторов. Новосибирск: «Наука», 1986. С. 344.
- Григоренко Е. Д., Евдокимов А. А., Лихошвай В. А., Лобарева И. А. Неподвижные точки и циклы автоматных отображений, моделирующих функционирование генных сетей // Вестник Томского гос. ун-та. Приложение. 2005. Т. 14. С. 206−212.
- Системная компьютерная биология, Под ред. Н. А. Колчанова, С. С. Гончарова, В. А. Лихошвая, В. А. Иванисенко. Новосибирск: Изд-во СО РАН, 2008. С. 767.
- MiniSat. URL: http://minisat.se/MiniSat.html (дата обращения: 10.05.2011).
- Отпущенников И.В., Семенов A.A. Технология трансляции комбинаторных проблем в булевы уравнения // Прикладная дискретная математика. 2011. № 1. С. 96−115.
- Отпущенников И.В., Семенов A.A. Преобразования алгоритмов вычисления дискретных функций в булевы уравнения // Известия ИГУ. Серия: математика. 2011. Т. 4, № 1. С. 83−96.
- Семенов A.A., Отпущенников И. В., Кочсмазов С. Е. Пропозициональный подход в задачах тестирования дискретных автоматов // Современные технологии. Системный анализ. Моделирование. 2009. № 4. С. 48−56.
- Семенов A.A., Отпущенников И. В. Об алгоритмах обращения дискретных функций из одного класса // Прикладные алгоритмы в дискретном анализе. Серия: дискретный анализ и информатика- вып. 2. Изд-во ИГУ. 2008. С. 127−156.
- Отпущенников И. В., Семенов А. А. Программная трансляция алгоритмов в пропозициональную логику применительно к комбинаторным задачам // Прикладная дискретная математика. Приложение. 2010. № 3. С. 81−82.
- Отпущенников И. В., Семенов А. А. Инструментальное средство трансляции алгоритмов вычисления дискретных функций в выражения исчисления высказываний Transaig 1.0. Свидетельство о государственной регистрации программы для ЭВМ № 2 011 611 151 (03.02.2011).
- Яблонский С. В. Введение в дискретную математику. Москва: «Наука», 1986. С. 384.
- Мендельсон Э. Введение в математическую логику. Москва: «Наука», 1971. С. 320.
- Катлепд Н. Вычислимость. Введение в теорию рекурсивных функций. Москва: «Мир», 1983. С. 256.
- Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. Москва: «Мир», 1982. С. 416.
- Пападимитриу X., Стайглиц К. Комбинаторная оптимизация. Алгоритмы и сложность. Москва: «Мир», 1985. С. 510.
- Васильев Ю. Л., Ветухновский Ф. Я., Глаголев В. В. и др. Дискретная математика и математические вопросы кибернетики. Москва: «Наука», 1974. Т. 1.
- Нигматуллин Р. Г. Сложность булевых функций. Москва: «Наука», 1991. С. 240.
- Wegener I. The complexity of Boolean function. Stuttgart: J. Wiley and Sons ltd, 1987.
- Закревский А. Д., Поттосин Ю. В., Черемисинова Л. Д. Логические основы проектирования дискретных устройств. Москва: ФИЗМАТЛИТ, 2007. С. 590.
- Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М., МЦНМО, 2002.
- Гаранина Н. О., Шилов Н. В. Верификация комбинированных логик знаний, действий и времени в моделях // Системная информатика. 2005. Т. 10. С. 114−173.
- Amman P., Ritchey R. Using Model Checking to Analyze Network Vulnerabilities // Proc. Of the 2000 IEEE Symposium on Security and Privacy. 2000. pp. 156−165.
- Sheyer O., Jha S., Wing J., et al. Automated Generation and Analysis of Attack Graphs // 2002 IEEE Symposium on Security and Privacy. 2002.
- Nemhauser G., Wolsey L. Integer and Combinatorial Optimization. John Wiley and Sons Ltd., 1998.
- Cela E. The Quadratic Assignment Problem. Theory and Algorithms. Kluwer Acadcmic Publishers, 1998. P. 287.
- Schrijver A. Combinatorial Optimization. Springer Verlag, Berlin, 2003.
- Cook S. A. The complexity of theorem-proving procedures // Proceedings of the third Annual ACM Symposium on Theory of Computing. 1971. Vol. 35, no. 8. pp. 151−159.
- Shepherdson J.C., Sturgis H. E. Computability of recursive functions // J. Assoc. Сотр. Machinery. 1963. Vol. 10. pp. 217−255.
- Семенов А. А. Трансляция алгоритмов вычисления дискретных функций в выражения пропозициональной логики // Прикладные алгоритмы в дискретном анализе. Серия: Дискретный анализ и информатика. 2008. Т. 2. С. 70−98.
- Menezes A., van Oorshot P., Vanstone S. Handbook of Applied Cryptography. CRC Press, 1996. P. 657.
- Schneier B. Applied Cryptography, Second Edition: Protocols, Algorithms, and Source Code in C. John Wiley and Sons, 1996. P. 758.
- Лидл P., Нидеррайтер Г. Конечные поля (в двух томах). Москва: «Мир», 1988.
- Biryukov A., Shamir A., Wagner D. Real Time Cryptanalysis of A5/1 on a PC. Fast Software Encryption Workshop 2000, April 10−12. New-York City, 2000.
- Семенов А. А. О преобразованиях Цейтина в логических уравнениях // Прикладная дискретная математика. 2009. № 4. С. 28−50.
- Цейтин Г. С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР. 1968. Т. 8. С. 234−259.
- Tseitin G. On the complexity of derivation in prepositional calculus // Automation of reasoning. 1983. Vol. 2. pp. 466−483.
- Hachtel G.D., Somenzi F. Logic synthesis and verification algorithms. Kluwer Ac. Publ., 2002.
- Черемисинова Jl. Д., Новиков Д. Я. Проверка схемной реализации частичных булевых функций // Вестник Томского гос. ун-та. Управление, вычислительная техника, информатика. 2008. № 4 (5). С. 102−111.
- Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification. URL: http://www.eecs.berkeley.edu/alanmi/abc/ (дата обращения: 10.05.2011).
- Kuehlmann A., Cornelis A. J., van Eijk. Combinational and Sequentional Equivalence Checking // Logic synthesis and Verification, Ed. by S. Hassoun, T. Sasao, R. K. Brayton. Kluwer Academic Publishers, 2002. pp. 343−372.
- Advanced Formal Verification // Ed. by R. Drechsler. Springer, 2005. P. 280.
- Ganai M., Gupta A. SAT-based scalable formal verification solutions. Springer, 2007. P. 326.
- Boole G. An investigation of the laws of thought on which are founded the mathematical theories of logic and probabilities. London, 1854.
- Rudeanu S. Boolean functions and equations. Amsterdam-London: North-Holland Publ. Сотр., 1974. P. 442.
- Akers S.B. On a theory of Boolean functions //J. Soc. Ind. Appl. Math. 1959. Vol. 7, no. 4. pp. 487−498.
- Buttner W., Simonis H. Embedding Boolean expressions into logic programming // Journal of Symbolic Computation. 1987. Vol. 4. pp. 191−205.
- Brown F. M. Boolean Reasoning: The Logic Of Boolean Equations. Dover Publications, 2003. P. 304.
- Бохмапп Д., Постхоф X. Двоичные динамические системы. Москва: «Энергоатомиздат», 1986. С. 401.
- Семенов А. А., Буранов Е. В. Погружение задачи криптоанализа симметричных шифров в пропозициональную логику // Вычислительные технологии (совместный выпуск с журналом «Региональный вестник Востока»), 2003. Т. 8. С. 118−126.
- Buchberger В. Grobner-Bases: An Algorithmic Method in Polynomial Ideal Theory // Multidimensional Systems Theory. 1985. Vol. 6. pp. 184−232.
- Кокс Д., Литтл Д., О’Ши Д. Идеалы, многообразия и алгоритмы. Москва: «Мир», 2000. С. 687.
- Агибалов Г. П. Логические уравнения в криптоанализе генераторов ключевого потока // Вестник Томского гос. ун-та. Приложение. 2003. № 6. С. 31−41.
- Тимошевская Н. Е. О линеаризационно эквивалентных покрытиях // Вестник Томского гос. ун-та. Приложение. 2005. № 14. С. 84−91.
- Тимошевская Н. Е. Задача о кратчайшем линеаризационном множестве // Вестник Томского гос. ун-та. Приложение. 2005. № 14. С. 79−83.
- Семенов А. А. О сложности обращения дискретных функций из одногокласса // Дискретный анализ и исследование операций. 2004. Т. 11, № 4. С. 44−55.
- Семенов А. А., Заикин О. С., Беспалов Д. В., Ушаков А. А. SAT-подход в криптоанализе некоторых систем поточного шифрования // Вычислительные технологии. 2008. Т. 13, № 6. С. 134−150.
- Bryant R. Е. Graph-Based Algorithms for Boolean Function Manipulation // IEEE Transactions on Computers. 1986. Vol. 35, no. 8. pp. 677−691.
- Bryant R. E. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams // ACM Computing Surveys. 1992. Vol. 24, no. 3. pp. 293−318.
- Meinel C., Theobald T. Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications. Springer-Verlag, 1998.
- Davis M., Logemann G., Loveland D. A machine program for theoremproving // Communications of the ACM. 1962. Vol. 5, no. 7. pp. 394−397.
- Marques-Silva J. P., Sakallah K. A. GRASP: A search algorithm for propositional satisfiability // IEEE Transactions on Computers. 1999. Vol. 48, no. 5. pp. 506−521.
- Zhang L., Madigan C.F., Moskewicz M.H., Malik S. Efficient conflict driven learning in a boolean satisfiability solver // In Proceedings of International Conference on Computer-Aided Design. 2001. pp. 279−285.
- Goldberg E., Novikov Y. Berkmin: The Fast and Robust SAT Solver // Automation and Test in Europe (DATE). 2002. pp. 142−149.
- Prestwich S.D. Sat problems with chains of dependent variables // Discrete Applied Mathematics. 2002. Vol. 3037. pp. 1−2.
- Crawford J. M., Baker А. В. Experimental results on the application of satisfiability algorithms to scheduling problems // In Twelfth National Conference on Artificial Intelligence. AAAI Press. 1994. Vol. 2. pp. 1092−1097.
- Ernst M., Millstein T., Weld D. Automatic sat-compilation of planning problems //In Fifteenth International Joint Conference on Artificial Intelligence. 1997. pp. 1169−1176.
- Опарин Г. А., Богданова В. Г. РЕБУС — интеллектуальный решатель комбинаторных задач в булевых ограничениях // Вестник НГУ. Серия: Информационные технологии. 2008. Т. 6, № 1. С. 60−68.
- Gent I. P. Arc consistency in sat. IOS Press, 2002. pp. 121−125.
- Kasif S. On the parallel complexity of discrete relaxation in constraint satisfaction networks // Artificial Intelligence. 1990. Vol. 45. pp. 275−286.
- Walsh T. Sat vs CSP // Lecture Notes in Computer Science. 2000. Vol. 1894. pp. 441−456.
- Bessiere C., Hebrard E., Walsh T. Local consistencies in sat // Lecture Notes in Computer Science. 2003. Vol. 2919. pp. 229−314.
- Bacchus F. Gac via unit propagation // Lecture Notes in Computer Science. 2007. Vol. 4741. pp. 133−147.
- Сергиепко A. M. VHDL для проектирования вычислительных устройств. Изд-во ТИД «ДС», 2003. С. 208.
- Поляков А. К. Языки VHDL и Verilog в проектировании цифровой аппаратуры. Москва: СОЛОН — Пресс, 2003. С. 320.
- King J. С. Symbolic execution and program testing // Communications of the ACM. 1976. Vol. 19, no. 7. pp. 385−394.
- Hansen Т., Schachte P., Sondergaard H. State joining and splitting for the symbolic execution of binaries // Springer-Verlag Berlin Heidelberg. 2009. pp. 76−92.
- Abstract Interpretation, MIT course. URL: http://web.mit.edu/afs/ athena.mit.edu/course/16/16.399/www (дата обращения: 10.05.2011).
- Bagnara R., Hill P. M., Pescetti A., Zaffanella E. On the design of generic static analyzers for imperative languages. 2007. arXiv: cs/70 3116v2 cs. PL].
- Wichmann В., Canning A., Cluttcrbuck D. L. et al. Industrial Perspective on Static Analysis // Software Engineering Journal. 1995. Vol. 10, no. 2. pp. 69−75.
- Ayewah N., Hovemeyer D., Morgenthaler J. D. et al. Using Static Analysis to Fing Bugs // IEEE Software. 2008. Vol. 25, no. 5. pp. 22−29.
- Ершов А. П. Проблемно-ориентированный язык программирования // Математическая энциклопедия. 1977−1985.
- Ахо А., Сети Р., Ульман Д. Компиляторы. Принципы, технологии, инструменты. Москва, СПб, Киев: «Вильяме», 2001. С. 768.
- Ахо А., Ульман Д. Теория синтаксического анализа, перевода и компиляции. Москва: «Мир», 1977.
- Карпов Ю. Г. Теория и технология программирования. Основы построения трансляторов. СПб: БХВ-Петербург, 2005. С. 272.
- Керниган Б.У., Ритчи Д. М. Язык программирования С. М.: «Вильяме», 2006. С. 304.
- Лавров С. С. Программирование. Математические основы, средства, теория. СПб: БХВ-Петербург, 2001. С. 314.
- Себеста Р. У. Основные концепции языков программирования. М.: «Вильяме», 2001. С. 672.
- Espresso. URL: http://embedded.eecs.berkeley.edu/pubs/downloads /espresso (дата обращения: 10.05.2011).
- DIMACS. URL: http://www.satalia.com/technology/cnf/ (дата обращения: 10.05.2011).
- Biere A. The AIGER And-Inverter Graph (AIG) Format Version 20 070 427 // Johannes Kepler University. 2007. URL: http://fmv.jku.at/aiger/ (дата обращения: 10.05.2011).
- Cook S., Mitchel D. G. Finding hard instances of the satisfiability problem: A survey // DIMACS Series in Discrete Mathematics and Theoretical Computer Science. 1997. Vol. 35. pp. 1−17.
- Заикин О. С., Семенов А. А. Технология крупноблочного параллелизма в SAT-задачах // Проблемы управления. 2008. № 1. С. 43−50.
- Посыпкин М.А., Заикин О. С., Беспалов Д. В., Семенов А. А. Решение задач криптоанализа поточных шифров в распределенных вычислительных средах // Труды ИСА РАН. 2009. Т. 46. С. 119−137.
- Rueppel R. A. Correlation immunity and the summation combiner // In Lecture Notes in Computer Science 218- Advances in Cryptology: Proc. Crypto'85, H. C. Williams Ed., Santa Barbara, CA, Aug. 18−22. 1985. Vol. 2. pp. 260−272.
- Gifford D.IC., Lucassen J.M., Berlin S.T. The Application of Digital Broadcast Communication to Large Scale Information Systems / / IEEE Journal on Selected Areas in Communications. 1985. Vol. 3, no. 3. pp. 457−467.
- Поточные шифры. Результаты зарубежной открытой криптологии. Москва: «Мир», 1997. С. 389.
- Cain T.R., Sherman А. Т. How to break Gifford’s Cipher // CRYPTOLOGIA. 1997. Vol. 21, no. 3. pp. 237−286.
- Biham E., Shamir A. Differential Cryptaanalysis of DES-like Cryptosystems // Advances in Cryptology- CRYPTO 90 Proceeding, Springer-Verlag. 1991. pp. 2−21.
- Guneysu Т., Kasper Т., Novotny M. et al. Cryptanalysis with COPACOBANA // IEEE Transactions on computers. 2008. Vol. 57, no. 11. pp. 1498−1513.
- Rivest L. R. The MD5 Message Digest Algorithm, RFC 1321. 1992. URL: http://rfc.com.ru/rfcl321.htm (дата обращения: 10.05.2011).
- Евдокимов А. А., Кочемазов C.E., Семенов А. А. Применение символьных вычислений к исследованию дискретных моделей некоторых классов генных сетей // Вычислительные технологии. 2011. Т. 16, № 1. С. 30−47.
- Евдокимов А. А., Лихошвай В. А., Комаров А. В. О восстановлении структуры дискретных моделей функционирования сетей / / Вестник Томского гос. ун-та. Приложение. 2005. Т. 14. С. 213−217.
- The International Pseudo-Boolean Competition. URL: http://www. cril. univ-artois.fr/PB10 (дата обращения: 10.05.2011).
- CPLEX Solver. URL: http://www.aimms.com/features/solvers/ cplex (дата обращения: 10.05.2011).
- MIPLIB Mixed Integer Problem Library. URL: http://miplib.zib.de (дата обращения: 10.05.2011).
- MiniSat+. URL: http://minisat.se/MiniSat+.html (дата обращения: 10.05.2011).