Edward
Zulkoski,
PhD
candidate
David
R.
Cheriton
School
of
Computer
Science
We present a method and an associated system, called MathCheck, that embeds the functionality of a computer algebra system (CAS) within the inner loop of a conflict-driven clause-learning SAT solver. Such a SAT+CAS system combines the efficient search routines of modern SAT solvers with the expressive power of CAS, thus complementing both. The key insight behind the power of the SAT+CAS combination is that the CAS system can help cut down the search-space of the SAT solver, by providing learned clauses that encode theory-specific lemmas, as it searches for a counter example to the input conjecture. In addition, the combination enables a more efficient encoding of problems than a pure Boolean representation.
As case studies, we study two open mathematical conjectures from graph theory regarding properties of hypercubes. The first conjecture states that any matching of any d-dimensional hypercube can be extended to a Hamiltonian cycle; the second states that given an edge-antipodal coloring of a hypercube there always exists a monochromatic path between two antipodal vertices. Previous results have shown the conjectures true up to certain low-dimensional hypercubes. We extend these two conjectures to higher-dimensional hypercubes.