The SAT+CAS method for combinatorial search with applications to best matrices
From MaRDI portal
Publication:2294574
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-`a-vis best matrices. The SAT+CAS method is a variant of the DavisPutnamLogemannLoveland 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 .
Recommendations
- Application of SAT-approach for solving combinatorial problems
- Matrix relaxations in combinatorial optimization
- Regular-SAT: A many-valued approach to solving combinatorial problems
- scientific article; zbMATH DE number 1342213
- Strategies for Solving SAT in Grids by Randomized Search
- An exact and a randomized approach for the satisfiability problem
- Local search with a SAT oracle for combinatorial optimization
- scientific article; zbMATH DE number 3847217
- Search techniques for SAT-based Boolean optimization
- Simultaneous approximation of constraint satisfaction problems
Cites work
- scientific article; zbMATH DE number 3643273 (Why is no real title available?)
- scientific article; zbMATH DE number 124523 (Why is no real title available?)
- scientific article; zbMATH DE number 3577144 (Why is no real title available?)
- scientific article; zbMATH DE number 1252517 (Why is no real title available?)
- scientific article; zbMATH DE number 5175625 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- A Decision Procedure for Bit-Vectors and Arrays
- A Hadamard matrix of order 428
- A SAT attack on the Erdős discrepancy conjecture
- A skew Hadamard matrix of order 36
- An empirical study of branching heuristics through the lens of global learning rate
- Building bridges between symbolic computation and satisfiability checking
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT
- Complex Golay sequences: Structure and applications
- Compression of periodic complementary sequences and applications
- Computational excursions in analysis and number theory
- Computer Aided Verification
- Enumeration of complex Golay pairs via programmatic SAT
- Formal Methods for Hardware Verification
- Goethals-Seidel difference families with symmetric or skew base blocks
- Green-Tao Numbers and SAT
- Hadamard matrices and their applications
- Hadamard matrices and their applications
- Hadamard matrices of Williamson type: A challenge for computer algebra
- Hadamard's determinant theorem and the sum of four squares
- Hamilton Cycles that Extend Transposition Matchings in Cayley Graphs of $S_n $
- Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
- On Balanced Half-Sample Variance Estimation in Stratified Random Sampling
- On circulant best matrices and their applications
- On skew-Hadamard matrices
- On the autocorrelations of \(\pm 1\) polynomials
- On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
- Perfect matchings extend to Hamilton cycles in hypercubes
- Skew Hadamard designs and their codes
- Skew-Hadamard matrices of orders 188 and 388 exist
- Small Golay sequences
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Supplementary difference sets with symmetry for Hadamard matrices
- The SAT+CAS method for combinatorial search with applications to best matrices
- The Search for Hadamard Matrices
- The van der Waerden NumberW(2, 6) Is 1132
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Weighing matrices and string sorting
- Williamson matrices up to order 59
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
Cited in
(7)- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
- Finding Antimagic Labelings of Trees by Evolutionary Search
- The SAT+CAS method for combinatorial search with applications to best matrices
- Applying computer algebra systems with SAT solvers to the Williamson conjecture
- MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
- Enumeration of complex Golay pairs via programmatic SAT
Describes a project that uses
Uses Software
This page was built for publication: The SAT+CAS method for combinatorial search with applications to best matrices
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2294574)
