LIPIcs.CP.2023.48.pdf
- Filesize: 0.63 MB
- 10 pages
Document
Proven Optimally-Balanced Latin Rectangles with SAT (Short Paper)
Authors
Vaidyanathan Peruvemba Ramaswamy 
,
Stefan Szeider
-
Part of:
Volume:
29th International Conference on Principles and Practice of Constraint Programming (CP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Principles and Practice of Constraint Programming (CP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-22
File
Document Identifiers
Author Details
Acknowledgements
This work was carried out in part while the second author visited the Simons Institute for the Theory of Computing, University of Berkeley, within the program Extended Reunion: Satisfiability.
Cite AsGet BibTex
Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider. Proven Optimally-Balanced Latin Rectangles with SAT (Short Paper). In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 48:1-48:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CP.2023.48
https://doi.org/10.4230/LIPIcs.CP.2023.48
Abstract
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.
Subject Classification
ACM Subject Classification
- Hardware → Theorem proving and SAT solving
- Theory of computation → Constraint and logic programming
- Mathematics of computing → Combinatoric problems
- Software and its engineering → Constraints
- Theory of computation → Integer programming
- Mathematics of computing → Combinatorial optimization
- Mathematics of computing → Enumeration
- Mathematics of computing → Solvers
- Computing methodologies → Theorem proving algorithms
- Applied computing → Agriculture
Keywords
- combinatorial design
- SAT encodings
- certified optimality
- arithmetic constraints
- spatially balanced Latin rectangles
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Carlos Ansótegui and Felip Manyà. Mapping problems with finite-domain variables to problems with boolean variables. In Holger H. Hoos and David G. Mitchell, editors, Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers, volume 3542 of Lecture Notes in Computer Science, pages 1-15. Springer Verlag, 2004. URL: https://doi.org/10.1007/11527695_1.
- Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. URL: https://tuhat.helsinki.fi/ws/files/142452772/sc2020_proceedings.pdf.
- Mateo Díaz, Ronan Le Bras, and Carla P. Gomes. In search of balance: The challenge of generating balanced Latin rectangles. In Domenico Salvagnin and Michele Lombardi, editors, Integration of AI and OR Techniques in Constraint Programming - 14th International Conference, CPAIOR 2017, Padua, Italy, June 5-8, 2017, Proceedings, volume 10335 of Lecture Notes in Computer Science, pages 68-76. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-59776-8_6.
- Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r)evolution of SAT. Communications of the ACM, 66(6):64-72, June 2023. URL: https://doi.org/10.1145/3560469.
-
Ian P. Gent and Peter Nightingale. A new encoding of alldifferent into SAT. In International Workshop on Modelling and Reformulating Constraint Satisfaction, volume 3, pages 95-110, 2004.
- Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, and Nathan Wetzler. Efficient, verified checking of propositional proofs. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, volume 10499 of Lecture Notes in Computer Science, pages 269-284. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_18.
- Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving very hard problems: Cube-and-conquer, a hybrid SAT solving method. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 4864-4868. ijcai.org, 2017. URL: https://doi.org/10.24963/ijcai.2017/683.
- Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In SAT, pages 428-437, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
- Marcus Jones, Richard Woodward, and Jerry Stoller. Increasing precision in agronomic field trials using latin square designs. Agronomy Journal, 107(1):20-24, 2015. URL: https://doi.org/10.2134/agronj14.0232.
- Ronan LeBras, Carla P. Gomes, and Bart Selman. From streamlined combinatorial search to efficient constructive procedures. In Jörg Hoffmann and Bart Selman, editors, Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, July 22-26, 2012, Toronto, Ontario, Canada. AAAI Press, 2012. URL: https://doi.org/10.1609/aaai.v26i1.8147.
- Nicholas Nethercote, Peter J Stuckey, Ralph Becket, Sebastian Brand, Gregory J Duck, and Guido Tack. Minizinc: Towards a standard cp modelling language. In International Conference on Principles and Practice of Constraint Programming, volume 4741 of Lecture Notes in Computer Science, pages 529-543. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_38.
-
Steven David Prestwich. CNF encodings. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, pages 75-97. IOS Press, 2009.
-
H.M. Van Es and C.L. Van Es. Spatial nature of randomization and its effect on the outcome of field experiments. Agronomy Journal, 85(2):420-428, 1993.
- Marc Vinyals, Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, and Jakob Nordström. In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 292-310. Springer Verlag, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_18.
- Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing - SAT 2014, volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer Verlag, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.