A SAT+CAS Method for Enumerating Williamson Matrices of Even Order
Authors: Curtis Bright, Ilias Kotsireas, Vijay Ganesh
AAAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present for the first time an exhaustive enumeration of Williamson matrices of even order n < 65. The search method relies on the novel SAT+CAS paradigm of coupling SAT solvers with computer algebra systems so as to take advantage of the advances made in both the field of satisfiability checking and the field of symbolic computation. Additionally, we use a programmatic SAT solver which allows conflict clauses to be learned programmatically, through a piece of code specifically tailored to the domain area. Timings for running our entire algorithm (in hours) are given in Table 1, and timings for the running of the SAT solver alone are given in Table 2. |
| Researcher Affiliation | Academia | Curtis Bright University of Waterloo Ilias Kotsireas Wilfrid Laurier University Vijay Ganesh University of Waterloo |
| Pseudocode | No | The paper describes the algorithm steps in paragraphs (e.g., |
| Open Source Code | No | The paper states: |
| Open Datasets | No | The paper is focused on the exhaustive enumeration of mathematical objects (Williamson matrices) rather than training a model on a pre-existing dataset. No public dataset for training is mentioned. |
| Dataset Splits | No | This paper does not involve machine learning models and therefore does not use validation sets or splits in the traditional sense. |
| Hardware Specification | Yes | Our computations were performed on a cluster of 64-bit AMD Opteron 2.2 GHz processors limited to 6 GB of memory and running Cent OS 6.7. |
| Software Dependencies | No | The paper mentions software used, such as |
| Experiment Setup | No | The paper describes the algorithmic steps and optimizations but does not provide specific experimental setup details like hyperparameter values or detailed configurations for the SAT solver beyond its programmatic interface. |