MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures

DOI10.1007/978-3-319-45641-6_9zbMath1453.05001OpenAlexW2512182535MaRDI QIDQ2829996

Krzysztof Czarnecki, Albert Heinle, Curtis Bright, Saeed Nejati, Vijay Ganesh, 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

Mathematics Subject Classification ID

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)

Related Items (6)

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 ⋮ The SAT+CAS method for combinatorial search with applications to best matrices ⋮ Applying computer algebra systems with SAT solvers to the Williamson conjecture ⋮ MathCheck ⋮ Investigating the existence of Costas Latin squares via satisfiability testing

Uses Software

• Coq
• Magma
• Maple
• Mathematica
• REDUCE
• SageMath
• SINGULAR
• Chaff
• veriT
• Hadamard
• Lean
• nsoks

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constraint models for the covering test problem
• Williamson matrices up to order 59
• The Magma algebra system. I: The user language
• Williamson matrices of order \(4n\) for \(n = 33, 35, 39\)
• Compression of periodic complementary sequences and applications
• 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
• On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers
• A SAT Attack on the Erdős Discrepancy Conjecture
• The Lean Theorem Prover (System Description)
• MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
• Construction of Williamson type matrices
• On Orthogonal Matrices
• Hadamard matrices and their applications

This page was built for publication: MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures