В статье описана новая процедура пропозиционального кодирования свойства различимости объектов, составляющих некоторое конечное множество. Для изучаемого в настоящей работе класса комбинаторных проблем достаточно представлять элементы рассматриваемого множества их натуральными номерами. Соответственно, возникает задача построения выполнимой булевой формулы, выполняющие наборы которой кодируют первые n целых неотрицательных чисел без учета их порядка. Необходимость булевого кодирования таких множеств вызвана желанием применить к соответствующим комбинаторным задачам алгоритмы решения проблемы булевой выполнимости (SAT). В статье предлагается новый способ задания булевой формулой характеристической функции предиката, который истин на наборе двоичных слов, представляющих числа от 0 до n − 1. Соответствующий предикат назван OtO (сокращение от One-to-One). Пропозициональная кодировка OtO-предиката имеет более экономную асимптотику роста в сравнении с кодировкой для близкого по смыслу предиката, известного как OOC-предикат (от Only One Cardinality). Описанный в статье OtO-предикат используется для сведения к SAT ряда задач, связанных с латинскими квадратами. Конкретно, с помощью OtO-предиката строятся SAT-кодировки для задач поиска ортогональных пар и квазиортогональных троек латинских квадратов порядка 10. Для вычислительного решения этих задач используются многопоточный SAT-решатель и вычислительный кластер.

Белей Евгения Геннадьевна, магистрант, Иркутский национальный исследовательский технический университет, Российская Федерация, 664074, Иркутск, Лермонтова, 83; тел.: (908)6684039, e-mail: zhenyha28@mail.ru

Семенов Александр Анатольевич, к.т.н., доцент, зав. лабораторией, Институт динамики систем и теории управления им. В.М. Матросова СО РАН, Российская Федерация, 664033, Иркутск, ул. Лермонтова, 134; тел.: (914)8707647, e-mail: biclop.rambler@yandex.ru

Белей Е.Г., Семенов А.А. О способах пропозиционального кодирования различимости объектов в конечных множествах // Известия Иркутского государственного университета. Серия Математика. 2019. Т. 28. С. 3-20. https://doi.org/10.26516/1997-7670.2019.28.3

1. Белей Е. Г., Семенов А. А. О вычислительном поиске квазиортогональных систем латинских квадратов, близких к ортогональным системам // International Journal of Open Information Technologies. 2018. Vol. 6, N 2, P. 22-30.
2. Семенов А. А. Декомпозиционные представления логических уравнений в задачах обращения дискретных функций // Изв. РАН. 2009. № 5. С. 47–61.
3. Тараненко А. А. Перманенты многомерных матриц: свойства и приложения // Дискретный анализ и исследование операций. 2016. Т. 23, № 4. С. 35-101. https://doi.org/10.17377/daio.2016.23.517
4. Холл М. Комбинаторика. M. : Мир, 1970. 424 c.
5. Цейтин Г.С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ. 1968. Т. 8. С. 234–259.
6. ЦКП Иркутский суперкомпьютерный СО РАН [Электронный ресурс]. http://hpc.icc.ru (дата обращения: 28.04.2019).
7. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М. : Наука, 1983. 360 с.
8. Яблонский С. В. Введение в дискретную математику. М. : Наука, 1986. 384 с.
9. Asin R., Nieuwenhuis R., Oliveras A., Rodriguez-Carbonell E. Cardinality networks: a theoretical and empirical study // Constraints. Vol. 16. Iss. 2011. P. 195–221. https://doi.org/10.1007/s10601-010-9105-0
10. Bard G. V. Algebraic Cryptanalysis. Springer Publishing Company, Incorporated, last Edition, 2009. https://doi.org/10.1007/978-0-387-88757-9
11. Beame P., Kautz H., Sabharwal A. Understanding the power of clause learning // IJCAI (18th International Joint Conference on Artificial Intelligence). 2003. P. 1194–1201.
12. Bessiere C., Katsirelos G., Narodytska N., Walsh T. Circuit complexity and decompositions of global constraints. In IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence. 2009. P. 412–418.
13. Biere A. Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016 // Proc. of SAT Competition / Balyo T., Heule M., Jarvisalo M. (eds.). 2016. P. 44–45.
14. Bose R. C. On the application of the properties of Galois fields to the problem of construction of hyper-Graeco-Latin squares // Sankhya. 1938. Vol. 3. P. 323–338.
15. Bose R. C., Shrikhande S. S., Parker E. T. Further results on the construction of mutually orthogonal Latin squares and the falsity of Euler’s conjecture // Canadian Journal of Mathematics. 1960. P. 189-203.
16. Colbourn C. J., Dinitz J. H. Handbook of combinatorial designs. Second edition. CRC Press, 2010. http://doi.org/10.1201/9781420010541
17. Cook S. A. The complexity of theorem-proving procedures // Third annual ACM symposium on Theory of computing, 1971, Ohio, USA. P. 151–159.
18. DIMACS Implementation Challenges [Electronic resource]. URL: http://dimacs.rutgers.edu/Challenges/
19. Egan J., Wanless I. M., Enumeration of MOLS of small order // Math. Comput. 2016. Vol. 85. P. 799–824. https://doi.org/10.1090/mcom/3010
20. Haken A. The intractability or resolution // Theoretical Computer Science. 1985. Vol. 39. P. 297–308.
21. Heule M. J. H., Kullman O., Marec V. W. Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer // Lecture Notes in Computer Science. 2014. Vol. 9710 (SAT-2016). P. 228–245.
22. Konev B., Lisitsa A. A SAT Attack on Erdos Discrepancy  Problem  // Lecture Notes in Computer Science. 2014. Vol. 8561 (SAT-2014). P. 219–226. https://doi.org/10.1007/978-3-319-09284-3_17
23. Lam C.W.H. The Search for a Finite Projective Plane of Order 10. The American Mathematical Monthly. 1991. P. 305-318.
24. Marques-Silva J. P., Lynce I., Malik S. Conflict-Driven Clause Learning SAT solvers // Handbook of Satisfiability / Biere A., Heule M., van Maaren H., Walsh T. (eds.). 2009. P. 131–153. https://www.doi.org/10.3233/978-1-58603-929-5-131
25. McKay B. D., Wanless I. M. A census of small Latin hypercubes // SIAM J. Discrete Math. 2008. Vol. 22. P. 719–736. https://doi.org/10.1137/070693874
26. Mironov I., Zhang L. Applications of SAT solvers to cryptanalysis of hash functions // Lecture Notes in Computer Science. 2006. Vol. 4121. P. 102-115. https://doi.org/10.1007/11814948_13
27. Semenov A., Zaikin O., Otpuschennikov I., Kochemazov S., Ignatiev A. On cryptographic attacks using backdoors for SAT. In The Thirty-Second AAAI Conference on Artificial Intelligence, AAAI’2018, pages 6641-6648, 2018.
28. Vatutin E., Kochemazov S., Zaikin O., Valyaev S. Enumerating the Transversals for Diagonal Latin Squares of Small Order // Ceur-WS. 2017. Vol. 1973 (BOINC:FAST 2017). P. 6–14.
29. Vatutin E., Kochemazov S., Zaikin O. Applying Volunteer and Parallel Computing for Enumerating Diagonal Latin Squares of Order 9 // Communication in Computer and Information Science. 2017. Vol. 753. P. 114–129. https://doi.org/10.1007/978-3-319-67035-5_9
30. Williams R., Gomes C. P., Selman B. Backdoors to typical case complexity // In 18th International Joint Conference on Articial Intelligence - IJCAI 2003. 2003. P. 1173-1178.