Curtis Bright, School of Computer Science, Waterloo University

In this talk, we present MathCheck2, a combination of a SAT solver and a computer algebra system (CAS) aimed at finitely verifying or counterexampling mathematical conjectures. Using MathCheck2 we generated Hadamard matrices all orders 4n with n < 35 and provided 160 matrices to the Magma Hadamard database that were not equivalent to any matrix previously in that database. Furthermore, we provide independent verification of the claim that Williamson matrices of order 35 do not exist, and demonstrate for the first time that 35 is the smallest number with this property. The crucial insight behind the MathCheck2 algorithm and tool is that a combination of an efficient search procedure (like those in SAT solvers) with a domain-specific knowledge base (a la CAS) can be a very effective way to verify, counterexample, and learn deeper properties of mathematical conjectures (especially in combinatorics) and the structures they refer to. MathCheck2 uses a divide-and-conquer approach to parallelize the search, and a CAS to prune away classes of structures that are guaranteed to not satisfy the conjecture-under-verification C. The SAT solver is used to verify whether any of the remaining structures satisfy C, and in addition learn UNSAT cores in a conflict-driven clause-learning style feedback loop to further prune away non-satisfying structures. (This is joint work by Curtis Bright, Vijay Ganesh, Albert Heinle, Ilias Kotsireas, Saeed Nejati, and Krzysztof Czarnecki)