The SAT+CAS method for combinatorial search with applications to best matrices
DOI10.1007/s10472-019-09681-3zbMath1434.05001arXiv1907.04987OpenAlexW2921963619WikidataQ126637641 ScholiaQ126637641MaRDI QIDQ2294574
Vijay Ganesh, Curtis Bright, Ilias S. Kotsireas, Dragomir Ž. Djoković
Publication date: 11 February 2020
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1907.04987
symbolic computationsatisfiability checkingcombinatorial searchskew Hadamard matrixSAT+CAScirculant best matrices
Symbolic computation and algebraic computation (68W30) Combinatorial aspects of matrices (incidence, Hadamard, etc.) (05B20) Combinatorics in computer science (68R05) Logic in artificial intelligence (68T27) Software, source code, etc. for problems pertaining to combinatorics (05-04)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Small Golay sequences
- On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
- Weighing matrices and string sorting
- Computational excursions in analysis and number theory
- On skew-Hadamard matrices
- Hadamard matrices of Williamson type: A challenge for computer algebra
- Williamson matrices up to order 59
- Skew Hadamard designs and their codes
- Complex Golay sequences: Structure and applications
- Goethals-Seidel difference families with symmetric or skew base blocks
- An empirical study of branching heuristics through the lens of global learning rate
- Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT
- Compression of periodic complementary sequences and applications
- The SAT+CAS method for combinatorial search with applications to best matrices
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Perfect matchings extend to Hamilton cycles in hypercubes
- Hadamard's determinant theorem and the sum of four squares
- On circulant best matrices and their applications
- $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Building Bridges between Symbolic Computation and Satisfiability Checking
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- On Balanced Half-Sample Variance Estimation in Stratified Random Sampling
- A SAT Attack on the Erdős Discrepancy Conjecture
- MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
- Solving SAT and SAT Modulo Theories
- The van der Waerden NumberW(2, 6) Is 1132
- Supplementary difference sets with symmetry for Hadamard matrices
- Skew-Hadamard matrices of orders 188 and 388 exist
- The Search for Hadamard Matrices
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- Green-Tao Numbers and SAT
- Enumeration of Complex Golay Pairs via Programmatic SAT
- Hamilton Cycles that Extend Transposition Matchings in Cayley Graphs of $S_n $
- Computer Aided Verification
- Theory and Applications of Satisfiability Testing
- A Decision Procedure for Bit-Vectors and Arrays
- A skew Hadamard matrix of order 36
- A Hadamard matrix of order 428
- Theory and Applications of Satisfiability Testing
- Formal Methods for Hardware Verification
- Hadamard matrices and their applications
