Distributed and Trustworthy Automated Reasoning

Presented as part of the 2020 HCSS conference. 

Distributed automated reasoning has become increasingly powerful and popular. This enabled solving very hard problems ranging from determining the correctness of complex systems to answering long-standing open questions in mathematics. The tools are based on a portfolio of solvers that share information or divide-and-conquer. The portfolio approach is effective on large formulas from industry, while divide-and-conquer shines on hard-combinatorial problems. Recently distributed solvers competed for the first time, with each tool running on 1600 cores in the Amazon cloud.

The talk presents an overview of progress in distributed automated reasoning and covers some successes, including the solutions---with proofs---of the Boolean Pythagorean Triples problem and Keller's conjecture. The proofs are gigantic, but they have been validated using a formally-verified proof checker. These results underscore the effectiveness of distributed automated reasoning to solve hard challenges arising in mathematics and elsewhere, while having stronger guarantees of correctness than pen-and-paper proofs.

Marijn Heule is an Associate Professor at Carnegie Mellon University and received his PhD at Delft University of Technology (2008). His contributions to automated reasoning have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning SAT solvers and his preprocessing and proof producing techniques are used in many state-of-the-art solvers.