Applying computer algebra systems with SAT solvers to the Williamson conjecture. (September 2020)

• Record Type: Journal Article
• Authors: Bright, Curtis; Kotsireas, Ilias; Ganesh, Vijay
• Is Part Of: Journal of symbolic computation. Volume 100(2020)
• Page Start: 187
• Page End: 209
• Publication Date: 2020-09
• Subjects: Williamson matrices -- Boolean satisfiability -- SAT solvers -- Exhaustive search -- Autocorrelation; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2019.07.024
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: We employ tools from the fields of symbolic computation and satisfiability checking—namely, computer algebra systems and SAT solvers—to study the Williamson conjecture from combinatorial design theory and increase the bounds to which Williamson matrices have been enumerated. In particular, we completely enumerate all Williamson matrices of even order up to and including 70 which gives us deeper insight into the behaviour and distribution of Williamson matrices. We find that, in contrast to the case when the order is odd, Williamson matrices of even order are quite plentiful and exist in every even order up to and including 70. As a consequence of this and a new construction for 8-Williamson matrices we construct 8-Williamson matrices in all odd orders up to and including 35. We additionally enumerate all Williamson matrices whose orders are divisible by 3 and less than 70, finding one previously unknown set of Williamson matrices of order 63.