SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics
Curtis Bright, Ilias Kotsireas, Vijay Ganesh

TL;DR
This paper discusses the integration of SAT solvers with computer algebra systems (CASs) to enhance mathematical problem solving, demonstrating success in disproving and verifying conjectures and discovering new algorithms.
Contribution
It introduces the SAT+CAS paradigm, combining search efficiency of SAT solvers with deep mathematical knowledge of CASs, and showcases its effectiveness through the MathCheck tool.
Findings
Successfully disproved and verified multiple mathematical conjectures.
Discovered new algorithms for 3x3 matrix multiplication.
Demonstrated the paradigm's potential as a standard method in mathematical problem solving.
Abstract
Over the last few decades, many distinct lines of research aimed at automating mathematics have been developed, including computer algebra systems (CASs) for mathematical modelling, automated theorem provers for first-order logic, SAT/SMT solvers aimed at program verification, and higher-order proof assistants for checking mathematical proofs. More recently, some of these lines of research have started to converge in complementary ways. One success story is the combination of SAT solvers and CASs (SAT+CAS) aimed at resolving mathematical conjectures. Many conjectures in pure and applied mathematics are not amenable to traditional proof methods. Instead, they are best addressed via computational methods that involve very large combinatorial search spaces. SAT solvers are powerful methods to search through such large combinatorial spaces---consequently, many problems from a variety of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPolynomial and algebraic computation · Logic, programming, and type systems · Numerical Methods and Algorithms
MethodsPruning
