A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples
Authors: Curtis Bright, Dragomir Ž. Ðoković, Ilias Kotsireas, Vijay Ganesh1435-1442
AAAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We enumerate all circulant good matrices with odd orders divisible by 3 up to order 70. As a consequence of this we find a previously overlooked set of good matrices of order 27 and a new set of good matrices of order 57. We also find that circulant good matrices do not exist in the orders 51, 63, and 69, thereby finding three new counterexamples to the conjecture that such matrices exist in all odd orders. Additionally, we prove a new relationship between the entries of good matrices and exploit this relationship in our enumeration algorithm. Our method applies the SAT+CAS paradigm of combining computer algebra functionality with modern SAT solvers to efficiently search large spaces which are specified by both algebraic and logical constraints.The computations were run on a cluster of 64-bit Opteron 2.2GHz and Xeon 2.6GHz processors running Cent OS 6.9 and using 500MB of memory. By far the most computationally expensive step of our algorithm was running the SAT solver. This accounted for 99.9% of the total running time, underscoring the importance of using a state-of-the-art SAT solver such as MAPLESAT. This step was parallelized across 250 cores and completed in about two weeks. Despite step 4 being the bottleneck the other steps were found to be essential could not be removed without significantly increasing the computation time. The timings for running our implementation in each odd order divisible by 3 up to order 70 are given in Table 1. |
| Researcher Affiliation | Academia | Curtis Bright University of Waterloo Dragomir Ž. Ðokovi c University of Waterloo Ilias Kotsireas Wilfrid Laurier University Vijay Ganesh University of Waterloo |
| Pseudocode | No | The paper describes its enumeration algorithm and SAT encoding steps in detailed paragraph text and numbered lists, but does not present them in structured pseudocode or an algorithm block format. |
| Open Source Code | Yes | Our code is available from our website uwaterloo.ca/mathcheck. |
| Open Datasets | No | The paper describes a computational enumeration algorithm for finding mathematical objects (circulant good matrices) rather than using or training on a pre-existing dataset. Therefore, the concept of public dataset availability is not applicable in this context. |
| Dataset Splits | No | The paper describes an enumeration algorithm for mathematical objects and does not involve dataset splitting for training, validation, or testing in the typical machine learning sense. |
| Hardware Specification | Yes | The computations were run on a cluster of 64-bit Opteron 2.2GHz and Xeon 2.6GHz processors running Cent OS 6.9 and using 500MB of memory. |
| Software Dependencies | No | The paper mentions several software components: 'NSOKS in MAPLE (Riel 2006)', 'custom C++ code', 'GNU core utility SORT', 'programmatic SAT solver MAPLESAT (Liang et al. 2016)', and 'the library FFTW (Frigo and Johnson 2005)'. While tools are named and cited, specific version numbers for MAPLE, MAPLESAT, FFTW, or GNU SORT are not provided, preventing full reproducibility based on software versions. |
| Experiment Setup | Yes | We now describe our algorithm in four steps followed by some postprocessing.We encode the entries of the defining rows of a set of good matrices A, B, C, D of order n using 4n Boolean variables where we let true values denote 1 and false values denote 1.The callback function used in our encoding of good matrices works by encoding the property given in Corollary 3 and its steps are described in detail below.Finally, we discuss how to encode Corollary 8.For the benefit of those who would like to implement our algorithm we now discuss some optimizations that we found useful. In the programmatic encoding and in step 2 of our enumeration algorithm we need to check if there exists an integer k such that PSDX(k) > 4n for a given sequence X. We only need to check k with 0 k < n/2 because the symmetries of the Fourier transform on real input X imply that PSDX(k) = PSDX( k mod n). |