# zbMATH — the first resource for mathematics

The SAT+CAS method for combinatorial search with applications to best matrices. (English) Zbl 1434.05001
Authors’ 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 on vis-à-vis best matrices. The SAT+CAS method is a variant of the Davis-Putnam-Logemann-Loveland DPLL($$T$$ ) architecture, where the $$T$$ solver is replaced by a CAS. We describe how the SAT+CAS method has been previously 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 present new skew Hadamard matrices constructed from best matrices. We show the best matrix conjecture (that best matrices exist in all orders of the form $$r^{2}+r+1$$) which was previously known to hold for $$r\leq 6$$ also holds for $$r = 7$$. We also confirmed the results of the exhaustive searches that have been previously completed for $$r\leq 6$$.”
The authors proved for the first time that best matrices exist for $$r = 7$$ by explicitly constructing best matrices of order 57 – the largest best matrices currently known.
##### MSC:
 05-04 Software, source code, etc. for problems pertaining to combinatorics 05B20 Combinatorial aspects of matrices (incidence, Hadamard, etc.) 68R05 Combinatorics in computer science 68T27 Logic in artificial intelligence 68W30 Symbolic computation and algebraic computation
##### Software:
STP; SageMath; Lynx; Mathematica; Mace4; z3; tawSolver; Maple; Yices; FFTW; MathCheck; GitHub
Full Text: