MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
DOI10.1007/978-3-319-45641-6_9zbMATH Open1453.05001OpenAlexW2512182535MaRDI QIDQ2829996FDOQ2829996
Authors: Curtis Bright, Vijay Ganesh, Albert Heinle, Saeed Nejati, Krzysztof Czarnecki, Ilias S. Kotsireas 
Publication date: 9 November 2016
Published in: Computer Algebra in Scientific Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-45641-6_9
Recommendations
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- CalcCheck: a proof checker for teaching the ``Logical approach to discrete math
- Optimal satisfiability checking for arithmetic \(\mu\)-calculi
- scientific article; zbMATH DE number 1323296
- Satisfiability checking: theory and applications
- Satisfiability Checking of Non-clausal Formulas Using General Matings
- scientific article; zbMATH DE number 7056222
- versat: A Verified Modern SAT Solver
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
Symbolic computation and algebraic computation (68W30) Software, source code, etc. for problems pertaining to combinatorics (05-04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- The Magma algebra system. I: The user language
- Title not available (Why is that?)
- The Lean Theorem Prover (System Description)
- MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
- The CRC handbook of combinatorial designs
- Title not available (Why is that?)
- Hadamard matrices and their applications
- On Orthogonal Matrices
- A SAT Attack on the Erdős Discrepancy Conjecture
- Williamson matrices up to order 59
- Williamson matrices of order \(4n\) for \(n = 33, 35, 39\)
- Compression of periodic complementary sequences and applications
- Constraint models for the covering test problem
- Hadamard's determinant theorem and the sum of four squares
- Learning Rate Based Branching Heuristic for SAT Solvers
- Building bridges between symbolic computation and satisfiability checking
- Efficient SAT solving under assumptions
- Construction of Williamson type matrices
- On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers
Cited In (7)
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Title not available (Why is that?)
- Investigating the existence of Costas Latin squares via satisfiability testing
- MathCheck
- The SAT+CAS method for combinatorial search with applications to best matrices
- Applying computer algebra systems with SAT solvers to the Williamson conjecture
- Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT
Uses Software
This page was built for publication: MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829996)
