MIP Engines are Saturation Engines Too
Talk by Diego Olivier Fernandez Pons
Abstract: Saturation-based theorem provers use heuristics to create and delete formulas. Mixed integer programming engines used in mathematical optimization, while based on DPLL, also are saturation-based theorem provers for systems of integer linear equations. The algorithm that guides and supports the formula generation is the LP while the formulas are generated by the cutting-planes heuristics in a process globally known as the separation problem. We will show the similarities and differences between saturation-based theorem provers and MIP engines, and try to identify research directions that could benefit both communities.
Bio: Diego Olivier Fernandez Pons started his career in ILOG R&D working on MIP and Constraint Programming engines. Then worked for IBM as an optimization consultant. He is the co-author of OptalCP a constraint programming engine for scheduling problems. And he works today in the quantum group of Microsoft.
