3.1. The MiniZinc Command Line Tool¶
The core of the MiniZinc constraint modelling system is the minizinc tool. You can use it directly from the command line, through the MiniZinc IDE, or through a programmatic interface (API). This chapter summarises the options accepted by the tool, and explains how it interacts with target solvers.
3.1.1. Basic Usage¶
The minizinc tool performs three basic functions: it compiles a MiniZinc model (plus instance data), it runs an external solver, and it translates solver output into the form specified in the model. Most users would use all three functions at the same time. For example, let us assume that we want to solve the following simple problem, given as two files (model.mzn and data.dzn):
int: n;
array[1..n] of var 1..2*n: x;
include "alldifferent.mzn";
constraint alldifferent(x);
solve maximize sum(x);
output ["The resulting values are \(x).\n"];
n = 5;
To run the model file model.mzn with data file data.dzn using the Gecode solver, you can use the following command line:
$ minizinc --solver Gecode model.mzn data.dzn
This would result in the output
The resulting values are [10, 9, 8, 7, 6].
----------
==========
However, each of the three functions can also be accessed individually. For example, to compile the same model and data, use the -c option:
$ minizinc -c --solver Gecode model.mzn data.dzn
This will result in two new files, model.fzn and model.ozn, being output in the same directory as model.mzn. You could then run a target solver directly on the model.fzn file, or use minizinc:
$ minizinc --solver Gecode model.fzn
You will see that the solver produces output in a standardised form, but not the output prescribed by the output item in the model:
x = array1d(1..5 ,[10, 9, 8, 7, 6]);
----------
==========
The translation from this output to the form specified in the model is encoded in the model.ozn file. You can use minizinc to execute the .ozn file. In this mode, it reads a stream of solutions from standard input, so we need to pipe the solver output into minizinc:
$ minizinc --solver Gecode model.fzn | minizinc --ozn-file model.ozn
These are the most basic command line options that you need in order to compile and run models and translate their output. The next section lists all available command line options in detail. Section 4.3.5 explains how new solvers can be added to the system.
3.1.2. Adding Solvers¶
Solvers that support MiniZinc typically consist of two parts: a solver executable, which can be run on the FlatZinc output of the MiniZinc compiler, and a solver library, which consists of a set of MiniZinc files that define the constraints that the solver supports natively. This section deals with making existing solvers available to the MiniZinc tool chain. For information on how to add FlatZinc support to a solver, refer to Section 4.3.
3.1.2.1. Configuration files¶
In order for MiniZinc to be able to find both the solver library and the executable, the solver needs to be described in a solver configuration file (see Section 4.3.5 for details). If the solver you want to install comes with a configuration file (which has the file extension .msc for MiniZinc Solver Configuration), it has to be in one of the following locations:
- In the minizinc/solvers/ directory of the MiniZinc installation. If you install MiniZinc from the binary distribution, this directory can be found at /usr/share/minizinc/solvers on Linux systems, inside the MiniZincIDE application on macOS system, and in the Program Files\\MiniZinc IDE (bundled) folder on Windows.
- In the directory $HOME/.minizinc/solvers on Linux and macOS systems, and the Application Data directory on Windows systems.
- In any directory listed on the MZN_SOLVER_PATH environment variable (directories are separated by : on Linux and macOS, and by ; on Windows systems).
- In any directory listed in the mzn_solver_path option of the global or user-specific configuration file (see Section 3.1.4)
- Alternatively, you can use the MiniZinc IDE to create solver configuration files, see Section 3.2.5.2 for details.
After adding a solver, it will be listed in the output of the minizinc --solvers command.
3.1.2.2. Configuration for MIP solvers¶
Some solvers require additional configuration flags before they can be used. For example, the binary bundle of MiniZinc comes with interfaces to the CPLEX and Gurobi Mixed Integer Programming solvers. However, due to licensing restrictions, the solvers themselves are not part of the bundled release. Depending on where CPLEX or Gurobi is installed on your system, MiniZinc may be able to find the solvers automatically, or it may require an additional option to point it to the shared library.
In case the libraries cannot be found automatically, you can use one of the following:
- CPLEX: Specify the location of the shared library using the --cplex-dll command line option. On Windows, the library is called cplexXXXX.dll and typically found in same directory as the cplex executable. On Linux it is libcplexXXX.so, and on macOS libcplexXXXX.jnilib, where XXX and XXXX stand for the version number.
- Gurobi: The command line option for Gurobi is --gurobi-dll. On Windows, the library is called gurobiXX.dll (in the same directory as the gurobi executable), and on Linux and macOS is it libgurobiXX.so (in the lib directory of your Gurobi installation).
- You can define these paths as defaults in your user configuration file, see Section 3.1.4.
3.1.3. Options¶
You can get a list of all the options supported by the minizinc tool using the --help flag.
3.1.3.1. General options¶
These options control the general behaviour of the minizinc tool.
-
--help
,
-h
¶
Print a help message.
-
--version
¶
Print version information.
-
--solvers
¶
Print list of available solvers.
-
--solver
<id>
,
--solver
<solver configuration file>.msc
¶ Select solver to use. The first form of the command selects one of the solvers known to MiniZinc (that appear in the list of the --solvers command). You can select a solver by name, id, or tag, and add a specific version. For example, to select a mixed-integer programming solver, identified by the mip tag, you can use --solver mip. To select a specific version of Gurobi (in case you have two versions installed), use --solver Gurobi@7.5.2. Instead of the name you can also use the solver’s identifier, e.g. --solver org.gecode.gecode.
The second form of the command selects the solver from the given configuration file (see Section 4.3.5).
-
--help
<id>
¶ Print help for a particular solver. The scheme for selecting a solver is the same as for the --solver option.
-
-v
,
-l
,
--verbose
¶
Print progress/log statements (for both compilation and solver). Note that some solvers may log to stdout.
-
--verbose-compilation
¶
Print progress/log statements for compilation only.
-
-s
,
--statistics
¶
Print statistics (for both compilation and solving).
-
--compiler-statistics
¶
Print statistics for compilation.
-
-c
,
--compile
¶
Compile only (do not run solver).
-
--config-dirs
¶
Output configuration directories.
-
--solvers-json
¶
Print configurations of available solvers as a JSON array.
-
--param-file
<file>
¶ Read command line options from the given JSON file. See Section 3.1.5.
3.1.3.2. Solving options¶
Each solver may support specific command line options for controlling its behaviour. These can be queried using the --help
-
-a
,
--all-solutions
¶
Report all solutions in the case of satisfaction problems, or print intermediate solutions of increasing quality in the case of optimisation problems.
-
-n
<i>
,
--num-solutions
<i>
¶ Stop after reporting i solutions (only used with satisfaction problems).
-
-i
,
--intermediate
¶
Turns on printing of intermediate solutions for optimisation problems. Has no effect for satisfaction problems.
-
-n-i
,
--no-intermediate
¶
Turns off printing of intermediate solutions for optimisation problems. Has no effect for satisfaction problems.
-
--all-satisfaction
¶
Turns on printing of all solutions for satisfaction problems. Has no effect for optimisation problems.
-
--disable-all-satisfaction
¶
Turns off printing of all solutions for satisfaction problems. Has no effect for optimisation problems.
-
-f
,
--free-search
¶
Instructs the solver to conduct a “free search”, i.e., ignore any search annotations. The solver is not required to ignore the annotations, but it is allowed to do so.
-
--solver-statistics
¶
Print statistics during and/or after the search for solutions.
-
--verbose-solving
¶
Print log messages (verbose solving) to the standard error stream.
-
-p
<i>
,
--parallel
<i>
¶ Run with i parallel threads (for multi-threaded solvers).
-
-r
<i>
,
--random-seed
<i>
¶ Use i as the random seed (for any random number generators the solver may be using).
3.1.3.3. Flattener input options¶
These options control aspects of the MiniZinc compiler.
-
--ignore-stdlib
¶
Ignore the standard libraries stdlib.mzn and builtins.mzn
-
--instance-check-only
¶
Check the model instance (including data) for errors, but do not convert to FlatZinc.
-
-e
,
--model-check-only
¶
Check the model (without requiring data) for errors, but do not convert to FlatZinc.
-
--model-interface-only
¶
Only extract parameters and output variables.
-
--model-types-only
¶
Only output variable (enum) type information.
-
--no-optimize
¶
Do not optimize the FlatZinc
-
-m
<file>
,
--model
<file>
¶ File named <file> contains the model.
-
-d
<file>
,
--data
<file>
¶ File named <file> contains data used by the model.
-
-D
<data>
,
--cmdline-data
<data>
¶ Include the given data assignment in the model.
-
--stdlib-dir
<dir>
¶ Path to MiniZinc standard library directory
-
-G
--globals-dir --mzn-globals-dir <dir>
¶ Search for included globals in <stdlib>/<dir>.
-
-
--input-from-stdin
¶ Read problem from standard input
-
-I
--search-dir
¶ Additionally search for included files in <dir>.
-
-D
"fMIPdomains=false"
¶ No domain unification for MIP
-
--MIPDMaxIntvEE
<n>
¶ Max integer domain subinterval length to enforce equality encoding, default 0
-
--MIPDMaxDensEE
<n>
¶ Max domain cardinality to N subintervals ratio to enforce equality encoding, default 0, either condition triggers
-
--only-range-domains
¶
When no MIPdomains: all domains contiguous, holes replaced by inequalities
-
--allow-multiple-assignments
¶
Allow multiple assignments to the same variable (e.g. in dzn)
-
--compile-solution-checker
<file>.mzc.mzn
¶ Compile solution checker model.
Flattener two-pass options¶
Two-pass compilation means that the MiniZinc compiler will first compile the model in order to collect some global information about it, which it can then use in a second pass to improve the resulting FlatZinc. For some combinations of model and target solver, this can lead to substantial improvements in solving time. However, the additional time spent on the first compilation pass does not always pay off.
-
--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)
-
-O<n>
¶
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
Flattener output options¶
These options control how the MiniZinc compiler produces the resulting FlatZinc output. If you run the solver directly through the minizinc command or the MiniZinc IDE, you do not need to use any of these options.
-
--no-output-ozn
,
-O-
¶
Do not output ozn file
-
--output-base
<name>
¶ Base name for output files
-
--fzn
<file>
,
--output-fzn-to-file
<file>
¶ Filename for generated FlatZinc output
-
-O
,
--ozn
,
--output-ozn-to-file
<file>
¶ Filename for model output specification (-O- for none)
-
--keep-paths
¶
Don’t remove path annotations from FlatZinc
-
--output-paths
¶
Output a symbol table (.paths file)
-
--output-paths-to-file
<file>
¶ Output a symbol table (.paths file) to <file>
-
--output-to-stdout
,
--output-fzn-to-stdout
¶
Print generated FlatZinc to standard output
-
--output-ozn-to-stdout
¶
Print model output specification to standard output
-
--output-paths-to-stdout
¶
Output symbol table to standard output
-
--output-mode
<item|dzn|json>
¶ Create output according to output item (default), or output compatible with dzn or json format
-
--output-objective
¶
Print value of objective function in dzn or json output
-
-Werror
¶
Turn warnings into errors
3.1.3.4. Solution output options¶
These options control how solutions are output. Some of these options only apply if minizinc is used to translate a stream of solutions coming from a solver into readable output (using a .ozn file generated by the compiler).
-
--ozn-file
<file>
¶ Read output specification from ozn file.
-
-o
<file>
,
--output-to-file
<file>
¶ Filename for generated output.
-
-i
<n>
,
--ignore-lines
<n>
,
--ignore-leading-lines
<n>
¶ Ignore the first <n> lines in the FlatZinc solution stream.
-
--soln-sep
<s>
,
--soln-separator
<s>
,
--solution-separator
<s>
¶ Specify the string printed after each solution (as a separate line). The default is to use the same as FlatZinc, “———-“.
-
--soln-comma
<s>
,
--solution-comma
<s>
¶ Specify the string used to separate solutions. The default is the empty string.
-
--unsat-msg
(--unsatisfiable-msg)
¶ Specify status message for unsatisfiable problems (default: "=====UNSATISFIABLE=====")
-
--unbounded-msg
¶
Specify status message for unbounded problems (default: "=====UNBOUNDED=====")
-
--unsatorunbnd-msg
¶
Specify status message for unsatisfiable or unbounded problems (default: "=====UNSATorUNBOUNDED=====")
-
--unknown-msg
¶
Specify status message if search finished before determining status (default: "=====UNKNOWN=====")
-
--error-msg
¶
Specify status message if search resulted in an error (default: "=====ERROR=====")
-
--search-complete-msg
<msg>
¶ Specify status message if when search exhausted the entire search space (default: "==========")
-
--non-unique
¶
Allow duplicate solutions.
-
-c
,
--canonicalize
¶
Canonicalize the output solution stream (i.e., buffer and sort).
-
--output-non-canonical
<file>
¶ Non-buffered solution output file in case of canonicalization.
-
--output-raw
<file>
¶ File to dump the solver’s raw output (not for hard-linked solvers)
-
--no-output-comments
¶
Do not print comments in the FlatZinc solution stream.
-
--output-time
¶
Print timing information in the FlatZinc solution stream.
-
--no-flush-output
¶
Don’t flush output stream after every line.
3.1.4. User Configuration Files¶
The minizinc tool reads a system-wide and a user-specific configuration file to determine default paths, solvers and solver options. The files are called Preferences.json, and you can find out the locations for your platform using the option --config-dirs:
$ minizinc --config-dirs
{
"globalConfigFile" : "/Applications/MiniZincIDE.app/Contents/Resources/share/minizinc/Preferences.json",
"userConfigFile" : "/Users/Joe/.minizinc/Preferences.json",
"userSolverConfigDir" : "/Users/Joe/.minizinc/solvers",
"mznStdlibDir" : "/Applications/MiniZincIDE.app/Contents/Resources/share/minizinc"
}
The configuration files are simple JSON files that can contain the following configuration options:
- mzn_solver_path (list of strings): Additional directories to scan for solver configuration files.
- mzn_lib_dir (string): Location of the MiniZinc standard library.
- tagDefaults (list of lists of strings): Each entry maps a tag to the default solver for that tag. For example, [["cp","org.chuffed.chuffed"],["mip","org.minizinc.gurobi"]] would declare that whenever a solver with tag "cp" is requested, Chuffed should be used, and for the "mip" tag, Gurobi is the default. The empty tag ("") can be used to define the system-wide default solver (i.e., the solver that is chosen when running minizinc without the --solver argument).
- solverDefaults (list of lists of strings): Each entry consists of a list of three strings: a solver identifier, a command line option, and a value for that command line option.For example, [["org.minizinc.gurobi","--gurobi-dll", "/Library/gurobi752/mac64/lib/libgurobi75.so"]] would specify the Gurobi shared library to use (on a macOS system with Gurobi 7.5.2). For command line options that don’t take a value, you have to specify an empty string, e.g. [["org.minizinc.gurobi","--uniform-search",""]].
Here is a sample configuration file:
{
"mzn_solver_path": ["/usr/share/choco"],
"tagDefaults": [["cp","org.choco-solver.choco"],["mip","org.minizinc.cplex"],["","org.gecode.gecode"]],
"solverDefaults": [["org.minizinc.cplex","--cplex-dll","/opt/CPLEX_Studio128/cplex/bin/x86-64_sles10_4.1/libcplex128.so"]]
}
Configuration values in the user-specific configuration file override the global values, except for solver default arguments, which are only overridden if the name of the option is the same, and otherwise get added to the command line.
Note: Due to current limitations in MiniZinc’s JSON parser, we use lists of strings rather than objects for the default mappings. This may change in a future release, but the current syntax will remain valid. The location of the global configuration is currently the share/minizinc directory of the MiniZinc installation. This may change in future versions to be more consistent with file system standards (e.g., to use /etc on Linux and /Library/Preferences on macOS).
3.1.5. Command-line Parameter Files¶
The minizinc tool is able to read command line options from one or more JSON files through use of the --param-file option. This option may be specified multiple times, and substitutes the options given in the JSON file in its place, meaning it can be combined with normal command-line options, as well as other --param-file configurations. MiniZinc also recognises the .mpc file extension for command line parameter files without requiring the --param-file option.
As most minizinc options which take a single value are given the final one they are assigned, later specifications of command-line parameter files will generally override options contained in previous ones, and later command-line options will override previous options.
The given file must be in JSON format and contain a root object whose keys and values correspond to command line options and their values respectively. For long-form options which start with two dashes, the leading dashes may be omitted from the JSON object key name. For short-form options which start with a single dash, the leading dash is required. Command line options which take multiple values through being specified multiple times can be represented using a JSON array. Options which take the JSON boolean value true are treated as flags without associated parameters (false omits the flag).
Consider the configuration file config.mpc:
{
"solver": "gecode",
"cmdline-data": ["x = 1", "y = 2", "z = 3"],
"-p": 2,
"output-paths": true
}
Running minizinc --verbose config.mpc -p 4 model.mzn (or minizinc --verbose --param-file config.mpc -p 4 model.mzn) is equivalent to running
$ minizinc --verbose \
--solver gecode \
--cmdline-data "x = 1" \
--cmdline-data "y = 2" \
--cmdline-data "z = 3" \
-p 2 \
--output-paths \
-p 4 \
model.mzn
Note that since -p 4 comes after -p 2, its value overrides the previous one and so -p 4 is used. However, the multiple --cmdline-data options do not override each other as --cmdline-data allows for specification of multiple strings of data.
Configuration files may also be used as a convenient way to specify instances.
For a configuration file instance.mpc
{
"model": "model.mzn",
"data": "data.dzn"
}
And another configuration file gecode.mpc
{
"solver": "gecode",
"intermediate-solutions": true
}
We can run the instance with minizinc gecode.mpc instance.mpc. Note that the files model.dzn and data.dzn will be resolved relative to the location of the configuration file which specified them.
In this way, multiple configuration files can be set up for different instances and solver configurations, then combined as required.