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

Zulkoski, Edward; Ganesh, Vijay; Czarnecki, Krzysztof

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

Edward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki

Download BibTeX Cite

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Pages 4228-4232.

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. We demonstrate the efficacy of our approach on a long-standing open conjecture regarding matchings of hypercubes.

Edward Zulkoski, Vijay Ganesh, and Krzysztof Czarnecki. 2016. MATHCHECK: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16. IJCAI, 4228–4232. https://ijcai.org/proceedings/2016/636

@inproceedings{ijcai2016p636,
  title     = {MATHCHECK: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers},
  author    = {Zulkoski, Edward and Ganesh, Vijay and Czarnecki, Krzysztof},
  booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-16}},
  publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
  editor    = {Subbarao Kambhampati},
  pages     = {4228--4232},
  year      = {2016},
  month     = {7},
  url       = {https://ijcai.org/proceedings/2016/636},
}

TY  - CPAPER
TI  - MATHCHECK: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
AU  - Zulkoski, Edward
AU  - Ganesh, Vijay
AU  - Czarnecki, Krzysztof
T2  - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16
PB  - AAAI Press / International Joint Conferences on Artificial Intelligence
PY  - 2016
SP  - 4228
EP  - 4232
UR  - https://ijcai.org/proceedings/2016/636
ER  -