Abstract: Mixed-integer linear programming is an optimization paradigm with a wide range of applications. Most software to solve these problems is based on inexact floating-point computation, which sometimes leads to erroneous results. Although it is possible to compute exact solutions by using exact precision arithmetic in all steps of the algorithms, this slows computation time considerably. Modern techniques for computing exact solutions employ a combination of numerical methods, interval arithmetic, and exact computation in novel ways to increase speed while still guaranteeing correct results. This talk will survey some of these methods and further describe how their computed results can be independently validated. In particular, how solvers can be adapted to output a proof of their conclusions using a limited number of simple inference rules which can be verified by a separate program that is much simpler than the optimization solver. This talk is based on joint work with Kevin K.H. Cheung and Ambros Gleixner.

Bio: Dan Steffy is an associate professor in the Department of Mathematics and Statistics at Oakland University. He earned his PhD in Algorithms, Combinatorics and Optimization from Georgia Tech in 2010, and has spent time as a research staff member at the Zuse Institute Berlin. His research interests include integer programming, computational optimization, graph theory and applications.