These are the official rules for the MiniZinc Challenge 2023. Version 1.2.
These rules were last updated on 23 February 2023.
The MiniZinc Challenge 2023 will test solvers on problems written in MiniZinc 2.7.0.
A participant is a person or entity (usually a solver developer) who has notified the challenge organisers of their intent to enter one or more solvers in the challenge. This must be done prior to the final submission date in order for any solver entries to be considered.
An entry is a constraint solver that is installed in a Docker image that uses the MiniZinc
Challenge 2023 image (as provided by the organisers) as its base.
Constraint solvers that have several variants (for example that can alternatively use copying or
trailing, or learning and non-learning solvers), may submit one entry per variant, although the
organisers reserve the right to reject such variations if they are not sufficiently interesting,
(e.g. multiple copies of the same solver with differing parameters).
Before the final submission date, participants must complete an online form (which will be made
available to participants before the initial submission round, or, as soon as possible after
notification of registration, whichever is later) for each prospective entry.
If this is done before the end of the initial submission round, feedback will be given on the
entry with respect to rules conformance and performance. This does not affect the final scoring.
Participants may amend, or add additional entries freely until the final submission date.
The form will collect the following information:
Which competition CLASS(ES) the entry will compete in (see below for details).
A short (1-2 pages) description of the system. This
should include a list of all authors of the system and their present institutional affiliations.
It should also describe any algorithms or data structures that are not standardly used in such
systems.
System descriptions will be posted on the MiniZinc Challenge 2023 website.
Whether the entry may be used by 3rd parties (entities that are not the submitters nor the MiniZinc Challenge organisers) for research purposes.
The repository and tag name for the entry on Docker Hub.
The organisers will test each entry to ensure conformance with the rules, and if conformant, the entry will be run in the challenge, where it will be given a score according to the assessment procedure. If the entry does not conform with the rules, or is otherwise unable to run successfully, the challenge organisers will make a reasonable attempt to contact the participant and notify them so that the issues can be remedied. Nevertheless, the organisers reserve the right to reject an entry if its process proves overly difficult. If an entry requires modification after the final submission date in order to be run in the challenge, the entry may be run at the organisers’ discretion, and disqualified from being awarded prizes.
The results will be announced at CP2023. Participants are encouraged to attend CP2023, but are not required to in order to enter or win.
There will be at most five competition CLASSES depending on how many solvers are entered in each of them:
A challenge entry Docker image must use the MiniZinc Challenge 2023 image (as provided by the
organisers) as its base. The image must be set up such that the default minizinc solver is the
entry’s solver. The entry will be run by executing the minizinc
command using the default
solver for the image with options depending on the entry CLASS.
minizinc -i --output-mode dzn --output-objective <model.dzn> [data.dzn]
minizinc -i --output-mode dzn --output-objective -f <model.dzn> [data.dzn]
minizinc -i --output-mode dzn --output-objective -p 4 <model.dzn> [data.dzn]
FlatZinc solvers must accept the following standard options, and they must be included in the supported
stdFlags
of the solver configuration:
-a
(output all solutions/intermediate solutions), or-i
(output intermediate solutions).One of these options (depending on which appears in the stdFlags
for the solver) will be given
for all optimisation problems (but not for satisfaction problems).
Solvers are free to simply always output intermediate solutions for optimisation problems, and a single solution for satisfaction problems (or whatever is supported by the solver). However, they must still accept one of these flags.
-f
(ignore given search strategy).
Entries competing in the FREE
class are free to always ignore the search strategy, however they must still
accept the -f
flag.
-p <n>
(use the specified number n
of threads and/or cores).PAR
and OPEN
classes must accept the -p
flag.MiniZinc solvers must support the following options
(by placing them in the solver configuration stdFlags
or in extraFlags
for long-form options):
--output-mode dzn
output
) in DZN format.
This option must be supported by the solver.--output-objective
_objective
for optimisation problems.
This option must be supported by the solver.-f
(ignore given search strategy)FREE
class are free to always ignore the search strategy, however they
must still accept the -f
flag.-p <n>
(use the specified number n
of threads and/or cores).PAR
and OPEN
classes must accept the -p
flag.Execution of solvers must not require running Docker with --privileged
.
More details about Docker images and how to create a Docker image with your solver is available here.
Output from FlatZinc solver entries must conform to the FlatZinc 2.7.0 specification.
MiniZinc solver entries must correctly implement the --output-mode dzn
and --output-objective
options (that is, output must exactly match the format that MiniZinc itself would output given
these options).
For optimization problems, if the time limit is exceeded before the final solution is printed then the last complete approximate solution printed will be considered to be the solution for that entry. Note that is important that entries flush the output stream after printing each approximate solution so that timing information is accurate.
During the MiniZinc Challenge 2023 all instances of Docker images will run on a compute server with the following specification:
Except in the Parallel search, Open class, and local search solver using multiple cores, only a single core of one processor will be used for each entry.
Note that during testing of submissions, solvers may be run with a different core/memory
configuration. The environment variables NUM_CPUS
and MEMORY_LIMIT
will be made available to
submission containers giving the number of cores and the memory limit in MiB respectively (these
will be present during testing and when running the Challenge).
Solver entries will be run with models that are compatible with
MiniZinc 2.7.0.
These models will adhere to the following restrictions:
Models may only use following types of variables:
var 1..10: x
),var opt 1..10: x
),var set of 1..10: x
)var bool: x
),var opt bool: x
)var MY_ENUM: x
),var opt MY_ENUM: x
),var set of MY_ENUM: x
)In particular, float variables are not permitted.
In order to facilitate local search entries, ideally a model should wrap symmetry breaking constraints in a predicate “symmetry_breaking_constraint” e.g.,
var 0..100: x :: output;
var 0..100: y :: output;
constraint x + y < 144;
constraint symmetry_breaking_constraint(x <= y);
and redundant constraints in a predicate “redundant_constraint”, e.g.,
array[1..4] of var 0..20: start :: output;
array[1..4] of int: duration = [3, 4, 6, 7];
array[1..4] of int: usage = [6, 3, 5, 3];
constraint cumulative(start, duration, usage, 10);
constraint redundant_constraint(start[1] + dur[1] <= start[3] \/ start[3] + dur[3] <= start[1]);
Each solve item must be annotated with a search strategy, such that fixing all the variables appearing in the search strategy would allow a value propagation solver to check a solution. For example,
var 1..5: x :: output;
var 1..5: y :: output;
var 1..5: z :: output;
constraint x <= y /\ y <= z;
solve :: int_search([x, y, z], input_order, indomain_min, complete)
satisfy;
is correct but not
solve :: int_search([x,z], input_order, indomain_min, complete)
satisfy;
even though most FD solvers would know the second was satisfiable.
For set_search, only the following parameters will be used:
Note that for variable choices ties are broken by taking the earliest variable in the given array. Also note that the decision is reassessed at each choice.
var 1..5: x :: output;
var 1..10: objective :: output;
constraint x > 1 -> objective > 7;
constraint x = 1 -> objective < 3;
solve :: int_search([x, objective], first_fail, indomain_min, complete)
maximize objective;
will first label x = 1
and find maximum value objective = 2
eventually on backtracking to
the choice x = 1
, then setting x >= 2
in most FD solvers will have domains for x :: 2..5
and objective :: 8..10
and this time objective
will be selected as the next variable to
label. A full specification of the available choices is given in the
FlatZinc 2.7.0 specification.
All variables appearing in the search strategy (that is, variables where if all fixed, would
allow a propagation solver to check a solution) must be annotated with output
(or must not
have a right-hand side).
var 1..10: x :: output;
var int: y = x div 2;
var 1..3: z :: output;
constraint y * z = 2;
solve :: int_search([x, z], input_order, indomain_min, complete)
satisfy;
This ensures that we are able to check for the correctness of solutions generated by solvers by
using the options --output-mode dzn
and --output-objective
when running the instance, then
passing the result to a value propagation solver with the original instance.
The benchmarks for MiniZinc Challenge 2023 will be selected by the judges to try to examine some of the breadth of characteristics of FD solvers:
To obtain benchmarks of suitable difficulty we will select only such instances that can be solved by at least one of the participating solvers in a sensible time-frame. For the qualification rounds no such restriction applies.
In order to collect good benchmarks each participant is strongly encouraged to submit one or two MiniZinc models, making use of only the global constraints included in the MiniZinc 2.7.0 library, as well as some (preferably 10 or more) instance files for each model. The instances should range from easy (about a minute) to hard (about 15 minutes) if possible. In addition, the submitter should provide one “toy” instance for testing purposes.
Note that the model must conform to the problem format restrictions above, and the Challenge organisers may make changes to the submitted problems to make them suitable for use in the Challenge.
Submitted problem must be placed under the MIT licence, and each model and data file must begin with a comment which includes the licence, unless otherwise agreed to by the submitter and the challenge organisers.
When solver submissions open, participants will be able to submit their Docker image and get automated feedback on compatibility with the competition hardware, compliance with these rules, and any other matters that may arise. Feedback is provided through an automated test suite, and is subject to a usage quota to prevent abuse of the system.
Participants may update their submission as often as they like until the submission deadline, at which point their latest submission will be taken as their entry to the Challenge. Only entries which pass the automated checks will be entered into the Challenge, except at the discretion of the Challenge organisers.
NOTE that passing the automated test suite does not guarantee eligibility for the Challenge. If there is evidence that the submission does not conform to these rules, the entry may be disqualified even if it passes the automated tests.
The challenge will require solvers to process 100 MiniZinc instances with a run-time limit of 20
minutes (process time) per instances.
NOTE that the MiniZinc to FlatZinc time will be included in this time.
Each solver s is run on problem p and the following information is collected.
There three different scoring procedure: complete, incomplete, and area. For prizes, the complete solver ranking is used.
The complete scoring procedure is based on the Borda count voting system. Each benchmark instance is treated like a voter who ranks the solvers. Each solver scores points equal to the number of solvers that they beat in the ranking (more or less). A solver s scores points on problem p by comparing its performance with each other solver s’ on problem p.
In the case on indistinguishable answers between s and s’, s scores timeUsed(p,s’) / (timeUsed(p,s’) + timeUsed(p,s)) , 0.5 if both finished in 0s. The exception is that if solved(p,s) is false, that is, s fails to find any solution or prove unsatisfiability for problem p it always scores 0 points (even if s’ also similarly fails).
The incomplete scoring procedure is the same as the complete one using the Borda count, but the proved optimal solution by a solver does not count.
The area scoring procedure computes the integral of a step function over the runtime horizon. Intuitively, a solver that quickly finds good solutions performs better than a solver that finds even better solutions, but much later in the solving stage. The step function f is defined as follows for a problem p and a solver s.
The scoring calculations will be done once for each run class: FD search, Free search, Parallel search, Open class, and Local search. Note that if too few solvers are entered in a class then the challenge won’t be run for that class.
The organizers may well run entries in the FD search class on a series of smaller problems to test that they indeed are following the given search strategy. These problems will not accrue points, but may disqualify an entry from the FD search class.
The solvers will be ranked on total points awarded. There will be prizes for the solvers with the highest scores in each of the run classes: FD search, Free search, Parallel search, Open class, and Local search. The organizers may also award prizes to the best solvers on a particular category of problems. Note that if too few solvers are entered in a class then the challenge won’t be run for that class and no prizes will be awarded for that class.
The organizers reserve the right to enter their own systems - or other systems of interest - to the competition, however these will not be eligible for prizes, but still will modify the scoring results. In addition, the organizers reserve the right not to run the challenge on classes with an insufficient number of solver entries.
Return to the MiniZinc Challenge 2023 home page.