Tutte Colloquium - Curtis Bright

Friday, April 1, 2022 3:30 pm - 3:30 pm EDT (GMT -04:00)

Title: SAT Solving with Computer Algebra for Combinatorics

Speaker: Curtis Bright
Affiliation: University of Windsor and Carleton University
Location: MC 5501 or please contact Emma Watson for Zoom link


This talk will describe a method of solving combinatorial problems by coupling Boolean satisfiability (SAT) solvers with computer algebra systems (CASs), thereby combining the search and learning power of SAT solvers with the expressiveness and mathematical sophistication of CASs.  This approach has led to the solution of a number of long-standing problems, including the first verifiable solution of Lam's problem from finite projective geometry.  We also discuss the resolution of a 75-year-old problem on the existence of Williamson matrices which led to the discovery of a family of perfect quaternion sequences conjectured to not exist.