Is there a high level (functional) language compiling to Mixed Integer Linear Programming problems?

Question

Many different kinds of optimization problems can be expressed as Mixed Integer Linear Programming (MILP). The translation is usually very direct, and one has to encode invariants as constraints in a somewhat tedious and error prone way. Decoding the actual value after the solver run can again be tedious. I'm wondering whether there is a nicer high level intermediate language that can be used to express the problem, and inspect the solution.

For example, a typical concept I've come across is encoding a function $f$ from a finite set $A$ to a finite set $B$. Typically one does this by declaring binary variables $f_{ab}$ where $a \in A, b \in B$, and constraining $\forall a . \sum_b f_{ab} = 1$. So basically, we have encoded a function by its set-theoretic definition. After I have run the solver, I will get values for $f_{ab}$ and have to decode the function by ranging over every $a$ and looking up the single assigned value $b$.

I want a language where I can simply declare "$f$ is a function from $A$ to $B$", and it will do the declaration, the constraints, and the mapping from the optimization result to the actual function.

I might later want to add further constraints, maybe $\sum_a f(a) c_a < c$, where $c$ and $c_a$ are constants, or add some specific value of $f(a_0)$ to the optimization goal. So the language should be composable (as far as possible to encode in MILP).

Finally, I would like to be able to define the types like $A$ and $B$ myself. In real life applications, these type definitions would typically come from input data used to generate the problem.

In summary, I'm looking for a high level language that compiles to MILP, with these features:

• Encode language concepts as MILP declarations & constraints
• Decode MILP results into values in the language
• Define custom types (with finite sets as semantics)
• Have useful, general purpose, polymorphic internal types such as functions
• Composability, whenever it is expressible in MILP

I realize that there is an expression problem here, it will not be feasible to compile an arbitrary high level language to MILP. Rather I'd like to compile a restricted language that allows to express many common optimization problems, and generates fairly idiomatic MILP problems that are not much slower than those written by hand.

• Neal Young: related: en.wikipedia.org/wiki/AMPL

Answer 1

Here are the systems/languages I know of for representing these kinds of problems at a higher level of abstraction:

• The Z3 solver has higher-level constructs for words (fixed-length bit-strings), arithmetic over them, arrays, pseudo-boolean constraints, and more. It translates to SAT instead of MILP.

• Sage, also known as SageMath, has a very convenient programming interface for expressing MILP problems. Check out their reference docs and these examples. It is super-convenient for expressing these problems elegantly in a Python-like language.

• AMPL is a language for expressing optimization and constraint problems, including MILP problems and others, at a higher level. It is supported by many solvers.

• MiniZinc is a solver for constraint programming and optimization. It has support for a broad range of different types of constraints, especially many kinds of discrete constraints, and also MILP-style constraints. minizinc-python provides Python bindings for MiniZinc.

• Turion: That's an interesting approach. One might extend an SMT solver by adding an objective function. What I'm unsure about is whether every SAT problem translates nicely to MILP such that a reasonable objective function will still be linear.
• Turion: Hah, this seems to be studied: dl.acm.org/doi/10.1145/2535838.2535857 microsoft.com/en-us/research/wp-content/uploads/2016/02/…
• Turion: A keyword seems to be "MAX-SMT": stackoverflow.com/questions/10602295/…
• D.W.: @Turion, I have extended my answer with some more pointers.
• D.W.: @cody, very nice, seems very relevant I've added that to my answer! Thank you!