Solving Hard Problems Automatically

No matter what scientific field we look at today, there is no lack of hard problems whose solutions seem completely out of reach. In mathematics alone, we can easily find countless questions that have been open for decades; but also in computer science and biology, researchers have been looking at problems that, so far, have brought even the greatest minds to their knees. Many of these problems are not only of theoretical interest, their solutions would also have significant practical implications.

Luckily, we are now at a point where automated reasoning has become mature enough to help us solve these problems. In my talk, I show how automated reasoning techniques have been crucial in tackling hard open problems from various fields, including mathematics, bioinformatics, and software engineering. I focus on several of my contributions, including mechanizing abstract reasoning and effectively parallelizing the big computations. I also address the issue of why we can have confidence in the correctness of the answers produced by today's automated reasoning tools. To complete the picture, I discuss popular open problems whose solutions could potentially be obtained by capitalizing on the power of automated reasoning.
Marijn Heule is a Research Assistant Professor at the University of Texas at Austin who received his PhD at Delft University of Technology (2008). His contributions to automated reasoning have enabled him and others to solve hard problems from various fields such as formal verification and mathematics. He has developed award-winning automated reasoning engines and his techniques are nowadays used in many state-of-the-art tools.