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 this approach by presenting the solutions of two hard math problems: the Boolean Pythagorean Triples problem and the Schur Number Five problem. He constructed and validated proofs of the solutions, which are 200 terabytes and 2 petabytes in size, respectively. The former has been called “the largest math proof ever.” 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.

ABOUT THE SPEAKER

Marijn Heule is a Research Assistant Professor at the University of Texas 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.

BEST PAPER AWARD AT IJCAR 2018

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.

Links

• Marijn Heule: Massively Parallel Solving of Math Problems

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.

Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!