Solving Combinatorial Problems Without Knowing How to Solve Them
Speaker
Pierre Flener
Date and Time
Friday, November 30th, 2018 at 14:15.
Location
Polacksbacken, ITC, room 1111.
Abstract
Solving technologies for combinatorial problems abound: mixed-integer programming (MIP), Boolean satisfiability (SAT), satisfiability modulo theories (SMT), constraint programming (CP), local search, etc, and hybrids. No technology dominates the others or shares a modelling language with them. Unbeknownst to many, it has become possible to model the constraints (and objective function) of a combinatorial problem upon learning a single fully declarative high-level modelling language and, upon experiments with solvers of different technologies, to choose a winning technology and solver, without knowing (in depth) how the solvers work.
I present one such language, MiniZinc, to the toolchain of which my research group contributes. I show how the high-level MiniZinc abstractions of common combinatorial structures enable very readable short models of complex problems. These abstractions are directly reasoned upon by CP and SMT solvers, sometimes with great effect, but translated for MIP solvers into linear (in)equalities over integer variables, and for SAT solvers into clauses over Boolean variables. This allows MIP and SAT modellers to reuse well-known encodings systematically rather than tediously or erroneously rediscovering them.
For most managers, engineers, and scientists, the time to achieve a particular solution speed or quality is drastically reduced by such model-once-solve-everywhere toolchains.
Speaker Bio
Pierre Flener is a professor of Computing Science. A short bio is here.