Title: Integrating Mixed Integer Optimisation and Logic with Satisfiability Modulo Theories
Speaker: Miten Mistry
Affiliation: Department of Computing – Imperial College London
Location: Room 418 Huxley Building
Time: 5:00pm

Abstract. Mixed integer optimisation problems, especially those involving design or organisation, often have an inherent logical structure. Existing frameworks to model and utilise such structure reformulate the problem into a mixed integer model or make use of specialised constraints. Using the application of two-dimensional bin packing, we explore Satisfiability Modulo Theories (SMT) as a means to exploit logical structure. The logical connectives and reasoning provided by SMT allows us to derive cuts to strengthen a Mixed Integer Linear Programming (MILP) solver and, by using unsatisfiability proofs, identify new ways of traversing the search tree.

About the speaker. Miten Mistry is a PhD student in the Department of Computing (QUADS group) at Imperial College London, under the supervision of Dr Ruth Misener. He received EPSRC HiPEDs CDT funding. He previously obtained a MEng Mathematics and Computer Science degree from Imperial College London.