846.minizinc_s
Constraint Programming
The Minizinc authors include Guido Tack, Jip J. Dekker, Jason Nguyen, Gleb Belov, and Kevin Leo.
846.minizinc_s was submitted to the SPEC CPU v8 Benchmark Search Program by Guido Tack <guido [dot] tack[at]monash [dot] edu>.
MiniZinc is a free and open-source constraint modeling language. One can use MiniZinc to model constraint satisfaction and discrete optimization problems in a high-level, solver-independent way, taking advantage of a large library of pre-defined constraints. The model is then compiled into FlatZinc, a solver input language that is understood by a wide range of solvers. MiniZinc can be used to build intelligent decision support systems for operations engineering. In SPEC CPU, we use two different solvers for the backend, Gecode and Chuffed. At a high abstraction level, one can consider Gecode to be a heavyweight compiler and Chuffed to be a lightweight interpreter. They each have their strengths and weaknesses, based on the kinds of problems to be solved.
Gecode is an open source C++ toolkit for developing constraint-based systems and applications. Gecode provides a constraint solver with state-of-the-art performance while being modular and extensible, which can be used as a backend to the MiniZinc language by compiling the FlatZinc solver language and offers five different optimization levels for compilation. It supports many of MiniZinc's global constraints natively, and has support for integer, set, and float variables. Gecode provides excellent performance with respect to both runtime and memory usage; for many years it won gold medals in all categories at the MiniZinc Challenge.
Chuffed is a state of the art lazy clause solver designed from the ground up with lazy clause generation in mind. Lazy clause generation is a hybrid approach to constraint solving that combines features of finite domain propagation and Boolean satisfiability. The hybrid system combines some of the advantages of finite domain constraint programming (high level model and programmable search) with some of the advantages of SAT solvers (reduced search by nogood creation, and effective autonomous search using variable activities). Chuffed can be used as a backend to the MiniZinc constraint modeling language, to interpret the FlatZinc solver language. The overhead from lazy clause generation ranges from negligible to around 100%. The search time reduction, however, can reach orders of magnitude on appropriate problems. Thus lazy clause generation is an extremely important and useful technology.
The inputs for the benchmark are .mzn files, which are constraint modeling programs written in the MiniZinc language. For example, one of the test command lines consists of a tennis puzzle. The comment at the top of tennis_problem.mzn describes:
% % Tennis problem in MiniZinc. % % From Jean-Louis Laurière "Problem Solving and Artificial Intelligence", % page 422pp: % % Frank and George play tennis. % Frank beats George 6 game to 3 % In 4 games the server loses. % Who served the first game? %
The rest of the file consists of the constraint code, which models the rules of tennis and the constraints given in the problem statement.
Then on the command line, a solver is chosen to compile or interpret the FlatZinc output of the MiniZinc compiler. Some of the command lines use the Chuffed solver, and others use the Gecode solver with various optimization levels. Here is the --help output describing the compiler optimization levels for Gecode:
Flattener two-pass options:
--two-pass Flatten twice to make better flattening decisions for the target
--use-gecode Perform root-node-propagation with Gecode (adds --two-pass)
--shave Probe bounds of all variables at the root node (adds --use-gecode)
--sac Probe values of all variables at the root node (adds --use-gecode)
--pre-passes N Number of times to apply shave/sac pass (0 = fixed-point, 1 = default)
-g Debug mode: Forces -O0 and records all domain changes as constraints instead of applying them
-O*
Two-pass optimisation levels:
-O0: Disable optimize (--no-optimize) -O1: Single pass (default)
-O2: Same as: --two-pass -O3: Same as: --use-gecode
-O4: Same as: --shave -O5: Same as: --sac
The input problems come either from the MiniZinc Challenge repository, or from Hakan Kjellerstrand's MiniZinc repository. A savvy user can download more problems from those sites and craft their own MiniZinc command lines and exercise the Gecode or Chuffed solvers.
MiniZinc has documentation available online at minizinc.org/doc-latest/en. Additionally, a offline PDF tutorial is available here: minizinc-tute.pdf.
Each command line is solving one problem, and the output consists of the answer to that problem. The answer is in a text file, which also contains the final values of other constraint variables important to the solution. For the example above, the output of tennis_problem.mzn is found in tennis_problem.mzn_2.out:
{
"fs" : [0, 1, 0, 1, 0, 1, 0, 1, 0],
"gs" : [1, 0, 1, 0, 1, 0, 1, 0, 1],
"fw" : [1, 0, 1, 1, 1, 1, 0, 1, 0],
"gw" : [0, 1, 0, 0, 0, 0, 1, 0, 1]
}
----------
The output consists of the rows which indicate when Frank served (fs), when George served (gs), when Frank won (fw) and when George won (gw), over the nine games that were played. The printout indicates that George served the first game. The benchmark run output should match exactly to the expected outputs, hence there is no tolerance allowed.
One command line option to help validate is --statistics. Adding this provides some more output regarding the size of the input problem and the constraint statistics after it is solved. These statistics should also match between systems. Here is the same example with statistics shown:
$ ./Minizinc --stdlib-dir share/minizinc -r 214365 --output-mode json --solver gecode_presolver tennis_problem.mzn --statistics
% Generated FlatZinc statistics:
%%%mzn-stat: paths=0
%%%mzn-stat: flatIntVars=54
%%%mzn-stat: flatIntConstraints=46
%%%mzn-stat: method="satisfy"
%%%mzn-stat-end
{
"fs" : [0, 1, 0, 1, 0, 1, 0, 1, 0],
"gs" : [1, 0, 1, 0, 1, 0, 1, 0, 1],
"fw" : [1, 0, 1, 1, 1, 1, 0, 1, 0],
"gw" : [0, 1, 0, 0, 0, 0, 1, 0, 1]
}
----------
%%%mzn-stat: variables=54
%%%mzn-stat: propagators=46
%%%mzn-stat: propagations=218
%%%mzn-stat: nodes=13
%%%mzn-stat: failures=3
%%%mzn-stat: restarts=0
%%%mzn-stat: peak_depth=9
%%%mzn-stat-end
%%%mzn-stat: nSolutions=1
%%%mzn-stat-end
C++, C, MiniZinc
The benchmark uses std::thread to solve problems in parallel using a work stealing scheme. The problems being solved are not conducive to parallelism beyond 4 threads, since after that point the extra threads are thrashing the scheduler and consuming system time while not completing useful work.
GNU/Linux systems implement C++ std::thread using POSIX Threads. Although some systems automatically include the needed support, this is not universal. Surprises have been seen when changing OS versions, or libraries, or compilers; or when FDO is added; or when combining C and C++ modules. Typically, it is safest to add -pthread to all compile and link lines for all SPEC CPU benchmarks that use std::thread. Please see the $SPEC/config directory for Example config files that demonstrate how to conveniently do so.
MiniZinc is a free and open-source constraint modeling language, consisting of:
A few source files are marked with the Bison exception: "As a special exception, you may create a larger work that contains part or all of the Bison parser skeleton and distribute that work under terms of your choice..." Such files are distributed under the same license as the other files in the same sub directory tree: Mozilla for src/mzn/ or MIT for src/gecode/.
spec_random_distributions.h is sampled from the LLVM project, which is distributed under the Apache License v2.0 with LLVM Exceptions.
The constraint problems models (benchmark inputs) are taken from two places:
Copyright © 2026 Standard Performance Evaluation Corporation (SPEC®)