2026-06-09T19:49:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19085 2024-03-06T11:03:28Z ddc:004 open_access

Proven Optimally-Balanced Latin Rectangles with SAT (Short Paper) Peruvemba Ramaswamy, Vaidyanathan Szeider, Stefan combinatorial design SAT encodings certified optimality arithmetic constraints spatially balanced Latin rectangles Motivated by applications from agronomic field experiments, Díaz, Le Bras, and Gomes [CPAIOR 2015] introduced Partially Balanced Latin Rectangles as a generalization of Spatially Balanced Latin Squares. They observed that the generation of Latin rectangles that are optimally balanced is a highly challenging computational problem. They computed, utilizing CSP and MIP encodings, Latin rectangles up to 12 × 12, some optimally balanced, some suboptimally balanced. In this paper, we develop a SAT encoding for generating balanced Latin rectangles. We compare experimentally encoding variants. Our results indicate that SAT encodings perform competitively with the MIP encoding, in some cases better. In some cases we could find Latin rectangles that are more balanced than previously known ones. This finding is significant, as there are many arithmetic constraints involved. The SAT approach offers the advantage that we can certify that Latin rectangles are optimally balanced through DRAT proofs that can be verified independently. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider 2023 Is Part Of LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2023.48 urn:nbn:de:0030-drops-190855 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.48 eng https://creativecommons.org/licenses/by/4.0/legalcode