Reproduce “A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples” 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
Curtis Bright, Dragomir Z. Djokovic, Ilias Kotsireas, Vijay Ganesh
A hybrid SAT, Fourier-filtering, compression, and computer-algebra search classifies circulant good matrices for odd orders divisible by 3 through 69. It uncovers a previously missed solution at order 27, finds the first solution at order 57, and establishes nonexistence at orders 51, 63, and 69 within the circulant class.
Key insights
- The product relation linking entries at positions k and 2k provides a strong local constraint that substantially strengthens the SAT encoding without explicitly Booleanizing Fourier calculations.
- Compression separates the large search into smaller spectral subproblems, while computer algebra restricts the possible sums of the three symmetric rows before enumeration begins.
- Existence among circulant good matrices is irregular: several orders fail despite neighboring orders admitting solutions, so the odd-order existence conjecture does not hold in this restricted setting.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.