MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers

DOI10.1007/978-3-319-21401-6_41zbMath1465.68300OpenAlexW2233119526MaRDI QIDQ3454125

Edward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_41

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Graph theory (including graph drawing) in computer science (68R10) Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.) (05C70) Coloring of graphs and hypergraphs (05C15) Eulerian and Hamiltonian graphs (05C45) Software, source code, etc. for problems pertaining to combinatorics (05-04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (8)

Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ Matchings extend to Hamiltonian cycles in 5-cube ⋮ Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions ⋮ The SAT+CAS method for combinatorial search with applications to best matrices ⋮ Applying computer algebra systems with SAT solvers to the Williamson conjecture ⋮ MathCheck ⋮ MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures ⋮ A nonexistence certificate for projective planes of order ten with weight 15 codewords

Uses Software

• SageMath
• z3
• veriT
• CPGraph
• CVC4
• Lynx
• sharpSAT

Cites Work

• Unnamed Item
• Unnamed Item
• Perfect matchings extending on subcubes to Hamiltonian cycles of hypercubes
• Perfect matchings extend to Hamilton cycles in hypercubes
• On hypercube labellings and antipodal monochromatic paths
• SAT Modulo Graphs: Acyclicity
• Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
• A SAT Attack on the Erdős Discrepancy Conjecture
• CP(Graph): Introducing a Graph Computation Domain in Constraint Programming
• Connectivity of Matching Graph of Hypercube
• Hamilton Cycles that Extend Transposition Matchings in Cayley Graphs of $S_n $
• A Decision Procedure for Bit-Vectors and Arrays
• Poly-logarithmic deterministic fully-dynamic algorithms for connectivity, minimum spanning tree, 2-edge, and biconnectivity
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers