MiniZinc Challenge 2023  Rules
These are the official rules for the MiniZinc Challenge 2023. Version 1.4.
These rules were last updated on 20 June 2023.
Solver Submission
The MiniZinc Challenge 2023 will test solvers on problems written in MiniZinc 2.7.6.
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 nonlearning 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 (12 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.
Competition classes
There will be at most five competition CLASSES depending on how many solvers are entered in each of them:
 FD search: solvers in this class must follow the search strategy defined in the problem. They will be disqualified if there is evidence that they do not follow the search strategy.
 Free search: solvers in this class are free to ignore the search strategy. All FD search solvers (and local search solver running on a single thread) will be automatically entered in this class too.
 Parallel search: solvers in this class are free to use multiple threads or cores to solve the problem. All entries in the free search class (and the local search class) will be automatically entered in this class too, but they will be run in a single threaded mode.
 Open class: This class allows the usage of portfolio solvers. Solvers in this class are free to use multiple threads or cores to solve the problem. All entries in the parallel search class will be automatically entered in this class too.
 Local search: This class is specific for the local search solvers. Solvers in this class are free to use multiple threads or cores to solve the problem.
Docker Images
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.
 FD:
minizinc i outputmode dzn outputobjective <model.dzn> [data.dzn]
 FREE:
minizinc i outputmode dzn outputobjective f <model.dzn> [data.dzn]
 PAR:
minizinc i outputmode dzn outputobjective 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:

One or more of:
a
(output all solutions/intermediate solutions), ori
(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 theFREE
class are free to always ignore the search strategy, however they must still accept thef
flag. 
p <n>
(use the specified numbern
of threads and/or cores).
Entries competing in thePAR
andOPEN
classes must accept thep
flag.
MiniZinc solvers must support the following options
(by placing them in the solver configuration stdFlags
or in extraFlags
for longform options):
outputmode dzn
Output solutions (assignments to variables annotated withoutput
) in DZN format. This option must be supported by the solver.outputobjective
Output the objective value as_objective
for optimisation problems. This option must be supported by the solver.f
(ignore given search strategy)
Entries competing in theFREE
class are free to always ignore the search strategy, however they must still accept thef
flag.p <n>
(use the specified numbern
of threads and/or cores).
Entries competing in thePAR
andOPEN
classes must accept thep
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 Requirements
Output from FlatZinc solver entries must conform to the FlatZinc 2.7.3 specification.
MiniZinc solver entries must correctly implement the outputmode dzn
and outputobjective
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.
Execution Environment
During the MiniZinc Challenge 2023 all instances of Docker images will run on a compute server with the following specification:
 Image Operating System: Ubuntu 20.04 LTS (focal)
 Processor(s): Intel Xeon® Platinum 8260
 Configuration for FD, FREE: 1 core, 16 GiB memory
 Configuration for PAR, OPEN: 4 cores, 32 GiB memory
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).
Benchmark Problem Specification
Solver entries will be run with models that are compatible with
MiniZinc 2.7.3.
These models will adhere to the following restrictions:

Models may only use following types of variables:
 integer (e.g.
var 1..10: x
),
optional integer (e.g.var opt 1..10: x
),
integer set (e.g.var set of 1..10: x
)  boolean (e.g.
var bool: x
),
optional boolean (e.g.var opt bool: x
)  enumerated type (e.g.
var MY_ENUM: x
),
optional enumerated type (e.g.var opt MY_ENUM: x
),
set of enumerated type (e.g.var set of MY_ENUM: x
)
(including use of enum constructors in enum type definitions)  arrays of the above types of variables
In particular, float variables are not permitted.
 integer (e.g.

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.

Search annotations will be restricted to bool_search, int_search, set_search and seq_search.
For bool_search and int_search, only the following parameters (where applicable) will be used: variable choice:
 input_order
 first_fail (variable with smallest domain size)
 anti_first_fail (variable with largest domain size)
 smallest (variable with smallest minimal value)
 largest (variable with largest maximum value)
 value choice: [examples for domain {1,3,4,18}]
 indomain_min (x <= 1; x > 1)
 indomain_max (x >= 18; x < 18)
 indomain_median (x = 3 ; x != 3)
 indomain_split (x <= (1+18)/2 ; x > (1+18)/2)
 indomain_reverse_split (x > (1+18)/2 ; x <= (1+18)/2)
 search style
 complete
For set_search, only the following parameters will be used:
 variable choice:
 input_order
 value choice:
 indomain_min
 indomain_max
 search style
 complete
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 valueobjective = 2
eventually on backtracking to the choicex = 1
, then settingx >= 2
in most FD solvers will have domains forx :: 2..5
andobjective :: 8..10
and this timeobjective
will be selected as the next variable to label. A full specification of the available choices is given in the FlatZinc 2.7.3 specification.  variable choice:

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 righthand 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
outputmode dzn
andoutputobjective
when running the instance, then passing the result to a value propagation solver with the original instance.
Benchmark Selection
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:
 propagation speed
 search speed
 global constraints
 satisfaction
 optimization
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 timeframe. 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.3 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.
Submissions
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
The challenge will require solvers to process 100 MiniZinc instances with a runtime limit of 20
minutes (process time) per instances.
NOTE that the MiniZinc to FlatZinc time will be included in this time.
Assessment
Each solver s is run on problem p and the following information is collected.
 timeUsed(p,s)  the wall clock time used by the solver, or timeLimit(p) if it was still running at the timeLimit (quantized to seconds by rounding towards zero).
 solved(p,s)  true if a correct solution is returned, or correct unsatisfiability is detected
 quality(p,s)  the objective value of the best solution found by the solver (that is the last solution fully output before the time limit) assuming maximization
 optimal(p,s)  whether the objective value is proved optimal by the solver.
 timeSol(p,s,i)  the wall clock time used by the solver for finding the ith solution on the problem
 qualitySol(p,s,i)  the objective value of the ith solution found by the solver on the problem
There three different scoring procedure: complete, incomplete, and area. For prizes, the complete solver ranking is used.
Complete Scoring Procedure
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.
 If s gives a better answer than s' it scores 1 point.
 If s and s' gives indistinguishable answers then scoring is based on execution time comparison (see below).
 If s gives a worse answer than s' it scores 0 points.
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).
 Satisfaction Problem
A solver s answer is better than solver s' answer on satisfaction problem p iff solved(p,s) && not solved(p,s')
 Optimization Problem
A solver s is better than solver s' on optimization problem p iff solved(p,s) && not solved(p,s'), or
 optimal(p,s) && not optimal(p,s'), or
 quality(p,s) > quality(p,s'), or
Incomplete Scoring Procedure
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.
 Satisfaction Problem
A solver s answer is better than solver s' answer on satisfaction problem p iff solved(p,s) && not solved(p,s')
 Optimization Problem
A solver s is better than solver s' on optimization problem p iff solved(p,s) && not solved(p,s'), or
 quality(p,s) > quality(p,s'), or
Area Scoring Procedure
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.
 Satisfaction and Unsatisfiable Problems
f(p,s) = timeUsed(p,s)  Satisfiable Minimization Problems
f(p,s) = 0.25 * timeSol(p,s,1) + 0.5 * sum(i in 1..n)(qualitySol(p,s,i1) * (timeSol(p,s,i)  timeSol(p,s,i1)) ) / (UB  LB + 1) + 0.25 * timeUsed(p,s)
where UB = max(s in Solvers)(qualitySol(p,s,1)) and LB = min(s in Solvers)(quality(p,s).
CLASSES
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.
Prizes
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.
Restrictions
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.