Trustworthy and Distributed Automated Reasoning

Marijn Heule (CMU, USA)

19 June 2023, 16:00-17:00 | ECHO-ARENA | https://collegerama.tudelft.nl/Mediasite/Play/ec7c2bcc758b491b8eb4fc8ed657af8b1d

Abstrat

Automated reasoning has become increasingly powerful over the past decades thanks to algorithmic breakthroughs and expanding processing capabilities. This made possible and popularized its usage in solving very hard problems ranging from determining the correctness of complex systems to tackling long-standing open problems in mathematics. This talk presents an overview of progress in trustworthy and distributed automated reasoning, and covers some of its successes, including the solutions — with proofs — of the Boolean Pythagorean Triples problem and Keller's conjecture. Although some proofs are gigantic, they can be (and have been) independently validated using efficient, formally-verified proof checkers. These results underscore the effectiveness of automated reasoning to solve hard challenges in mathematics and elsewhere, while obtaining stronger guarantees of correctness than pen-and-paper proofs.

Marijn Heule

Marijn Heule is an Associate Professor in the Computer Science Department at Carnegie Mellon University and received his PhD at Delft University of Technology in the Netherlands. His research focuses on solving hard-combinatorial problems in areas such as formal verification, number theory, and extremal combinatorics. Most of his contributions are related to theory and practice of satisfiability (SAT) solving. He has developed award-winning SAT solvers, and his preprocessing techniques are used in state-of-the-art SAT solvers.
His current research focusses on two major challenges for SAT solving: 1) exploiting the potential of high-performance computing; and 2) validating the results of SAT solvers and related tools. He has been developing a novel parallel SAT solving paradigm, called cube-and-conquer, which enables linear time speedups on many hard problems. The first publication on cube-and-conquer won the best paper award at HVC 2011.

Deel deze pagina: