A SAT+CAS Method for Enumerating Williamson Matrices of Even Order

Authors

  • Curtis Bright University of Waterloo
  • Ilias Kotsireas Wilfrid Laurier University
  • Vijay Ganesh University of Waterloo

Keywords:

satisfiability checking, symbolic computation, Williamson matrices

Abstract

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. Prior to our work, Williamson matrices had only been enumerated for odd orders n < 60, so our work increases the bounds that Williamson matrices have been enumerated up to and provides the first enumeration of Williamson matrices of even order. Our results show that Williamson matrices of even order tend to be much more abundant than those of odd orders. In particular, Williamson matrices exist for every even order n < 65 but do not exist in orders 35, 47, 53, and 59.

Downloads

Published

2018-04-26

How to Cite

Bright, C., Kotsireas, I., & Ganesh, V. (2018). A SAT+CAS Method for Enumerating Williamson Matrices of Even Order. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1). Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/12203

Issue

Section

Main Track: Search and Constraint Satisfaction