On computational search for quasi-orthogonal systems of Latin squares which are close to orthogonal systems.

Evgenia Beley, Alexandr Semenov

Abstract


In the paper we study the applicability of modern algorithms of computational logic to problems of finding some combinatorial designs. In particular, we consider the well-known open problem – to answer whether there exist three mutually orthogonal Latin squares of order 10. We propose an iterative procedure to search for such a triple. At each iteration, it constructs the so-called quasi–orthogonal systems. We use the orthogonality index metric that makes it possible to measure how close is the quasi–orthogonal system to the orthogonal one. To construct quasi-orthogonal systems with specified orthogonality index we employ the state-of-the-art algorithms for solving Boolean satisfiability problem (SAT). The results of our computational experiments show that the SAT-solvers can successfully be used to search for new combinatorial designs based on Latin squares.

Full Text:

PDF (Russian)

References


Kostrikin A.I. Vvedenie v algebru. M.: «Nauka». 1977. 495 S.

Holl M. Kombinatorika. M.: «Mir». 1970. 425 S.

Colbourn C.J., Dinitz J.H. Handbook of Combinatorial Designs. Second Edition. Chapman&Hall, 2006. 984 p.

Lin, Keh Ying (2004), "Number Of Sudokus", Journal of Recreational Mathematics, 33 (2): 120–124.

Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

Mironov I., Zhang L. Applications of SAT solvers to cryptanalysis of hash functions // Lecture Notes in Computer Science. 2006. Vol. 4121, pp. 102–115.

Semenov. A., Zaikin. O., Bespalov. D., Posypkin. M.: Parallel logical cryptanalysis of the generator A5/1 in BNB-grid system // Lecture Notes in Computer Science. 2011. Vol. 6873, pp. 473–483.

Lynce I. Ouaknine J. Sudoku as a sat problem. In 9th International Symposium on Artificial Intelligence and Mathematics, 2006.

Zhang H. Combinatorial Design by SAT Solvers. In [6], Chapter 17. Pp. 533- 568.

Zaikin, O., Kochemazov, S., Semenov, A.: SAT-based search for systems of diagonal latin squares in volunteer computing project sat@home // In Proc. of MIPRO 2016, Opatija, Croatia, May 30 - June 3, 2016. pp. 277–281.

Zaikin, O., Zhuravlev, A., Kochemazov, S., Vatutin, E. On the construction of triples of diagonal Latin squares of order 10 // Electronic Notes in Discrete Mathematics. 2016. Vol. 54. pp. 307–312.

Zaikin, O., Kochemazov, S. The Search for Systems of Diagonal Latin Squares Using the SAT@home Project // International Journal of Open Information Technologies. 2015. Vol. 3. No. 11. pp. 4-9.

Egan J., Wanless I. Enumeration of MOLS of Small Order// Mathematics of Computation. 2016. Vol. 85. N 298. 799-824

Cook S.A. The complexity of theorem-proving procedures // Third annual ACM symposium on Theory of computing, 1971, Ohio, USA. ACM. 1971. P. 151-159.

Gjeri M., Dzhonson D. Vychislitel'nye mashiny i trudnoreshaemye zadachi. M.: «Mir». 1982. 416 S.

Selman B., Kautz H., Cohen B. Noise strategies for local search. In Proc. of AAAI-94, pp. 337-343. AAAI Press/The MIT Press, 1994.

Schoning U. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In 40th FOCS, pages 410–414, New York, NY, October 1999. IEEE.

Hirsch E., Kojevnikov A. UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. Annals Math. and AI, 43(1):91-111, 2005.

Kautz H., Sabharwal A., Selman B. Incomplete Algorithms. In [6], Chapter 6. Pp. 185-203.

Marques-Silva J.P., Sakallah K.A. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506–521, 1999.

Marques-Silva J.P., Lynce I., Malik S. Conflict-Driven Clause Learning SAT solvers. In [6], Chapter 4. Pp. 131–153.

Steffen Hölldobler and Van Hau Nguyen. An Efficient Encoding of the At-Most-One Constraint.//Tech. rep. 2013-04, Technische Universität Dresden, Germany, 2013.

Kochemazov S.E., Semenov A.A. O razlichnyh podhodah k bulevomu kodirovaniju zadach poiska sistem ortogonal'nyh latinskih kvadratov // Trudy XVIII konferencii «Informacionnye i matematicheskie tehnologii v nauke i upravlenii». Irkutsk. 2013. T.3. S. 40–44.

Asin R, Nieuwenhuis R, Oliveras A, Rodriguez-Carbonell E (2011) Cardinality networks: a theoretical and empirical study. Constraints 16:195–221.

Sinz C. Towards an Optimal Encoding of Boolean Cardinality Constraints // Lecture Notes in Computer Science. 2005. Vol. 3709. Pp. 827-831.

Cejtin G.S. O slozhnosti vyvoda v ischislenii vyskazyvanij // Zapiski nauchnyh seminarov LOMI AN SSSR. 1968. T.8. C. 234–259.

Shaowei Cai, Chuan Luo, Kaile Su: Scoring Functions Based on Second Level Score for k-SAT with Long Clauses // J. Artif. Intell. Res. 51, pp. 413-441 (2014)

Shaowei Cai, Kaile Su: Local search for Boolean Satisfiability with configuration checking and subscore // Artif. Intell. 204, pp. 75-98 (2013)

Biere, A.: Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In: Balyo, T., Heule, M., Jarvisalo, M. (eds.) Proc. of SAT Competition 2016. Dep. of Compju Sci. Series of Publications B, vol. B-2016-1, pp. 44–45. University of Helsinki (2016)

Soos, M., Nohl, K., Castelluccia, C.: Extending SAT Solvers to Cryptographic Problems. In: Kullmann, O. (ed.) SAT. Lecture Notes in Computer Science, vol. 5584, pp. 244–257. Springer (2009)

Posypkin M.A., Zaikin O.S., Bespalov D.V., Semenov A.A. Reshenie zadach kriptoanaliza potochnyh shifrov v raspredelennyh vychislitel'nyh sredah // Trudy Instituta sistemnogo analiza Rossijskoj akademii nauk. 2009. T. 46. S. 119-137.

Posypkin M., Semenov A., Zaikin O. Using BOINC desktop grid to solve large scale SAT problems // Computer Science (AGH). 2012. Vol. 13. pp 25-34.

Zaikin O.S., Posypkin M.A., Semenov A.A., Hrapov N.P. Opyt organizacii dobrovol'nyh vychislenij na primere proektov OPTIMA@home i SAT@home // Vestnik Nizhegorodskogo universiteta im. N.I. Lobachevskogo. 2012. # 5-2. S. 340-347.

Zaikin O. S., Semenov A. A., Posypkin M. A. Procedury postroenija dekompozicionnyh mnozhestv dlja raspredelennogo reshenija SAT-zadach v proekte dobrovol'nyh vychislenij SAT@home // Upravlenie bol'shimi sistemami: sbornik trudov. 2013. #. 43. S. 138-156.


Refbacks

  • There are currently no refbacks.


Abava   IEEE FRUCT 2018

ISSN: 2307-8162