Results for the 2024 MiniZinc Challenge have now been announced!

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 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:

  1. Which competition CLASS(ES) the entry will compete in (see below for details).

  2. 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.

  3. Whether the entry may be used by 3rd parties (entities that are not the submitters nor the MiniZinc Challenge organisers) for research purposes.

  4. 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 --output-mode dzn --output-objective <model.dzn> [data.dzn]
  • FREE: minizinc -i --output-mode dzn --output-objective -f <model.dzn> [data.dzn]
  • PAR: 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:

  • One or more of:

    • -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).
    Entries competing in the 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 solutions (assignments to variables annotated with output) in DZN format. This option must be supported by the solver.
  • --output-objective
    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 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).
    Entries competing in the 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 Requirements

Output from FlatZinc solver entries must conform to the FlatZinc 2.7.3 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.

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:

  1. 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.

  2. 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]);

  3. 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.

  4. 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 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.3 specification.

  5. 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.

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 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.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 run-time 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 i-th solution on the problem
  • qualitySol(p,s,i) - the objective value of the i-th 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,i-1) * (timeSol(p,s,i) - timeSol(p,s,i-1)) ) / (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.