<p>Here are the systems/languages I know of for representing these kinds of problems at a higher level of abstraction:</p>
<ul>
<li><p>The <a href="https://en.wikipedia.org/wiki/Z3_Theorem_Prover" rel="nofollow noreferrer">Z3 solver</a> has higher-level constructs for words (fixed-length bit-strings), arithmetic over them, arrays, <a href="https://stackoverflow.com/q/43081929/781723">pseudo-boolean constraints</a>, and more.  It translates to SAT instead of MILP.</p>
</li>
<li><p><a href="https://www.sagemath.org/" rel="nofollow noreferrer">Sage</a>, also known as SageMath, has a very convenient programming interface for expressing MILP problems.  Check out <a href="https://doc.sagemath.org/html/en/reference/numerical/sage/numerical/mip.html" rel="nofollow noreferrer">their reference docs</a> and <a href="https://doc.sagemath.org/html/en/thematic_tutorials/linear_programming.html" rel="nofollow noreferrer">these examples</a>.  It is super-convenient for expressing these problems elegantly in a Python-like language.</p>
</li>
<li><p><a href="https://en.wikipedia.org/wiki/AMPL" rel="nofollow noreferrer">AMPL</a> is a language for expressing optimization and constraint problems, including MILP problems and others, at a higher level.  It is supported by many solvers.</p>
</li>
<li><p><a href="https://www.minizinc.org/" rel="nofollow noreferrer">MiniZinc</a> is a solver for <a href="https://en.wikipedia.org/wiki/Constraint_programming" rel="nofollow noreferrer">constraint programming</a> 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.  <a href="https://github.com/MiniZinc/minizinc-python" rel="nofollow noreferrer">minizinc-python</a> provides Python bindings for MiniZinc.</p>
</li>
</ul>

CC BY-SA 4.0
2024-01-05T14:09:49.860Z
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
CC BY-SA 4.0
2024-01-05T14:44:37.320Z
Hah, this seems to be studied: https://dl.acm.org/doi/10.1145/2535838.2535857 https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf
Turion
CC BY-SA 4.0
2024-01-05T14:47:02.213Z
A keyword seems to be "MAX-SMT": https://stackoverflow.com/questions/10602295/how-max-smt-solvers-do-work
Turion
CC BY-SA 4.0
2024-01-05T21:05:51.337Z
@Turion, I have extended my answer with some more pointers.
D.W.
CC BY-SA 4.0
2024-01-05T23:12:23.840Z
This seems to fit the theme: https://github.com/MiniZinc/minizinc-python
cody
CC BY-SA 4.0
2024-01-05T23:21:35.220Z
@cody, very nice, seems very relevant I've added that to my answer!  Thank you!
D.W.
CC BY-SA 4.0
2024-01-07T12:14:01.377Z
Yes, minizinc is a lot like what I was looking for! Thanks! (https://www.minizinc.org/doc-2.8.2/en/predicates.html#defining-functions)
Turion
CC BY-SA 4.0
2023-12-20T18:31:02.147Z
2024-01-05T23:21:21.367Z
2024-01-05T23:21:21.367Z
D.W.
<p>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.</p>
<p>For example, a typical concept I've come across is encoding a <em>function</em> <span class="math-container">$f$</span> from a finite set <span class="math-container">$A$</span> to a finite set <span class="math-container">$B$</span>. Typically one does this by declaring binary variables <span class="math-container">$f_{ab}$</span> where <span class="math-container">$a \in A, b \in B$</span>, and constraining <span class="math-container">$\forall a . \sum_b f_{ab} = 1$</span>. So basically, we have encoded a function by its set-theoretic definition. After I have run the solver, I will get values for <span class="math-container">$f_{ab}$</span> and have to decode the function by ranging over every <span class="math-container">$a$</span> and looking up the single assigned value <span class="math-container">$b$</span>.</p>
<p>I want a language where I can simply declare &quot;<span class="math-container">$f$</span> is a function from <span class="math-container">$A$</span> to <span class="math-container">$B$</span>&quot;, and it will do the declaration, the constraints, and the mapping from the optimization result to the actual function.</p>
<p>I might later want to add further constraints, maybe <span class="math-container">$\sum_a f(a) c_a &lt; c$</span>, where <span class="math-container">$c$</span> and <span class="math-container">$c_a$</span> are constants, or add some specific value of <span class="math-container">$f(a_0)$</span> to the optimization goal. So the language should be composable (as far as possible to encode in MILP).</p>
<p>Finally, I would like to be able to define the types like <span class="math-container">$A$</span> and <span class="math-container">$B$</span> myself. In real life applications, these type definitions would typically come from input data used to generate the problem.</p>
<p>In summary, I'm looking for a high level language that compiles to MILP, with these features:</p>
<ul>
<li>Encode language concepts as MILP declarations &amp; constraints</li>
<li>Decode MILP results into values in the language</li>
<li>Define custom types (with finite sets as semantics)</li>
<li>Have useful, general purpose, polymorphic internal types such as functions</li>
<li>Composability, whenever it is expressible in MILP</li>
</ul>
<p>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.</p>

CC BY-SA 4.0
2023-12-20T19:37:45.610Z
related: https://en.wikipedia.org/wiki/AMPL
Neal Young
<pl.programming-languages><linear-programming><functional-programming><compilers>
Is there a high level (functional) language compiling to Mixed Integer Linear Programming problems?
Turion
# Is there a high level (functional) language compiling to Mixed Integer Linear Programming problems?

(Asked by: username_0 on 2023-12-20)

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.

**Tags:** pl.programming-languages, linear-programming, functional-programming, compilers

> **Comments:**
> **username_1**: related: https://en.wikipedia.org/wiki/AMPL  

---

## 1 answers

### Answer by username_2 on 2023-12-20. Score: 5 | Accepted answer

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

* The [Z3 solver](https://en.wikipedia.org/wiki/Z3_Theorem_Prover) has higher-level constructs for words (fixed-length bit-strings), arithmetic over them, arrays, [pseudo-boolean constraints](https://stackoverflow.com/q/43081929/781723), and more. It translates to SAT instead of MILP.
* [Sage](https://www.sagemath.org/), also known as SageMath, has a very convenient programming interface for expressing MILP problems. Check out [their reference docs](https://doc.sagemath.org/html/en/reference/numerical/sage/numerical/mip.html) and [these examples](https://doc.sagemath.org/html/en/thematic_tutorials/linear_programming.html). It is super-convenient for expressing these problems elegantly in a Python-like language.
* [AMPL](https://en.wikipedia.org/wiki/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](https://www.minizinc.org/) is a solver for [constraint programming](https://en.wikipedia.org/wiki/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](https://github.com/MiniZinc/minizinc-python) provides Python bindings for MiniZinc.

> **Comments:**
> **username_0**: 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.  
> **username_0**: Hah, this seems to be studied: https://dl.acm.org/doi/10.1145/2535838.2535857 https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf  
> **username_0**: A keyword seems to be "MAX-SMT": https://stackoverflow.com/questions/10602295/how-max-smt-solvers-do-work  
> **username_2**: @username_0, I have extended my answer with some more pointers.  
> **username_3**: This seems to fit the theme: https://github.com/MiniZinc/minizinc-python  
> **username_2**: @username_3, very nice, seems very relevant I've added that to my answer!  Thank you!  
> **username_0**: Yes, minizinc is a lot like what I was looking for! Thanks! (https://www.minizinc.org/doc-2.8.2/en/predicates.html#defining-functions)  

---

