SAT Solving with Computer Algebra and its Application to Graph Theory and Geometry

Curtis Bright

Carleton University

In this talk we describe a combinatorial search method that combines the search power of Boolean satisfiability (SAT) solvers with the mathematical expressiveness of computer algebra systems (CAS). We discuss our system MathCheck and how the SAT+CAS method has been used to derive the best known results in a number of problems from graph theory, geometry, combinatorics, and number theory. Specifically, we describe how MathCheck has been used in the Ruskey-Savage hypercube conjecture (1993), Lam's problem from discrete geometry (1800s), and briefly outline Heule's result in the Hadwiger-Nelson plane-colouring problem (1950).