Massively Parallel Solving of Math Problems

VCLA hosted a talk by Marijn Heule

ABSTRACT

Progress in satisfiability (SAT) solving has enabled determining the correctness of complex systems and answering long-standing open questions in mathematics. The SAT solving approach is completely automatic and can produce clever though potentially gigantic proofs. This technology will become increasingly important to verify security and safety properties of critical systems. Moreover, we can have confidence in the correctness of the answers, because highly trustworthy systems can validate the underlying proofs regardless of their size.

Martin Heule illustrates the success of the completely automatic SAT solving approach by presenting the solutions of two hard math problems: the Boolean Pythagorean Triples problem and the Schur Number Five problem. Since the 1980s one of the problems which solution has been eluding mathematicians was the Boolean Pythagorean triples problem. The problem was solved in 2016 by Marijn Heule with the largest mathematical proof in the history for which generation a supercomputer needed 2 days. The proof needed to be checked for correctness by a computer as a human check would demand about 30,000 hours of one´s life. However, the enormous size of these proofs is not important - in fact, shorter proofs would have been preferable. Still, its size shows that automated tools, combined with supercomputing, facilitate solving bigger problems. At the same time, a question arises: is there a way for a prompter human check of the mathematical proofs generated by a computer?

Marijn Heule, University of Texas at Austin

BIO

Marijn Heule is a Research Assistant Professor at the University of Texas at Austin whose research focuses on major challenges in automated reasoning. Marijn Heule´s current research focusses on two major challenges for SAT solving. The first challenge is the exploitation of the potential of high-performance computing. The second is validating the results of SAT solvers and related tools. His computer-aided solutions of long-standing mathematical problems such as the Pythagorean Triples Problem and the computation of the fifth Schur Number have received substantial media coverage.

In 2018 Marijn Heule, and Benjamin Kiesl and Adrian Rebola-Pardo (PhD students of the FWF-funded doctoral college Logical Methods in Computer Science – LogiCS at TU Wien) received the Best Paper Award at the premier international conference on all topics in automated reasoning, IJCAR 2018 in Oxford, UK. The best paper award recognizes the originality and significance of the awarded paper “Extended Resolution Simulates DRAT”, which for the first time provides a mathematical argument showing that Tseitin’s old system of proof checking was actually already powerful enough to do everything that can be done by modern approaches. The paper finally bridges the gap between proofs of the present and of the past, thereby helping the humans to actually better understand computer-generated proofs.