On propositional encoding of distinction property in finite sets

E. G. Beley ; A. A. Semenov

The Bulletin of Irkutsk State University. Series Mathematics, Tome 28 (2019), pp. 3-20

Résumé

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.

Détail

Keywords: propositional encoding, SAT, latin squares.

Bibliographie

[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, 6:2 (2018), 22–30 (in Russian) | MR

[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, 47–61 (in Russian) | Zbl

[3] Taranenko A. A., “Permanents of multidimensional matrices: Properties and applications”, Journal of Applied and Industrial Mathematics, 10:4 (2016), 567–604 | DOI | DOI | MR | Zbl

[4] Hall M., Combinatorics, Mir Publ, M., 1970, 424 pp. | MR

[5] Tseitin G. S., “About the complexity of the conclusion in the calculus of statements”, Notes of scientific seminars LOMI, 8, 1968, 234–259 (in Russian) | MR | Zbl

[6] CCU Irkutsk supercomputer SB RAS (the date of handling: 04.28.2019)

[7] Chen C., Lee R., Mathematical logic and automatic proof of theorems, Nauka Publ., M., 1983, 360 pp. (in Russian)

[8] Yablonsky S. V., Introduction to discrete mathematics, Nauka Publ., M., 1986, 384 pp. (in Russian) | MR

[9] Asin R., Nieuwenhuis R., Oliveras A., Rodriguez-Carbonell E., “Cardinality networks: a theoretical and empirical study”, Constraints, 16:2 (2011), 195–221 | DOI | MR | Zbl

[10] Bard G. V., Algebraic Cryptanalysis, last Edition, Springer Publishing Company, Incorporated, 2009 | DOI | MR | Zbl

[11] Beame P., Kautz H., Sabharwal A., “Understanding the power of clause learning”, IJCAI (18th International Joint Conference on Artificial Intelligence) (2003), 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, IJCAI 2009, 2009, 412–418

[13] Biere A., “Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016”, Proc. of SAT Competition, eds. Balyo T., Heule M., Jarvisalo M., 2016, 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, 3 (1938), 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, 189–203 | DOI | MR | Zbl

[16] Colbourn C. J., Dinitz J. H., Handbook of combinatorial designs, Second edition, CRC Press, 2010 | DOI | MR

[17] Cook S. A., “The complexity of theorem-proving procedures”, Third annual ACM symposium on Theory of computing (Ohio, USA, 1971), 151–159

[18] DIMACS Implementation Challenges, http://dimacs.rutgers.edu/Challenges/

[19] Egan J., Wanless I. M., “Enumeration of MOLS of small order”, Math. Comput., 85 (2016), 799–824 | DOI | MR | Zbl

[20] Haken A., “The intractability or resolution”, Theoretical Computer Science, 39 (1985), 297–308 | DOI | MR

[21] Heule M. J. H., Kullman O., Marec V. W., “Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer”, SAT-2016, Lecture Notes in Computer Science, 9710, 2014, 228–245 | DOI | MR

[22] Konev B., Lisitsa A., “A SAT Attack on Erdos Discrepancy Problem”, SAT-2014, Lecture Notes in Computer Science, 8561, 2014, 219–226 | DOI | MR | Zbl

[23] Lam C. W. H., “The Search for a Finite Projective Plane of Order 10”, The American Mathematical Monthly, 1991, 305–318 | DOI | MR | Zbl

[24] Marques-Silva J. P., Lynce I., Malik S., “Conflict-Driven Clause Learning SAT solvers”, Handbook of Satisfiability, eds. Biere A., Heule M., van Maaren H., Walsh T., 2009, 131–153 | DOI

[25] McKay B. D., Wanless I. M., “A census of small Latin hypercubes”, SIAM J. Discrete Math., 22 (2008), 719–736 | DOI | MR | Zbl

[26] Mironov I., Zhang L., “Applications of SAT solvers to cryptanalysis of hash functions”, Lecture Notes in Computer Science, 4121, 2006, 102–115 | DOI | MR | Zbl

[27] Semenov A., Zaikin O., Otpuschennikov I., Kochemazov S., Ignatiev A., “On cryptographic attacks using backdoors for SAT”, The Thirty-Second AAAI Conference on Artificial Intelligence, AAAI'2018, 2018, 6641–6648

[28] Vatutin E., Kochemazov S., Zaikin O., Valyaev S., “Enumerating the Transversals for Diagonal Latin Squares of Small Order”, BOINC:FAST 2017, Ceur-WS, 1973, 2017, 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, 753 (2017), 114–129 | DOI

[30] Williams R., Gomes C. P., Selman B., “Backdoors to typical case complexity”, 18th International Joint Conference on Articial Intelligence – IJCAI 2003, 1173–1178