How I write MiniZincDRAFT

I like writing MiniZinc models. I think it is a nice language, and I have been using it for as long as it has existed. It lets me describe an optimisation problem directly, in a form that I can still read as the model grows.

How I write a model includes how I organise its data, choose types, and express the rules, as well as how I lay out the source. These choices have developed over years of using MiniZinc and reflect my own preferences.

How I use MiniZinc#

I use MiniZinc to understand problems, solve them and experiment with different approaches, sometimes as part of my research.

Prototyping a problem. MiniZinc is often where I start when modelling a new problem. Writing down the decisions, constraints and objective gives me a formulation to experiment with while I am still working out the details. The model is usually concise enough to read through as a whole.

Solving small puzzles. I am a big fan of modelling and solving small puzzles. Their rules usually fit into a small model, so I can try a formulation, check that it captures the rules and see how difficult it is to solve. My post From constraint models to playable puzzle games includes MiniZinc models for several of the puzzles on this site, and my LinkedIn Queens post shows how to solve LinkedIn Queens and Star Battle with MiniZinc.

Experimenting with different solvers. With MiniZinc, I can compare different solvers and search strategies using the same formulation. I don’t have to rewrite the model in each solver’s own language. My LinkedIn Queens benchmarking post goes into these experiments in more detail.

Solving real problems. I have used MiniZinc for experiments at Optischedule, as well as in consulting work.

On one consulting engagement, a team had built an in-house solver for a scheduling problem and wanted an external check of how well it performed. During a workshop over a couple of days, they described the problem and I wrote a MiniZinc model as we talked. Writing the model during the discussion let us check the scheduling rules against the source as we went. The names and constraint blocks had to be understandable while we were still working out the details.

Contributing problems to the MiniZinc Challenge. I also submit problems to the MiniZinc Challenge. Contributing models has been a substantial part of my work with MiniZinc over the years, alongside working on constraint solvers.¹

Give the source room to explain the problem#

MiniZinc often appears in academic papers, where there are few lines to spare and each line must fit the column. Syntax highlighting is often limited too. A compact listing can be a reasonable way to present a formulation under those conditions.

I think those constraints have influenced how a lot of MiniZinc source is written. For a model that I will read, change and debug, I want the same care I would give any other program. I am happy to use more space when it makes the problem easier to see.

For example, a weekly limit on working hours could be written like this:

constraint forall(w in W)(sum(d in D)(h[w,d]) <= l[w]);

Giving the expression more room already helps:

constraint forall (w in W) (
    sum (d in D) (h[w, d]) <= l[w]
);

I can now see the universal quantifier and its body separately, though I still have to remember what h and l mean. Better names and an explanation of the rule would help more.

Names and structure that follow the problem#

I use snake_case for parameters, decision variables, record fields, functions and predicates, and UpperCamelCase for enums, types, enum constructors and named sets or domains.² That gives Worker and Days visibly different roles from assigned_shift and weekly_limit.

Within those conventions, I prefer words from the problem. In the constraint above, weekly_limit tells me more than l, and a generator binding named worker is easier to follow through a longer expression.

I generally organise model files into short, commented sections for data, validation, derived data, decision variables, constraints, and the objective and output. A small model may only need a few of these. I keep data validation close to the declarations so the assumptions are easy to find. Derived quantities come before the decisions and constraints, so I can see how a bound was obtained before seeing it used.

Constraints as units of explanation#

With descriptive names, a comment and a short string label, the weekly-hours rule reads in the language of the problem.³

% A worker may be within each day's limit and still exceed their weekly allowance in aggregate.
constraint :: "Weekly hours respect worker limits"
forall (worker in Worker) (
    sum (day in Days) (hours[worker, day]) <= weekly_limit[worker]
);

The label gives the rule a short name. The comment explains why checking individual days is insufficient. I use this combination for non-trivial constraints, with longer comments when a rule needs more explanation. For simpler cases, the label is often enough.

MiniZinc’s FindMUS tool can use named constraints when investigating an unsatisfiable model. The label then helps me identify which scheduling rule is involved.

For layout, I like four-space indentation and a maximum line width of 120 columns. Within expressions, I use indentation to show the nesting. I mostly give forall expressions an expanded body, so the rule stands below the domain it applies to. Conjunctions usually go on separate lines. Short sum expressions mostly stay on one line. String labels get their own line, with the constraint expression at the same indentation as constraint.

I also like aligned matrix columns when they help me read tabular data. I avoid aligning unrelated declarations into columns, because changing one long name then moves every neighbouring declaration.

Use the language as it evolves#

MiniZinc has changed substantially since its beginnings. I particularly appreciate the additions that let me give problem concepts their own types and keep related data together.

Enums and records#

If the problem has workers and kinds of shifts, I can give those concepts types:

enum Worker = {Ada, Bo};
enum ShiftType = {Day, Evening, Off};
array[Worker] of var ShiftType: assigned_shift;

I no longer need a separate explanation that worker 1 is Ada or that shift 3 means a day off. Arrays can use the enum directly as their index set, and the compiler can distinguish a worker from a shift type.

Records are useful when several values describe the same thing:

type ShiftData = record(int: duration_hours, int: required_workers);
array[ShiftType] of ShiftData: shift_info = [
    Day: (duration_hours: 8, required_workers: 2),
    Evening: (duration_hours: 6, required_workers: 2),
    Off: (duration_hours: 0, required_workers: 0),
];

shift_info[Day].duration_hours gives me the duration of the day shift. The array is indexed by ShiftType, with each entry named explicitly. Duration and required staffing belong to the same shift description, so a record keeps them together.

Absence and defaults#

An optional value lets me represent genuine absence without reserving an ordinary number such as -1. In limits.mzn, I declare the input and the fallback:

opt int: supplied_limit;
int: effective_limit = supplied_limit default 40;

The data file limits.dzn specifies that no limit was supplied:

supplied_limit = <>;

With this data, the effective limit is 40. Another data file can supply a specific limit without changing the model.

Arrays with their indices attached#

Indexed constructions let me keep the index and the value together:

set of int: Days = 1 .. 2;
set of int: Periods = 1 .. 3;
array[Days, Periods] of int: demand = [ (day, period):
    day + period
  | day in Days,
    period in Periods
];

The expression constructs a two-dimensional array directly, with days and periods as its indices. I don’t need to make a flat list and reshape it with array2d. The index order is visible beside the value being constructed.

More recent additions include named arguments and index-dependent array domains. For example, different jobs can have different upper bounds on their start times in the declaration itself:

set of int: Jobs = 1 .. 3;
array[Jobs] of int: latest_start = [4, 7, 9];
array[job in Jobs] of var 0 .. latest_start[job]: start;

If a job cannot start after latest_start[job], that bound belongs in its domain. An unnecessarily broad var int withholds information I already have from both the reader and the solver.

The MiniZinc change log records how these features arrived over several releases, from enums in 2016 to index-dependent domains in 2026. My style has changed with them. The examples here use MiniZinc 2.10.1.

Make assumptions and modelling choices explicit#

If a model assumes nonnegative limits, I want that assumption checked:

constraint :: "Weekly limits are nonnegative"
assert(
    forall (worker in Worker) (
        weekly_limit[worker] >= 0
    ),
    "Every weekly limit must be nonnegative",
);

The assertion identifies invalid input before I spend time investigating why a schedule cannot be found. I use assertions to check assumptions about ranges, dimensions, indices and compatibility that the rest of the model relies on.

I use standard global constraints when they express a relation clearly. For example, all_different gives a familiar name to a collection of pairwise distinct values. While it is possible to include individual global constraints, I generally start a model with include "globals.mzn";.

I extract a function or predicate when a recurring or complicated rule has a useful name in the language of the problem, and pass the data and decisions it needs as arguments. That makes its dependencies visible at the call site.

I wrap redundant strengthening constraints in implied_constraint(...) and symmetry breakers in symmetry_breaking_constraint(...), keeping their comments and string labels. The wrappers make those modelling decisions visible and can also be used by some solvers.

Keep experiments separate from the formulation#

When I try several objectives or search strategies, I keep the shared formulation in a base model. Each experiment gets a small wrapper with an include, its additional declarations or constraints, and its solve item and search annotations:

include "scheduling-base.mzn";

solve minimize total_overtime;

That keeps me from copying a whole model and gradually letting the copies diverge. A solver-specific annotation belongs in the relevant wrapper rather than throughout the shared formulation.

I check representative instances with different solvers, typically Gecode, OR-Tools CP-SAT and Huub. When appropriate, I also try relax_and_reconstruct with Gecode and restart settings for a simple large neighbourhood search (LNS).⁴ I use comparable instances and limits, and distinguish a run that found a good solution from one that proved optimality.

Zincite#

Manual formatting is tedious, especially when agents write large parts of the code and I have to fix the style afterwards. I started building Zincite to automate formatting according to my preferences. Zincite also supports linting, which can give agents feedback on the models they write, including the naming and constraint-label conventions described here. The formatter handles layout, while lint suggestions can prompt a closer look at modelling choices, such as whether an integer set would be clearer as an enum.

I have now released Zincite 0.1.0, the first published version. Zincite is still in early development. It provides zincite fmt, zincite lint and zincite query for MiniZinc model (.mzn) and data (.dzn) files, without invoking a MiniZinc compiler or solver. Expect changes to formatting and interfaces, including changes that break existing workflows.

Formatting#

zincite fmt produces the layouts shown above, apart from the deliberately compact example. It expands forall bodies in constraints, aligns matrix columns and sorts adjacent include groups with globals.mzn first. Comments, names and literal spelling are preserved.

Print a formatted file, check a directory, or write formatting changes to explicit files:

zincite fmt model.mzn
zincite fmt --check models/
zincite fmt --write model.mzn data.dzn

The formatting guide shows the choices in more detail, and the site has a format-on-save recipe. The same formatter can run after an agent edits a file, so formatting happens automatically. I have been aiming for formatting to take less than 100 ms for a typical MiniZinc file.

Linting#

zincite lint runs six checks by default. It checks naming conventions and constraint labels, and recommends direct array comprehensions where appropriate. It also checks for incompatible array indices, shadowed names and partial expressions such as division by zero or access outside an array’s index set.

For a small example, save this as model.mzn:

var 0 .. 40: weekly_hours;
constraint weekly_hours <= 32;
solve satisfy;

Run the label check on its own:

$ zincite lint --rules missing-constraint-label model.mzn
[root model.mzn] model.mzn:2:1: bytes 27..37: warning [missing-constraint-label]: consider adding a string label to explain this constraint's modelling intent
  |
2 | constraint weekly_hours <= 32;
  | ^^^^^^^^^^

An agent can use that feedback to give the constraint a meaningful label. I still need to review whether the explanation and the constraint agree, with or without an agent’s help.

There are 28 rules in total, with presets for concerns such as arrays, domains and search. Optional checks include hidden optional values and unbounded decision variables; some draw on Erik Rimskog’s A Linter for Static Analysis of MiniZinc Models. The linting guide covers model and standard-library setup, rule selection and the fixes Zincite can offer.

Asking questions about a model#

As a model grows, I also want to ask questions about its structure. zincite query has a pipeline language for selecting source items and working with the results. For the small model.mzn above:

zincite query 'filter(kind("constraint")) | count' model.mzn

This prints 1, the number of constraint items written in that file. Queries can also find uses of declarations, build reports and transform data instances, for example to make a smaller instance for investigation.

The query guide and cookbook have more examples. The query language is particularly early in development, so I expect substantial changes there.

Trying Zincite#

To try Zincite 0.1.0, install it from crates.io with a current stable Rust toolchain:

cargo install --locked --version '=0.1.0' zincite

Zincite targets MiniZinc 2.10.1. The support guide describes the limits of its analysis.

The 0.1.0 release notes describe the release. The project site has the guides and examples, and the source is on GitHub. Start with zincite fmt model.mzn, then try the lint rules on a model you know well.