zbMATH — the first resource for mathematics

Investigating the existence of large sets of idempotent quasigroups via satisfiability testing. (English) Zbl 06958110
Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer (ISBN 978-3-319-94204-9/pbk; 978-3-319-94205-6/ebook). Lecture Notes in Computer Science 10900. Lecture Notes in Artificial Intelligence, 354-369 (2018).
Summary: In this paper, we describe a method for solving some open problems in design theory based on SAT solvers. Modern SAT solvers are efficient and can produce unsatisfiability proofs. However, the state-of-the-art SAT solvers cannot solve the so-called Large Set problem of idempotent quasigroups. Two idempotent quasigroups over the same set of elements are said to be disjoint if at any position other than the main diagonal, the two elements from the two idempotent quasigroups at the same position are different. A collection of \(n-2\) idempotent quasigroups of order \(n\) is called a large set if all idempotent quasigroups are mutually disjoint, denoted by \(LIQ(n)\). The existence of \(LIQ(n)\) satisfying certain identities has been a challenge for modern SAT solvers even if \(n=9\). We will use a finite-model generator to help the SAT solver avoiding symmetric search spaces, and take advantages of both first order logic and the SAT techniques. Furthermore, we use an incremental search strategy to find a maximum number of disjoint idempotent quasigroups, thus deciding the non-existence of large sets. The experimental results show that our method is highly efficient. The use of symmetry breaking is crucial to allow us to solve some instances in reasonable time.
For the entire collection see [Zbl 1391.68006].
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI