zbMATH — the first resource for mathematics

On propositional coding techniques for the distinguishability of objects in finite sets. (Russian. English summary) Zbl 1425.94047
Summary: 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.
94A60 Cryptography
94C10 Switching theory, application of Boolean algebra; Boolean functions (MSC2010)
05B15 Orthogonal arrays, Latin squares, Room squares
68R05 Combinatorics in computer science
Full Text: DOI Link
[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, 2, 22-30, (2018)
[2] Semenov, A. A., Decomposition representations of logical equations in inversion problems of discrete functions, News of the Russian Academy of Sciences, 5, 47-61, (2009)
[3] Taranenko, A. A., Permanents of multidimensional matrices: Properties and applications, Journal of Applied and Industrial Mathematics, 4, 567-604, (2016) · Zbl 1374.05024
[4] Hall, M., Combinatorics, 424, (1970)
[5] Tseitin, G. S., About the complexity of the conclusion in the calculus of statements, Notes of scientific seminars LOMI, 234-259, (1968) · Zbl 0197.00102
[6] CU Irkutsk supercomputer SB RAS [Electronic resource], http://hpc.icc.ru (the date of handling: 04.28.2019), (2019)
[7] Chen, C.; Lee, R., Mathematical logic and automatic proof of theorems, 360, (1983)
[8] Yablonsky, S. V., Introduction to discrete mathematics, 384, (1986)
[9] Asin, R.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez-Carbonell, E., Cardinality networks: a theoretical and empirical study, Constraints, 195-221, (2011) · Zbl 1217.68200
[10] Bard, G. V., Algebraic Cryptanalysis, (2009), Springer Publishing Company, Incorporated · Zbl 1183.94019
[11] Beame, P.; Kautz, H.; Sabharwal, A., Understanding the power of clause learning, Proceedings of the 18th International Joint Conference on Artificial Intelligence, 1194-1201, (2003)
[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, 412-418, (2009)
[13] Biere, A., Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016, Proc. of SAT Competition, 44-45, (2016)
[14] Bose, R. C., On the application of the properties of Galois fields to the problem of construction of hyper-Graeco-Latin squares, Sankhya, 4, 323-338, (1938)
[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, 189-203, (1960) · Zbl 0093.31905
[16] Colbourn, C. J.; Dinitz, J. H., Handbook of combinatorial designs, (2010), CRC Press
[17] Cook, S. A., The complexity of theorem-proving procedures, Third annual ACM symposium on Theory of computing, 151-159, (1971)
[18] IMACS Implementation Challenges [Electronic resource], URL: http://dimacs.rutgers.edu/Challenges/
[19] Egan, J.; Wanless, I. M., Enumeration of MOLS of small order, Math. Comput, 799-824, (2016) · Zbl 1332.05025
[20] Haken, A., The intractability or resolution, Theoretical Computer Science, 297-308, (1985) · Zbl 0586.03010
[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, 228-245, (2014)
[22] Konev, B.; Lisitsa, A., A SAT Attack on Erdos Discrepancy Problem, Lecture Notes in Computer Science, 219-226, (2014) · Zbl 1343.68217
[23] Lam, C. W.H., The Search for a Finite Projective Plane of Order 10, The American Mathematical Monthly, 305-318, (1991) · Zbl 0744.51011
[24] Marques-Silva, J. P.; Lynce, I.; Malik, S., Conflict-Driven Clause Learning SAT solvers, Handbook of Satisfiability, 131-153, (2009)
[25] McKay, B. D.; Wanless, I. M., A census of small Latin hypercubes, SIAM J. Discrete Math., 719-736, (2008) · Zbl 1167.05302
[26] Mironov, I.; Zhang, L., Applications of SAT solvers to cryptanalysis of hash functions, Lecture Notes in Computer Science, 102-115, (2006) · Zbl 1187.94028
[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, 6641-6648, (2018)
[28] Vatutin, E.; Kochemazov, S.; Zaikin, O.; Valyaev, S., Enumerating the Transversals for Diagonal Latin Squares of Small Order, Ceur-WS, 6-14, (2017)
[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, 114-129, (2017)
[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, 1173-1178, (2003)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.