Sciweavers

Share
CADE
2015
Springer

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

3 years 9 months ago
MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
Abstract. 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...
Edward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CADE
Authors Edward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki
Comments (0)
books