MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
DOI10.1007/978-3-319-45641-6_9zbMATH Open1453.05001OpenAlexW2512182535MaRDI QIDQ2829996FDOQ2829996
Krzysztof Czarnecki, Albert Heinle, Curtis Bright, Ilias S. Kotsireas, Saeed Nejati, Vijay Ganesh
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
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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Magma algebra system. I: The user language
- The Lean Theorem Prover (System Description)
- MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
- 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
Recommendations
- Title not available (Why is that?) ๐ ๐
- Title not available (Why is that?) ๐ ๐
- versat: A Verified Modern SAT Solver ๐ ๐
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ๐ ๐
- Satisfiability Checking: Theory and Applications ๐ ๐
- Optimal satisfiability checking for arithmetic \(\mu\)-calculi ๐ ๐
- $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ๐ ๐
- CalcCheck: a proof checker for teaching the ``Logical approach to discrete math ๐ ๐
- Satisfiability Checking of Non-clausal Formulas Using General Matings ๐ ๐
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)
