The SAT+CAS method for combinatorial search with applications to best matrices

DOI10.1007/S10472-019-09681-3zbMATH Open1434.05001arXiv1907.04987OpenAlexW2921963619WikidataQ126637641 ScholiaQ126637641MaRDI QIDQ2294574FDOQ2294574

Vijay Ganesh, Ilias S. Kotsireas, Dragomir Ž. Đoković, Curtis Bright

Publication date: 11 February 2020

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

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 Davis$unicode8211$Putnam$unicode8211$Logemann$unicode8211$Loveland $operatornameDPLL(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 $rleq6$ also holds for $r=7$. We also confirmed the results of the exhaustive searches that have been previously completed for $rleq6$.

Full work available at URL: https://arxiv.org/abs/1907.04987

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

zbMATH Keywords

symbolic computationsatisfiability checkingcombinatorial searchskew Hadamard matrixSAT+CAScirculant best matrices

Mathematics Subject Classification ID

Combinatorics in computer science (68R05) Symbolic computation and algebraic computation (68W30) Combinatorial aspects of matrices (incidence, Hadamard, etc.) (05B20) Logic in artificial intelligence (68T27) Software, source code, etc. for problems pertaining to combinatorics (05-04)

Cites Work

• MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
• MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
• A Decision Procedure for Bit-Vectors and Arrays
• On Balanced Half-Sample Variance Estimation in Stratified Random Sampling
• Title not available (Why is that?)
• Title not available (Why is that?)
• Hadamard matrices and their applications
• Solving SAT and SAT Modulo Theories
• Hadamard matrices and their applications
• Computer Aided Verification
• Computational excursions in analysis and number theory
• Perfect matchings extend to Hamilton cycles in hypercubes
• Supplementary difference sets with symmetry for Hadamard matrices
• Skew-Hadamard matrices of orders 188 and 388 exist
• Title not available (Why is that?)
• On skew-Hadamard matrices
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• A Hadamard matrix of order 428
• Small Golay sequences
• Title not available (Why is that?)
• Hamilton Cycles that Extend Transposition Matchings in Cayley Graphs of $S_n $
• The van der Waerden NumberW(2, 6) Is 1132
• On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
• Green-Tao Numbers and SAT
• Weighing matrices and string sorting
• A SAT Attack on the Erdős Discrepancy Conjecture
• Williamson matrices up to order 59
• The Search for Hadamard Matrices
• Compression of periodic complementary sequences and applications
• Skew Hadamard designs and their codes
• Title not available (Why is that?)
• A skew Hadamard matrix of order 36
• Hadamard's determinant theorem and the sum of four squares
• Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
• Building bridges between symbolic computation and satisfiability checking
• Enumeration of Complex Golay Pairs via Programmatic SAT
• Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
• Theory and Applications of Satisfiability Testing
• On circulant best matrices and their applications
• Title not available (Why is that?)
• Complex Golay sequences: Structure and applications
• Hadamard matrices of Williamson type: A challenge for computer algebra
• Goethals-Seidel difference families with symmetric or skew base blocks
• An empirical study of branching heuristics through the lens of global learning rate
• $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
• Theory and Applications of Satisfiability Testing
• Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT
• The SAT+CAS method for combinatorial search with applications to best matrices
• On the autocorrelations of \(\pm 1\) polynomials
• Formal Methods for Hardware Verification

Cited In (3)

• 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

Uses Software

• Maple
• Mathematica
• SageMath
• FFTW
• Yices
• z3
• Mace4
• tawSolver
• MathCheck
• Lynx
• STP
• GitHub

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)