The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices
arXiv:1907.04987 · doi:10.1007/s10472-019-09681-3
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 Davis$\unicode{8211}$Putnam$\unicode{8211}$Logemann$\unicode{8211}$Loveland architecture, where the 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 ) which was previously known to hold for also holds for . We also confirmed the results of the exhaustive searches that have been previously completed for .
arXiv commentTo appear in Annals of Mathematics and Artificial Intelligence
References in corpus (10)
- Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
- Compression of Periodic Complementary Sequences and Applications
- Satisfiability Checking meets Symbolic Computation (Project Paper)
- Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture
- On the van der Waerden numbers w(2;3,t)
- Exact Ramsey Theory: Green-Tao numbers and SAT
- Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT
- Goethals--Seidel difference families with symmetric or skew base blocks
- Skew-Hadamard matrices of orders 188 and 388 exist
- A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples