Curtis Bright (University of Waterloo)
SAT+CAS: A Powerful New Combinatorial Search Method

Solvers for the Boolean satisfiability problem have been increasingly used to solve hard problems in many fields and now routinely solve problems with millions of variables. Combinatorics is a natural source of problems for this as SAT solvers contain excellent combinatorial search algorithms. Despite this, sometimes SAT solvers will fail on tiny instances of such problems. This can often be solved by exploiting theoretical properties of the problem but many properties are too cumbersome to specify in Boolean logic. We describe a new combinatorial search method which allows such properties to be specified using a computer algebra system (CAS), thereby combining the expressiveness of a CAS with the search power of SAT solvers. As a case study we consider the Hadamard conjecture from combinatorial design theory and outline how the SAT+CAS paradigm was successful in finding many new Hadamard matrices. In particular, our SAT+CAS system MathCheck found over 100,000 new Williamson matrices including the first Williamson matrices of odd order found in over ten years (see curtisbright.com/mathcheck for more information). Joint work with Vijay Ganesh of the University of Waterloo and Ilias Kotsireas of Wilfrid Laurier University.