MathCheck

MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers. We present a method and an associated system, called MathCheck, that embeds the functionality of a computer algebra system (CAS) within the inner loop of a conflict-driven clause-learning SAT solver. SAT+CAS systems, a la MathCheck, can be used as an assistant by mathematicians to either counterexample or finitely verify open universal conjectures on any mathematical topic (e.g., graph and number theory, algebra, geometry, etc.) supported by the underlying CAS system. Such a SAT+CAS system combines the efficient search routines of modern SAT solvers, with the expressive power of CAS, thus complementing both. The key insight behind the power of the SAT+CAS combination is that the CAS system can help cut down the search-space of the SAT solver, by providing learned clauses that encode theory-specific lemmas, as it searches for a counterexample to the input conjecture (just like the T in DPLL(T)). In addition, the combination enables a more efficient encoding of problems than a pure Boolean representation.{par}In this paper, we leverage the graph-theoretic capabilities of an open-source CAS, called SAGE. As case studies, we look at two long-standing open mathematical conjectures from graph theory regarding properties of hypercubes: the first conjecture states that any matching of any d-dimensional hypercube can be extended to a Hamiltonian cycle; and the second states that given an edge-antipodal coloring of a hypercube, there always exists a monochromatic path between two antipodal vertices. Previous results have shown the conjectures true up to certain low-dimensional hypercubes, and attempts to extend them have failed until now. Using our SAT+CAS system, MathCheck, we extend these two conjectures to higher-dimensional hypercubes. We provide detailed performance analysis and show an exponential reduction in search space via the SAT+CAS combination relative to finite brute-force search. (new: MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures)


References in zbMATH (referenced in 11 articles , 2 standard articles )

Showing results 1 to 11 of 11.
Sorted by year (citations)

  1. Bright, Curtis; Kotsireas, Ilias; Heinle, Albert; Ganesh, Vijay: Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT (2021)
  2. Bright, Curtis; Cheung, Kevin; Stevens, Brett; Roy, Dominique; Kotsireas, Ilias; Ganesh, Vijay: A nonexistence certificate for projective planes of order ten with weight 15 codewords (2020)
  3. Bright, Curtis; Kotsireas, Ilias; Ganesh, Vijay: Applying computer algebra systems with SAT solvers to the Williamson conjecture (2020)
  4. Bright, Curtis; Kotsireas, Ilias; Ganesh, Vijay: New infinite families of perfect quaternion sequences and Williamson sequences (2020)
  5. Bright, Curtis; Đoković, Dragomir Ž.; Kotsireas, Ilias; Ganesh, Vijay: The SAT+CAS method for combinatorial search with applications to best matrices (2019)
  6. Huang, Pei; Liu, Minghao; Ge, Cunjing; Ma, Feifei; Zhang, Jian: Investigating the existence of orthogonal golf designs via satisfiability testing (2019)
  7. Bright, Curtis; Kotsireas, Ilias; Heinle, Albert; Ganesh, Vijay: Enumeration of complex golay pairs via programmatic SAT (2018)
  8. Wang, Fan; Zhao, Weisheng: Matchings extend to Hamiltonian cycles in 5-cube (2018)
  9. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  10. Bright, Curtis; Ganesh, Vijay; Heinle, Albert; Kotsireas, Ilias; Nejati, Saeed; Czarnecki, Krzysztof: \textscMathCheck2: a SAT+CAS verifier for combinatorial conjectures (2016)
  11. Zulkoski, Edward; Ganesh, Vijay; Czarnecki, Krzysztof: MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers (2015)


Further publications can be found at: https://uwaterloo.ca/mathcheck/publications