  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-\`a-vis best
matrices. The SAT+CAS method is a variant of the
Davis$\unicode{8211}$Putnam$\unicode{8211}$Logemann$\unicode{8211}$Loveland
$\operatorname{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\leq6$
also holds for $r=7$. We also confirmed the results of the exhaustive searches
that have been previously completed for $r\leq6$.
