Tutte Colloquium - Curtis Bright

Title: SAT Solving with Computer Algebra for Combinatorics

Abstract:

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.