The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices

EasyChair Preprint no. 825

Abstract

In this paper, we provide an overview of the SAT+CAS method that combines satisfiability checkers (SAT solvers) and computer algebra systems (CAS) to resolve combinatorial conjectures, and present new results vis-à-vis best matrices. The SAT+CAS method is a variant of the DPLL(T) architecture, where the T solver is replaced by a CAS. We describe how the SAT+CAS method has been used to resolve many open problems from graph theory, combinatorial design theory, and number theory, showing that the method has broad applications across a variety of fields. Additionally, we apply the method to construct the largest best matrices yet known and find new skew Hadamard matrices constructed from best matrices. As a consequence of this we show that a conjecture on the existence of best matrices that was previously known to hold for r ≤ 6 also holds for r = 7.

Keyphrases: Artificial Intelligence, combinatorial design theory, combinatorial search, SAT+CAS, satisfiability checking, symbolic computation

@Booklet{EasyChair:825,
  author = {Curtis Bright and Dragomir Ž Djoković and Ilias Kotsireas and Vijay Ganesh},
  title = {The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices},
  howpublished = {EasyChair Preprint no. 825},
  doi = {10.29007/91wj},
  year = {EasyChair, 2019}}