Speaker: Curtis Bright, School of Computer Science, University of Windsor

and Vijay Ganesh, Dept. of Electrical and Computer Engineering, University of Waterloo

**Title**: When Computer Algebra Meets Satisfiability: A New Approach to Combinatorial Mathematics

**Abstract**: Solvers for the Boolean satisfiability (SAT) problem have been increasingly used to resolve problems in mathematics due to their excellent search algorithms. This talk will describe a new method for mathematical search that couples SAT solvers with computer algebra systems (CAS), thereby combining the expressiveness of CASs with the search power of SAT solvers. This paradigm has led to a number of results on long-standing mathematical questions such as the first computer-verifiable resolution of Lam’s problem and the discovery of a new infinite class of Williamson matrices.