Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture

TL;DR

This paper uses computer algebra systems and SAT solvers to enumerate Williamson matrices up to order 70, revealing their distribution and constructing new matrices, thus advancing understanding in combinatorial design theory.

Contribution

It introduces a novel computational approach combining symbolic computation and satisfiability checking to enumerate Williamson matrices and discover new instances.

Findings

Williamson matrices are abundant in even orders up to 70.

Constructed 8-Williamson matrices for all odd orders up to 35.

Discovered a previously unknown Williamson matrix set of order 63.

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.