Reproduce “Improving SAT Solvers on Orthogonal Latin Square Problems” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Aaron Barnoff, Curtis Bright
A hybrid solver combines CaDiCaL SAT search with the Euler–Parker transversal and exact-cover procedure to construct orthogonal mates under complex structural constraints. On unrestricted instances of orders 8–12, it reduced median solve times from as much as 39,383.54 seconds to 2.23 seconds, and on Myrvold’s eight structured order-10 cases it solved every randomized run, including cases that pure SAT frequently failed to finish.
Key insights
- The most effective division of labour is to let SAT manage unusual global constraints while delegating the specialized orthogonal-mate construction to transversal and exact-cover algorithms.
- Static SAT encodings may find suitable Latin squares but can become trapped in inefficient mate construction; explicit Euler–Parker calls avoid repeatedly altering the underlying square during that search.
- External reasoning must be scheduled carefully: requiring ordinary SAT conflicts between callbacks substantially reduced memory consumption and improved practical performance.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.