In the paper we describe a new propositional encoding procedure for the property that all objects comprising some finite set are distinct. For the considered class of combinatorial problems it is sufficient to represent the elements of such set by their natural numbers. Thus, there is a problem of constructing a satisfiable Boolean formula, the satisfying assignments of which encode the first n natural numbers without taking into account their order. The necessity to encode such sets into Boolean logic is motivated by the desire to apply to the corresponding combinatorial problems the state-of-the-art algorithms for solving the Boolean satisfiability problem (SAT). In the paper we propose the new approach to defining the Boolean formula for the characteristic function of the predicate which takes the value of True only on the sets of binary words encoding the numbers from 0 to n − 1. The corresponding predicate was named OtO (from One-to-One). The propositional encoding of the OtO-predicate has a better lower bound compared to the propositional encoding of a relatively similar predicate known as OOC-predicate (from Only One Cardinality). The proposed OtO-predicate is used to reduce to SAT a number of problems related to Latin squares. In particular, using the OtO-predicate we constructed the SAT encodings for the problems of finding orthogonal pairs and quasi-orthogonal triples of Latin squares of order 10. We used the multi-threaded SAT solvers and the resources of a computing cluster to solve these problems.

Evgenia Beley, Master Student, Irkutsk National Research Technical University, 83, Lermontov st., Irkutsk, 664074, Russian Federation; tel.: (908)6684039, e-mail: zhenyha28@mail.ru

Alexander Semenov, PhD (Technical Sciences), head of laboratory, Matrosov Institute for System Dynamics and Control Theory SB RAS, 134, Lermontov st., Irkutsk, 664033, Russian Federation; tel.: (914)8707647, e-mail: biclop.rambler@yandex.ru

Beley E.G., Semenov A.A. On Propositional Encoding of Distinction Property in Finite Sets. The Bulletin of Irkutsk State University. Series Mathematics, 2019, vol. 28, pp. 3-20. (in Russian) https://doi.org/10.26516/1997-7670.2019.28.3

1. Beley E.G., Semenov A.A. On computational search for quasi-orthogonal systems of Latin squares which are close to orthogonal system. International Journal of Open Information Technologies, 2018, vol. 6, no. 2, pp. 22-30. (in Russian)
2. Semenov A.A. Decomposition representations of logical equations in inversion problems of discrete functions. News of the Russian Academy of Sciences, 2009, no. 5, pp. 47-61. (in Russian)
3. Taranenko A.A. Permanents of multidimensional matrices: Properties and applications. Journal of Applied and Industrial Mathematics, 2016, vol. 10, no. 4, pp. 567-604. https://doi.org/10.1134/S1990478916040141
4. Hall M. Combinatorics. Moscow, Mir Publ., 1970. 424 p.
5. Tseitin G.S. About the complexity of the conclusion in the calculus of statements. Notes of scientific seminars LOMI, 1968, vol. 8., pp.234-259. (in Russian)
6. CCU Irkutsk supercomputer SB RAS [Electronic resource]. URL: http://hpc.icc.ru (the date of handling: 04.28.2019).
7. Chen C., Lee R. Mathematical logic and automatic proof of theorems. Moscow, Nauka Publ. 1983. 360 p. (in Russian)
8. Yablonsky S.V. Introduction to discrete mathematics. Moscow, Nauka Publ. 1986. 384 p. (in Russian)
9. Asin R., Nieuwenhuis R., Oliveras A., Rodriguez-Carbonell E. Cardinality networks: a theoretical and empirical study. Constraints, vol. 16, Iss. 2011, pp. 195–221. https://doi.org/10.1007/s10601-010-9105-0
10. Bard G.V. Algebraic Cryptanalysis. Springer Publishing Company, Incorporated, 2009. https://doi.org/10.1007/978-0-387-88757-9
11. Beame P., Kautz H., Sabharwal A. Understanding the power of clause learning. Proceedings of the 18th International Joint Conference on Artificial Intelligence, 2003, pp. 1194-1201.
12. Bessiere C., Katsirelos G., Narodytska N., Walsh T. Circuit complexity and decompositions of global constraints. Proceedings of the 21st International Joint Conference on Artificial Intelligence, 2009, pp. 412-418.
13. Biere A. Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. Proc. of SAT Competition 2016, pp. 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. no. 4, pp. 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, pp. 189-203.
16. Colbourn C.J., Dinitz J.H. Handbook of combinatorial designs. 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. pp. 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, pp. 799–824. https://doi.org/10.1090/mcom/3010
20. Haken A. The intractability or resolution. Theoretical Computer Science, 1985, vol. 39. pp. 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), pp. 228-245.
22. Konev B., Lisitsa A. A SAT Attack on Erdos Discrepancy Problem. Lecture Notes in Computer Science, 2014, vol. 8561 (SAT-2014), pp. 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. pp. 305-318.
24. Marques-Silva J. P., Lynce I., Malik S. Conflict-Driven Clause Learning SAT solvers. Handbook of Satisfiability, 2009, pp. 131–153. https://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, pp. 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, pp. 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, 2018, pp. 6641-6648.
28. Vatutin E., Kochemazov S., Zaikin O., Valyaev S. Enumerating the Transversals for Diagonal Latin Squares of Small Order. Ceur-WS, 2017, vol. 1973, pp. 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, pp. 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. Proceedings of the 18th International Joint Conference on Articial Intelligence - IJCAI 2003, 2003, pp. 1173-1178.