On Propositional Encoding of Distinction Property in Finite Sets
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: email@example.com
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: firstname.lastname@example.org
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
- 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)
- 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)
- 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
- Hall M. Combinatorics. Moscow, Mir Publ., 1970. 424 p.
- Tseitin G.S. About the complexity of the conclusion in the calculus of statements. Notes of scientiﬁc seminars LOMI, 1968, vol. 8., pp.234-259. (in Russian)
- CCU Irkutsk supercomputer SB RAS [Electronic resource]. URL: http://hpc.icc.ru (the date of handling: 04.28.2019).
- Chen C., Lee R. Mathematical logic and automatic proof of theorems. Moscow, Nauka Publ. 1983. 360 p. (in Russian)
- Yablonsky S.V. Introduction to discrete mathematics. Moscow, Nauka Publ. 1986. 384 p. (in Russian)
- 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
- Bard G.V. Algebraic Cryptanalysis. Springer Publishing Company, Incorporated, 2009. https://doi.org/10.1007/978-0-387-88757-9
- 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.
- 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.
- Biere A. Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. Proc. of SAT Competition 2016, pp. 44–45.
- 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.
- 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.
- Colbourn C.J., Dinitz J.H. Handbook of combinatorial designs. CRC Press. 2010. http://doi.org/10.1201/9781420010541
- Cook S.A. The complexity of theorem-proving procedures. Third annual ACM symposium on Theory of computing, 1971, Ohio, USA. pp. 151-159.
- DIMACS Implementation Challenges [Electronic resource]. URL: http://dimacs.rutgers.edu/Challenges/
- 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
- Haken A. The intractability or resolution. Theoretical Computer Science, 1985, vol. 39. pp. 297–308.
- 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.
- 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
- Lam C.W.H. The Search for a Finite Projective Plane of Order 10. The American Mathematical Monthly. 1991. pp. 305-318.
- 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
- 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
- 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
- Semenov A., Zaikin O., Otpuschennikov I., Kochemazov S., Ignatiev A. On cryptographic attacks using backdoors for SAT. In The Thirty-Second AAAI Conference on Artiﬁcial Intelligence, AAAI’2018, 2018, pp. 6641-6648.
- 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.
- 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
- 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.