SAT Solving with Computer Algebra: A Powerful Combinatorial Search Method.

Curtis Bright, University of Waterloo.

Tuesday September 3rd, 1:30pm in K9509.

Abstract

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.