Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture

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.

To appear in the Journal of Symbolic Computation

References in corpus (5)

• Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
• Compression of Periodic Complementary Sequences and Applications
• Satisfiability Checking meets Symbolic Computation (Project Paper)
• A New Form of Williamson's Product Theorem
• A doubling construction for Williamson matrices

Cited by in corpus (6)

• The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices
• New Infinite Families of Perfect Quaternion Sequences and Williamson Sequences
• SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
• Improving probability selecting based weights for Satisfiability Problem
• New Results on Periodic Golay Pairs
• Nonexistence Certificates for Ovals in a Projective Plane of Order Ten