Chapter II 0-1 Integer Programming

Modeling in MiniZinc

MiniZinc is a constraint language that compiles to whatever solver you have — Gecode, Chuffed, OR-Tools, Gurobi.

01

Declare your variables and their domains up front. The language separates modeling (what the problem is) from solving (which engine attacks it) — a single .mzn model runs on every supported backend.
```
int: n = 4;
array[1..n] of var 0..1: x;
```
02

State constraints in something close to ordinary mathematics. MiniZinc handles the encoding to whatever the solver speaks underneath — clauses for SAT, linear forms for LP/MIP, propagators for CP.
```
constraint x[1] + (1 - x[2]) + x[3] >= 1;
constraint x[2] + x[3] + x[4] >= 1;
constraint (1 - x[1]) + (1 - x[4]) >= 1;
```
03

Add an objective if you want optimization rather than feasibility. Drop the "solve minimize ..." line and you get back to plain SAT-as-IP: just find any solution.
```
solve minimize sum(i in 1..n)(x[i]);

output [ "x = ", show(x), "\n" ];
```
04

Run it. minizinc --solver gecode model.mzn returns the optimal 0/1 assignment, or UNSATISFIABLE if no assignment satisfies the constraints.
```
$ minizinc --solver gecode model.mzn
x = [1, 0, 1, 0]
----------
==========
```

Grammar — MiniZinc

MiniZinc is a modeling language. You write what the problem is — variables, constraints, an objective — and a separate solver (Gecode, Chuffed, Gurobi) attacks it. The .mzn file is portable across solvers.

int: n = 4;: a parameter — a known constant, set before solving. Type comes first, then name, then value.
var 0..1: a decision variable with the given domain. The solver chooses its value.
array[1..n] of var T: a fixed-size array of n decision variables, each of type T. Indexing is 1-based.
constraint EXPR;: assert that EXPR must hold in any solution. Stack as many as you need.
forall (i in 1..n) (...): quantification over a range. Pair with sum, exists, or another forall.
solve satisfy;: find any feasible assignment. solve minimize EXPR; or maximize EXPR; turns it into optimization.
output [...]: a list of strings to print on a solution. show(x) formats a variable.
/\ \/ not: AND, OR, and negation on Booleans. Relations >=, <=, =, != come from the math side.

Take the SAT clause (a ∨ ¬b ∨ c). Each Boolean becomes a 0-1 integer; the OR becomes a single linear inequality.

array[1..3] of var 0..1: x;
% the clause becomes one linear constraint:
constraint x[1] + (1 - x[2]) + x[3] >= 1;
solve satisfy;
output [ "x = ", show(x), "\n" ];

MiniZinc — docs and tutorials →