Discrete Math Seminar: Curtis Bright

Solvers for the Boolean satisfiability problem have been increasingly used to solve hard problems from many fields and now routinely solve problems with millions of variables. Combinatorial problems are a natural target, as SAT solvers contain excellent combinatorial search algorithms. Despite this, SAT solvers can fail on small problems, for example when properties of the problem cannot be concisely expressed in Boolean logic. We describe a new combinatorial search method that allows properties to be specified using a computer algebra system (CAS), thereby combining the expressiveness of a CAS with the search power of SAT solvers. In this talk we describe how our SAT+CAS system MathCheck has verified, partially verified, or found new counterexamples to conjectures from design theory, graph theory, and number theory. In particular, we have classified Williamson matrices up to order 70, quaternary Golay sequence pairs up to length 28, best matrices up to order 7, verified the Ruskey–Savage and Norine conjectures up to larger bounds than had previously been verified, found the smallest counterexample of the Williamson conjecture, and found three new counterexamples to a conjecture on good matrices. Currently we are using the system to verify the nonexistence of projective planes of order 10.