MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures

DOI10.1007/978-3-319-45641-6_9MaRDI QIDQ2829996zbMATH OpenOpenAlexFDO

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

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)

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)

Cites work

• scientific article; zbMATH DE number 1292563 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A SAT attack on the Erdős discrepancy conjecture
• Building bridges between symbolic computation and satisfiability checking
• Compression of periodic complementary sequences and applications
• Constraint models for the covering test problem
• Construction of Williamson type matrices
• Efficient SAT solving under assumptions
• Hadamard matrices and their applications
• Hadamard's determinant theorem and the sum of four squares
• Learning rate based branching heuristic for SAT solvers
• MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
• On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers
• On Orthogonal Matrices
• The CRC handbook of combinatorial designs
• The Lean theorem prover (system description)
• The Magma algebra system. I: The user language
• Williamson matrices of order \(4n\) for \(n = 33, 35, 39\)
• Williamson matrices up to order 59

Cited in

(10)

• Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
• scientific article; zbMATH DE number 7056222 (Why is no real title available?)
• Investigating the existence of Costas Latin squares via satisfiability testing
• SAT and lattice reduction for integer factorization
• Satisfiability modulo user propagators
• MathCheck
• The SAT+CAS method for combinatorial search with applications to best matrices
• Applying computer algebra systems with SAT solvers to the Williamson conjecture
• MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
• Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT

Describes a project that uses

Uses Software

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

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)