pith. machine review for the scientific record. sign in

arxiv: 2605.02132 · v1 · submitted 2026-05-04 · 💻 cs.DM · math.CO

Recognition: unknown

Improving SAT Solvers on Orthogonal Latin Square Problems

Aaron Barnoff, Curtis Bright

Pith reviewed 2026-05-08 01:38 UTC · model grok-4.3

classification 💻 cs.DM math.CO
keywords orthogonal Latin squaresSAT solversEuler-Parker algorithmhybrid algorithmscombinatorial search10x10 Latin squaresDiophantine systemsCaDiCaL
0
0 comments X

The pith

Augmenting CaDiCaL with the Euler-Parker algorithm solves the hardest 10x10 orthogonal Latin square cases in a median of 5100 seconds.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to demonstrate that general SAT solvers can be strengthened on orthogonal Latin square problems by calling an external Euler-Parker algorithm during search. This matters because standard SAT encodings lack built-in knowledge of Latin square structure, such as efficient ways to construct orthogonal mates, and the hybrid method turns that gap into a practical advantage. A sympathetic reader would note that the approach resolves instances whose existence remained open for decades by letting the solver hand off subproblems to a Diophantine solver that implements the Euler-Parker technique. The reported outcome is that previously intractable 10x10 pairs become solvable where the plain solver times out after seven days.

Core claim

CaDiCaL augmented with an external Euler-Parker algorithm solves the hardest 10x10 orthogonal Latin square instances in a median of around 5100 seconds, whereas the unaugmented solver could not solve them within seven days. The method works by invoking the Euler-Parker construction, realized through a Diophantine system solver, at appropriate points in the SAT search to generate or prune orthogonal mate candidates.

What carries the argument

The Euler-Parker algorithm for constructing orthogonal mates, implemented as a Diophantine equation solver that is invoked externally from within the SAT search.

If this is right

  • Pairs of 10x10 orthogonal Latin squares whose existence was unknown for over 25 years become computationally reachable.
  • The hybrid solver achieves orders-of-magnitude reductions in runtime on the most difficult cases compared with the unaugmented version.
  • The same integration pattern can be applied to other orthogonal Latin square problems of varying orders and types.
  • SAT solvers can usefully incorporate domain-specific combinatorial routines without losing their general-purpose character.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same hybrid pattern may transfer to other combinatorial search problems that possess efficient specialized algorithms, such as certain design-theoretic or scheduling instances.
  • Embedding the Diophantine solver more tightly inside the SAT engine rather than calling it externally could further reduce overhead.
  • The reported speedups suggest that partial domain knowledge can be added modularly to existing solvers, offering a scalable route for other long-standing open problems in combinatorics.

Load-bearing premise

Calling the Euler-Parker algorithm from inside the SAT search can be arranged so that the added overhead and any compatibility friction do not erase the observed speedups on the target 10x10 instances.

What would settle it

Running the same hardest 10x10 instances with the augmented solver and finding that the median time exceeds seven days or that the plain CaDiCaL finishes faster.

Figures

Figures reproduced from arXiv: 2605.02132 by Aaron Barnoff, Curtis Bright.

Figure 1
Figure 1. Figure 1: (a) A Latin square of order 5 decomposed into 5 non-overlapping transversals, with each transversal highlighted in a separate colour. (b) The orthogonal mate of the square in (a) produced by labelling the cells of each colour with a distinct symbol. (c) The original square and orthogonal mate overlaid, showing that every pair of symbols appears exactly once. be decomposed into 𝑛 disjoint (i.e., non-overlap… view at source ↗
Figure 2
Figure 2. Figure 2: A type-UW transversal representation pair, with white, light, and dark colouring. Each row of each square represents a transversal of the other square. For example, consider the first row of the first square [0, 2, 3, 4, . . . ]. Going through the second square column-by-column and extracting the cell from each column containing these symbols in sequence yields the cells (0, 0), (6, 1), (5, 2), (1, 3), . .… view at source ↗
Figure 3
Figure 3. Figure 3: Scatterplot comparing the hybrid approach (left) to the pure SAT approach (right), for the eight Myrvold pair types. The median time is indicated with a black bar. being passed to Euler–Parker between clause database reductions, and this substantially reduced memory usage. The highest recorded memory usage by the hybrid solver was 0.99 GiB (after running for about 5 days). A breakdown of the median time sp… view at source ↗
read the original abstract

Latin squares are $n\times n$ matrices containing $n$ symbols, where each symbol appears exactly once in each row and column. They were studied by Euler, later popularized through Sudoku, and remain a rich source of difficult combinatorial search problems. Two Latin squares are orthogonal mates if, when overlaid, no ordered pair of symbols repeats. Pairs of orthogonal Latin squares exist for every order except 2 and 6, but finding orthogonal Latin squares computationally can be challenging. Satisfiability (SAT) solvers are strong at combinatorial search and have been used to resolve a number of various kinds of orthogonal Latin square problems. On the other hand, SAT solvers lack domain knowledge about Latin squares, such as the Euler-Parker algorithm for orthogonal mate construction. In this paper, we propose a hybrid method combining a SAT solver with the Euler-Parker algorithm (implemented using a Diophantine system solver) and show that the resulting solver is effective at finding certain kinds of orthogonal Latin squares. For example, certain pairs of $10\times10$ orthogonal Latin squares whose existence was unknown for over 25 years were recently found by Bright, Keita, and Stevens using a SAT solver. The hardest cases could not be solved by the SAT solver CaDiCaL within seven days, but CaDiCaL augmented with an external Euler-Parker algorithm solves these cases in a median of around 5,100 seconds.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper proposes augmenting the CaDiCaL SAT solver with an external Euler-Parker algorithm (implemented via a Diophantine system solver) to find pairs of orthogonal Latin squares. It reports that this hybrid approach solves the hardest known 10x10 instances—previously unsolved by unaugmented CaDiCaL within seven days—in a median runtime of approximately 5100 seconds.

Significance. If the integration details and overhead measurements hold, the work demonstrates a practical way to inject domain-specific Latin-square knowledge into general-purpose SAT solvers, yielding concrete speedups on long-standing hard instances. The empirical runtime comparisons against an external baseline provide direct evidence for the performance claim and could inform similar hybridizations for other combinatorial problems.

major comments (2)
  1. [Hybrid method description (near the end of the abstract and corresponding methods section)] The hybrid integration is described only at a high level (external Euler-Parker calls during search) without specifying invocation points inside CaDiCaL, the exact form of partial Latin-square assignments passed to the Diophantine solver, triggering conditions, or any instrumentation of the fraction of runtime spent outside the SAT engine. This information is load-bearing for the central speedup claim, as prohibitive overhead or state-conversion costs could erase the reported gains.
  2. [Experimental results and runtime tables] The experimental results report median runtimes but omit error bars, the number of independent runs per instance, full benchmark specifications (e.g., exact instance encodings, hardware details, or timeout handling), and any comparison of search-node counts or learned-clause statistics between the plain and augmented solvers. These omissions make it difficult to assess whether the improvement is robust or instance-specific.
minor comments (2)
  1. [Introduction / abstract] The abstract states that pairs of orthogonal Latin squares exist for every order except 2 and 6; a brief reference to the known non-existence proofs would improve context.
  2. [Euler-Parker algorithm subsection] Notation for the Diophantine encoding of the Euler-Parker algorithm should be introduced with a small example for a small order (e.g., order 4) to aid readers unfamiliar with the technique.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback. We address each major comment below and agree that expanding the description of the hybrid method and strengthening the experimental reporting will improve the manuscript.

read point-by-point responses

  1. Referee: The hybrid integration is described only at a high level (external Euler-Parker calls during search) without specifying invocation points inside CaDiCaL, the exact form of partial Latin-square assignments passed to the Diophantine solver, triggering conditions, or any instrumentation of the fraction of runtime spent outside the SAT engine. This information is load-bearing for the central speedup claim, as prohibitive overhead or state-conversion costs could erase the reported gains.

    Authors: We agree that the current description of the integration is high-level and that additional specifics are needed to fully support the speedup claims. In the revised manuscript we will expand the methods section to detail the exact points at which external Euler-Parker calls are invoked inside CaDiCaL, the precise format of the partial Latin-square assignments passed to the Diophantine solver, the triggering conditions used, and instrumentation results showing the fraction of runtime spent outside the SAT engine. These additions will demonstrate that the overhead is modest relative to the observed gains. revision: yes

  2. Referee: The experimental results report median runtimes but omit error bars, the number of independent runs per instance, full benchmark specifications (e.g., exact instance encodings, hardware details, or timeout handling), and any comparison of search-node counts or learned-clause statistics between the plain and augmented solvers. These omissions make it difficult to assess whether the improvement is robust or instance-specific.

    Authors: We acknowledge that the experimental section would benefit from greater statistical detail and additional solver metrics. In the revision we will include error bars derived from multiple independent runs, state the number of runs performed per instance, provide complete benchmark specifications (instance encodings, hardware platform, and timeout policy), and report comparisons of search-node counts and learned-clause statistics between plain CaDiCaL and the augmented solver. These changes will allow a clearer assessment of robustness. revision: yes

Circularity Check

0 steps flagged

No significant circularity in empirical runtime comparison

full rationale

The paper reports an experimental result: a hybrid SAT solver (CaDiCaL augmented with an external Euler-Parker/Diophantine algorithm) solves certain 10x10 orthogonal Latin square instances in a median of ~5100 seconds where the unaugmented solver times out after seven days. This is a direct benchmark measurement on fixed instances, not a derivation, fitted model, or theorem whose conclusion is forced by its own inputs. No equations, ansatzes, uniqueness theorems, or parameter fits are presented whose outputs reduce to the inputs by construction. Prior self-citations (e.g., Bright et al. on the original discovery) supply context for the benchmark instances but are not load-bearing for the runtime claim itself. The result is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on the established Euler-Parker algorithm and standard SAT solving techniques with no new free parameters or invented entities introduced.

axioms (1)
  • domain assumption The Euler-Parker algorithm can be implemented using a Diophantine system solver.
    Explicitly stated in the abstract as the chosen implementation approach for the hybrid component.

pith-pipeline@v0.9.0 · 5545 in / 1183 out tokens · 69773 ms · 2026-05-08T01:38:17.371961+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

55 extracted references · 32 canonical work pages

  1. [1]

    Euler, Recherches sur une nouvelle espèce de quarrés magiques, Verhandelingen uitgegeven door het zeeuwsch Genootschap der Wetenschappen te Vlissingen (1782) 85–239

    L. Euler, Recherches sur une nouvelle espèce de quarrés magiques, Verhandelingen uitgegeven door het zeeuwsch Genootschap der Wetenschappen te Vlissingen (1782) 85–239

  2. [2]

    Tarry, Le problème des 36 officiers, Association Française pour l’Avancement des Sciences: Compte Rendu de la 29me session, Paris 1900 2 (1901) 170–203

    G. Tarry, Le problème des 36 officiers, Association Française pour l’Avancement des Sciences: Compte Rendu de la 29me session, Paris 1900 2 (1901) 170–203

    1900

  3. [3]

    Peterson, Les 36 officieurs, Annuaire des Mathématiciens (1902) 413–427

    J. Peterson, Les 36 officieurs, Annuaire des Mathématiciens (1902) 413–427

    1902

  4. [4]

    Wernicke, Das problem der 36 offiziere, Jahresbericht der Deutschen Mathematiker-Vereinigung 19 (1910) 264–267

    P. Wernicke, Das problem der 36 offiziere, Jahresbericht der Deutschen Mathematiker-Vereinigung 19 (1910) 264–267

    1910

  5. [5]

    H. F. MacNeish, Euler squares, Annals of Mathematics 23 (1922) 221–227. doi: 10.2307/1967920

    work page doi:10.2307/1967920 1922

  6. [6]

    E. T. Parker, Orthogonal Latin squares, Proceedings of the National Academy of Sciences 45 (1959) 859–862. doi:10.1073/pnas.45.6.859

    work page doi:10.1073/pnas.45.6.859 1959

  7. [7]

    R. C. Bose, S. S. Shrikhande, On the construction of sets of mutually orthogonal Latin squares and the falsity of a conjecture of Euler, Transactions of the American Mathematical Society 95 (1960) 191–209. doi:10.2307/1993286

    work page doi:10.2307/1993286 1960

  8. [8]

    R. C. Bose, S. S. Shrikhande, E. T. Parker, Further results on the construction of mutually orthogonal Latin squares and the falsity of Euler’s conjecture, Canadian Journal of Mathematics 12 (1960) 189–203. doi:10.4153/CJM-1960-016-5

    work page doi:10.4153/cjm-1960-016-5 1960

  9. [9]

    L. J. Paige, C. B. Tompkins, The size of the10×10 orthogonal Latin square problem, Combinatorial Analysis (1960) 71–83. doi:10.1090/psapm/010/0115927

    work page doi:10.1090/psapm/010/0115927 1960

  10. [10]

    E. T. Parker, A computer search for Latin squares orthogonal to Latin squares of order ten, abstract 564-71, American Mathematical Society Notices 6 (1959) 798

    1959

  11. [11]

    D. E. Knuth, The Art of Computer Programming, Volume 4A: Combinatorial Algorithms, Part 1, Addison-Wesley, Upper Saddle River, NJ, 2011

    2011

  12. [12]

    Kochemazov, O

    S. Kochemazov, O. Zaikin, A. Semenov, The comparison of different SAT encodings for the problem of search for systems of orthogonal Latin squares, in: International Conference Mathematical and Information Technologies-MIT, volume 1839 ofCEUR Workshop Proceedings, 2016, pp. 155–165. URL: https://ceur-ws.org/Vol-1839/MIT2016-p14.pdf

    2016

  13. [13]

    G. Appa, D. Magos, I. Mourtos, Searching for mutually orthogonal Latin squares via integer and constraint programming, European Journal of Operational Research 173 (2006) 519–530. doi:10.1016/j.ejor.2005.01.048

    work page doi:10.1016/j.ejor.2005.01.048 2006

  14. [14]

    Rubin, C

    N. Rubin, C. Bright, K. Cheung, B. Stevens, Improving integer and constraint programming for Graeco-Latin squares, in: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI), IEEE, 2021, p. 604–608. doi:10.1109/ictai52525.2021.00096

    work page doi:10.1109/ictai52525.2021.00096 2021

  15. [16]

    B. D. McKay, A. Meynert, W. Myrvold, Small Latin squares, quasigroups, and loops, Journal of Combinatorial Designs 15 (2006) 98–119. doi:10.1002/jcd.20105

    work page doi:10.1002/jcd.20105 2006

  16. [17]

    Bright, A

    C. Bright, A. Keita, B. Stevens, Myrvold’s results on orthogonal triples of 10×10 Latin squares: A SAT investigation, The Electronic Journal of Combinatorics 33 (2026) P1.30. doi:10.37236/13960

    work page doi:10.37236/13960 2026

  17. [18]

    Myrvold, Negative results for orthogonal triples of Latin squares of or- der 10, Journal of Combinatorial Mathematics and Combinatorial Computing 29 (1999) 95–105

    W. Myrvold, Negative results for orthogonal triples of Latin squares of or- der 10, Journal of Combinatorial Mathematics and Combinatorial Computing 29 (1999) 95–105. URL: https://combinatorialpress.com/jcmcc-articles/volume-029/ negative-results-for-orthogonal-triples-of-Latin-squares-of-order-10/

    1999

  18. [19]

    Biere, T

    A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, F. Pollitt, CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024, in: M. Heule, M. Iser, M. Järvisalo, M. Suda (Eds.), Proc. of SAT Competition 2024 – Solver, Benchmark and Proof Checker Descriptions, volume B-2024-1 ofDepartment of Computer Science Report Series B, University of H...

    2024

  19. [20]

    In: Gurfinkel, A., Ganesh, V

    A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, F. Pollitt, CaDiCaL 2.0, in: A. Gurfinkel, V. Ganesh (Eds.), Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 ofLecture Notes in Computer Science, Springer, 2024, pp. 133–152. doi:10.1007/978-3-031-65627-9_7

    work page doi:10.1007/978-3-031-65627-9_7 2024

  20. [21]

    S. A. Cook, The complexity of theorem-proving procedures, in: Proceedings of the third annual ACM symposium on Theory of computing - STOC ’71, STOC ’71, ACM Press, 1971, p. 151–158. doi:10.1145/800157.805047

    work page doi:10.1145/800157.805047 1971

  21. [22]

    Ganesh, M

    V. Ganesh, M. Y. Vardi, On the Unreasonable Effectiveness of SAT Solvers, Cambridge University Press, 2020, p. 547–566. doi:10.1017/9781108637435.032

    work page doi:10.1017/9781108637435.032 2020

  22. [23]

    M. J. H. Heule, M. Scheucher, Happy ending: An empty hexagon in every set of 30 points, in: B. Finkbeiner, L. Kovács (Eds.), 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 14570 ofLecture Notes in Computer Science, Springer Nature Switzerland, Cham, 2024, p. 61–80. doi:10.1007/978-3-031-57246-3_5

    work page doi:10.1007/978-3-031-57246-3_5 2024

  23. [24]

    Subercaseaux, E

    B. Subercaseaux, E. Mackey, L. Qian, M. Heule, Automated symmetric constructions in discrete geometry, in: V. de Paiva, P. Koepke (Eds.), Intelligent Computer Mathematics, volume 16136 of Lecture Notes in Computer Science, Springer Nature Switzerland, 2025, p. 29–47. doi: 10.1007/ 978-3-032-07021-0_3

    2025

  24. [25]

    Subercaseaux, J

    B. Subercaseaux, J. Mackey, M. J. H. Heule, R. Martins, Automated mathematical discovery and verification: Minimizing pentagons in the plane, in: A. Kohlhase, L. Kovács (Eds.), Intelligent Computer Mathematics, volume 14960 ofLecture Notes in Computer Science, Springer Nature Switzerland, Cham, 2024, p. 21–41. doi:10.1007/978-3-031-66997-2_2

    work page doi:10.1007/978-3-031-66997-2_2 2024

  25. [26]

    Bright, K

    C. Bright, K. K. H. Cheung, B. Stevens, I. Kotsireas, V. Ganesh, A SAT-based resolution of Lam’s problem, Proceedings of the AAAI Conference on Artificial Intelligence 35 (2021) 3669–3676. doi:10.1609/aaai.v35i5.16483

    work page doi:10.1609/aaai.v35i5.16483 2021

  26. [27]

    In: Sankaranarayanan, S., Sharygina, N

    B. Subercaseaux, M. J. H. Heule, The packing chromatic number of the infinite square grid is 15, in: S. Sankaranarayanan, N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, volume 13993 ofLecture Notes in Computer Science, Springer Nature Switzerland, Cham, 2023, p. 389–406. doi:10.1007/978-3-031-30823-9_20

    work page doi:10.1007/978-3-031-30823-9_20 2023

  27. [28]

    Bright, J

    C. Bright, J. Gerhard, I. Kotsireas, V. Ganesh, Effective problem solving using SAT solvers, in: J. Gerhard, I. Kotsireas (Eds.), Maple in Mathematics Education and Research, volume 1125 of Communications in Computer and Information Science, Springer International Publishing, Cham, 2020, p. 205–219. doi:10.1007/978-3-030-41258-6_15

    work page doi:10.1007/978-3-030-41258-6_15 2020

  28. [29]

    Fazekas, A

    K. Fazekas, A. Niemetz, M. Preiner, M. Kirchweger, S. Szeider, A. Biere, IPASIR-UP: User Propagators for CDCL, in: M. Mahajan, F. Slivovsky (Eds.), 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), volume 271 ofLeibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für Inf...

    work page doi:10.4230/lipics.sat.2023.8 2023

  29. [30]

    Bright, I

    C. Bright, I. Kotsireas, V. Ganesh, When satisfiability solving meets symbolic computation, Communications of the ACM 65 (2022) 64–72. doi:10.1145/3500921

    work page doi:10.1145/3500921 2022

  30. [31]

    M. England, SC-square: Overview to 2021, in: SC 2 2021: 6th International Workshop on Satisfia- bility Checking and Symbolic Computation, volume 3273 ofCEUR Workshop Proceedings, 2021, pp. 1–6. URL: https://ceur-ws.org/Vol-3273/invited1.pdf

    2021

  31. [32]

    E. Abraham, Building bridges between symbolic computation and satisfiability checking, in: Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation, ISSAC’15, ACM, 2015, p. 1–6. doi:10.1145/2755996.2756636

    work page doi:10.1145/2755996.2756636 2015

  32. [33]

    Zulkoski, V

    E. Zulkoski, V. Ganesh, K. Czarnecki, MathCheck: A math assistant via a combination of computer algebra systems and SAT solvers, in: Automated Deduction - CADE-25, volume 9195 ofLecture Notes in Computer Science, Springer International Publishing, 2015, p. 607–622. doi: 10.1007/ 978-3-319-21401-6_41

    2015

  33. [34]

    Z. Li, C. Bright, V. Ganesh, An SC-square approach to the minimum Kochen–Specker problem, in: SC2 2022: 7th International Workshop on Satisfiability Checking and Symbolic Computation, volume 3458 ofCEUR Workshop Proceedings, 2022, p. 55–66. URL: https://ceur-ws.org/Vol-3458/ paper6.pdf

    2022

  34. [35]

    Z. Li, C. Bright, V. Ganesh, A SAT solver + computer algebra attack on the minimum Kochen–Specker problem, in: K. Larson (Ed.), Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24, International Joint Conferences on Artificial Intelligence Organization, 2024, pp. 1898–1906. doi:10.24963/ijcai.2024/210, main Track

    work page doi:10.24963/ijcai.2024/210 2024

  35. [36]

    Ajani, C

    Y. Ajani, C. Bright, A hybrid SAT and lattice reduction approach for integer factorization, in: SC 2 2023: 8th International Workshop on Satisfiability Checking and Symbolic Computation, volume 3455 ofCEUR Workshop Proceedings, 2023, pp. 39–43. URL: https://cs.uwaterloo.ca/~cbright/reports/ sc2-fact-update.pdf

    2023

  36. [37]

    Ajani, C

    Y. Ajani, C. Bright, SAT and lattice reduction for integer factorization, in: Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation, ISSAC ’24, ACM, 2024, p. 391–399. doi:10.1145/3666000.3669712

    work page doi:10.1145/3666000.3669712 2024

  37. [38]

    Alamgir, S

    N. Alamgir, S. Nejati, C. Bright, SHA-256 collision attack with programmatic SAT, in: SC 2 2024: 9th International Workshop on Satisfiability Checking and Symbolic Computation, volume 3717 ofCEUR Workshop Proceedings, 2024, pp. 91–110. URL: https://ceur-ws.org/Vol-3717/paper5.pdf

    2024

  38. [39]

    Ahmed, L

    T. Ahmed, L. Zaman, C. Bright, Symbolic sets for proving bounds on Rado numbers, in: SC 2 2025: 10th International Workshop on Satisfiability Checking and Symbolic Computation, volume 4116 ofCEUR Workshop Proceedings, 2025, pp. 55–75. URL: https://ceur-ws.org/Vol-4116/paper139.pdf

    2025

  39. [40]

    Kaski, O

    P. Kaski, O. Pottonen,libexactuser’s guide, version 1.0 (2008). URL: https://pottonen.kapsi.fi/ hiit-tr-2008-1.pdf, HIIT Technical Reports 2008–1, Helsinki Institute for Information Technology HIIT

    2008

  40. [41]

    G. Appa, I. Mourtos, D. Magos, Integrating Constraint and Integer Programming for the Orthog- onal Latin Squares Problem, volume 2470 ofLecture Notes in Computer Science, Springer Berlin Heidelberg, 2002, p. 17–32. doi:10.1007/3-540-46135-3_2

    work page doi:10.1007/3-540-46135-3_2 2002

  41. [42]

    G. Appa, D. Magos, I. Mourtos, A branch & cut algorithm for a four-index assignment problem, Journal of the Operational Research Society 55 (2004) 298–307. doi:10.1057/palgrave.jors. 2601655

    work page doi:10.1057/palgrave.jors 2004

  42. [43]

    G. Appa, D. Magos, I. Mourtos, An LP-based proof for the non-existence of a pair of orthogonal Latin squares of order 6, Operations Research Letters 32 (2004) 336–344. doi: 10.1016/j.orl. 2003.10.010

    work page doi:10.1016/j.orl 2004

  43. [44]

    F. Ma, J. Zhang, Finding orthogonal Latin squares using finite model searching tools, Science China Information Sciences 56 (2013) 1–9. doi:10.1007/s11432-011-4343-3

    work page doi:10.1007/s11432-011-4343-3 2013

  44. [45]

    Zaikin, S

    O. Zaikin, S. Kochemazov, A. Semenov, SAT-based search for systems of diagonal Latin squares in volunteer computing project SAT@home, in: 39th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), 2016, pp. 277–281. doi:10.1109/MIPRO.2016.7522152

    work page doi:10.1109/mipro.2016.7522152 2016

  45. [46]

    Zaikin, S

    O. Zaikin, S. Kochemazov, The search for systems of diagonal Latin squares using the SAT@home project, volume 3 ofCEUR Workshop Proceedings, 2015, pp. 4–9. URL: https://ceur-ws.org/Vol-1502/ paper6.pdf

    2015

  46. [47]

    Zaikin, A

    O. Zaikin, A. Zhuravlev, S. Kochemazov, E. Vatutin, On the construction of triples of diagonal Latin squares of order 10, Electronic Notes in Discrete Mathematics 54 (2016) 307–312. doi: 10. 1016/j.endm.2016.09.053

    2016

  47. [48]

    Vatutin, O

    E. Vatutin, O. Zaikin, M. Manzyuk, N. Nikitina, Searching for Orthogonal Latin Squares via Cells Mapping and BOINC-Based Cube-and-Conquer, volume 1510 ofCommunications in Computer and Information Science, 2021, pp. 498–512. doi:10.1007/978-3-030-92864-3_38

    work page doi:10.1007/978-3-030-92864-3_38 2021

  48. [49]

    R. Lu, S. Liu, J. Zhang, Searching for Doubly Self-orthogonal Latin Squares, volume 6876 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2011, p. 538–545. doi: 10.1007/ 978-3-642-23786-7_41

    2011

  49. [50]

    R. M. Falcón, Ó. J. Falcón, J. Núñez, Computing the sets of totally symmetric and totally conjugate orthogonal partial Latin squares by means of a SAT solver, in: Proceedings of the 17th International Conference on Computational and Mathematical Methods in Science and Engineering, 2017, pp. 841–852. URL: http://hdl.handle.net/11441/62076

    2017

  50. [51]

    Huang, M

    P. Huang, M. Liu, C. Ge, F. Ma, J. Zhang, Investigating the existence of orthogonal golf designs via satisfiability testing, in: ISSAC ’19: Proceedings of the 2019 International Symposium on Symbolic and Algebraic Computation, 2019, pp. 203–210. doi:10.1145/3326229.3326232

    work page doi:10.1145/3326229.3326232 2019

  51. [52]

    J. Jin, Y. Lv, C. Ge, F. Ma, J. Zhang, Investigating the Existence of Costas Latin Squares via Satisfiability Testing, volume 12831 ofLecture Notes in Computer Science, 2021, pp. 270–279. doi:10.1007/978-3-030-80223-3_19

    work page doi:10.1007/978-3-030-80223-3_19 2021

  52. [53]

    Zhang, Specifying Latin square problems in propositional logic, in: Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, Cambridge, MA, USA, 1997, p

    H. Zhang, Specifying Latin square problems in propositional logic, in: Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, Cambridge, MA, USA, 1997, p. 115–146. URL: https://dl.acm.org/doi/10.5555/271101.271124

    work page doi:10.5555/271101.271124 1997

  53. [54]

    Zaikin, E

    O. Zaikin, E. Vatutin, C. Bright, Enumerating extended self-orthogonal diagonal Latin squares of order up to 10, Journal of Integer Sequences 28 (2025). URL: https://cs.uwaterloo.ca/journals/JIS/ VOL28/Zaikin/zaikin4.html, article 28.7.4

    2025

  54. [55]

    Bright, A

    C. Bright, A. Keita, B. Stevens, Orthogonal Latin squares of order 10 with two relations: A SAT investigation, Discrete Mathematics, Algorithms and Applications (2025). doi: 10.1142/ s1793830925501563, to appear

    2025

  55. [56]

    Bailleux, Y

    O. Bailleux, Y. Boufkhad, Efficient CNF Encoding of Boolean Cardinality Constraints, in: F. Rossi (Ed.), Principles and Practice of Constraint Programming – CP 2003, volume 2833 ofLecture Notes in Computer Science, Springer Berlin Heidelberg, Berlin, Heidelberg, 2003, pp. 108–122. doi:10.1007/978-3-540-45193-8_8

    work page doi:10.1007/978-3-540-45193-8_8 2003