this repo has no description
dekker.one
1.. _ch-solvers:
2
3Solving Technologies and Solver Backends
4========================================
5
6The ``minizinc`` tool can use various solver backends for a given model.
7Some solvers are separate executables that are called by ``minizinc``;
8other solvers are part of the ``minizinc`` binary (either hard-coded or loaded as a dynamic library or "plugin").
9In the former case, a temporary FlatZinc file is created and passed to the solver binary;
10in the latter one, the flattened model is passed to the backend directly in memory.
11Some solvers are part of the binary MiniZinc distribution, others have to be installed separately.
12You can find instructions for installing these solvers from source code and integrating into the ``minizinc`` tool
13in :ref:`ch-installation_detailed`.
14This chapter summarises usage options available for various target solvers.
15
16The help text of ``minizinc`` shows a list of configured solver backends and their tags. You can see solver-specific command-line options by running
17
18.. code-block:: bash
19
20 $ minizinc --help <solver-id or tag>
21
22Constraint Programming Solvers
23------------------------------
24
25Constraint Programming is the 'native' paradigm of MiniZinc. Below we discuss most common CP solvers.
26For their performance, consult MiniZinc Challenges (https://www.minizinc.org/challenge.html).
27
28Gecode
29~~~~~~
30
31Gecode is an open-source constraint programming system (see https://www.gecode.org).
32It supports many of MiniZinc's global constraints natively, and has support for integer, set and float variables.
33
34Gecode supports a number of constraints and search annotations that are not part of the MiniZinc standard library.
35You can get access to these by adding :mzn:`include "gecode.mzn";` to your model. The additional declarations are documented in :numref:`ch-lib-gecode`.
36
37
38Chuffed
39~~~~~~~
40
41Chuffed is a constraint solver based on *lazy clause generation* (see https://github.com/chuffed/chuffed).
42This type of solver adapts techniques from SAT solving, such as conflict clause learning,
43watched literal propagation and activity-based search heuristics, and can often be much faster than traditional CP solvers.
44
45In order to take full advantage of Chuffed's performance,
46it is often useful to add a search annotation to the model (see :ref:`sec-search`),
47but allow Chuffed to switch between this defined search and its activity-based search.
48In order to enable this behaviour, use the ``-f`` (free search) command line option or
49select *Free search* in the solver configuration pane of the MiniZinc IDE.
50
51Chuffed supports a number of additional search annotations that are not part of the MiniZinc standard library.
52The additional declarations are documented in :numref:`ch-lib-chuffed`.
53
54OR-Tools
55~~~~~~~~
56
57OR-Tools is a powerful open-source CP/SAT/LP solver (see https://developers.google.com/optimization/).
58It supports many of MiniZinc's global constraints natively. It often performs better multi-threaded (option ``-p``)
59so it can employ various solving technologies. A search annotation (see :ref:`sec-search`) can be useful,
60however allowing OR-Tools to mix the prescribed strategy with its own (option ``-f``) usually is best,
61analogously to Chuffed.
62
63
64Mixed-Integer Programming Solvers
65---------------------------------
66
67MiniZinc has built-in support for Mixed Integer Programing solvers.
68If you have any MIP solver installed (and MiniZinc was compiled with its support),
69you can run a model using MIP like this on the command line:
70
71.. code-block:: bash
72
73 minizinc --solver mip -v -s -a model.mzn data.dzn
74
75Of course, you can also select a particular solver, e.g. Gurobi (in case it is available):
76
77.. code-block:: bash
78
79 minizinc --solver gurobi -v -s -a model.mzn data.dzn
80
81MIP-Aware Modeling (But Mostly Useful for All Backends)
82~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
83
84Avoid mixing positive and negative coefficients in the objective. Use 'complementing' variables to revert sense.
85
86Avoid nested expressions which are hard to linearize (decompose for MIP). For example, instead of
87
88.. code-block:: minizinc
89
90 constraint forall(s in TASKS)(exists([whentask[s]=0] ++
91 [whentask[s]>= start[s]+(t*numslots) /\ whentask[s]<=stop[s]+(t*numslots) | t in 0..nummachines-1]));
92
93prefer the tight domain constraint
94
95.. code-block:: minizinc
96
97 constraint forall(s in TASKS)(whentask[s] in
98 {0} union array_union([ start[s]+(t*numslots) .. stop[s]+(t*numslots) | t in 0..nummachines-1]));
99
100To avoid **numerical issues**, make variable domains as tight as possible (compiler can deduce bounds in certain cases but explicit bounding can be stronger).
101Try to keep magnitude difference in each constraint below 1e4.
102Especially for variables involved in logical constraints, if you cannot reduce the domains to be in +/-1e4,
103consider indicator constraints (available for some solvers, see below), or use the following trick:
104instead of saying :mzn:`b=1 -> x<=0` where x can become very big, use e.g. :mzn:`b=1 -> 0.001*x<=0.0`.
105Especially for integer variables, the domain size of 1e4 should be an upper bound if possible -- what is the value of integrality otherwise?
106Avoid large coefficients too, as well as large values in the objective function.
107See more on tolerances in the Solver Options section.
108
109Example 1: *basic big-M constraint vs implication*. Instead of :mzn:`<expr> <= 1000000*y` given :mzn:`var 0..1: y`
110and where you use the 'big-M' value of 1000000 because you don't know a good upper bound on :mzn:`<expr>`, prefer :mzn:`y=0 -> <expr> <= 0`
111so that MiniZinc computes a possibly tighter bound, and consider the above trick: :mzn:`y=0 -> 0.0001*<expr> <= 0.0` to reduce magnitudes.
112
113Example 2: *cost-based choice*. Assume you want the model to make a certain decision, e.g., constructing a road, but then its cost should be minimal among some others, otherwise not considered. This can be modeled as follows:
114
115.. code-block:: minizinc
116
117 var 0..1: c; %% Whether we construct the road
118 var int: cost_road = 286*c + 1000000*(1-c);
119 var int: cost_final = min( [ cost_road, cost1, cost2 ] );
120
121Note the big coefficient in the definition of :mzn:`cost_road`. It can lead to numerical issues and a wrong answer: when the solver's integrality tolerance is 1e-6, it can assume :mzn:`c=0.999999` as equivalent to :mzn:`c=1` leading to :mzn:`cost_road=287` after rounding.
122
123A better solution, given reasonable bounds on :mzn:`cost1` and :mzn:`cost2`, is to replace the definition as follows:
124
125.. code-block:: minizinc
126
127 int: cost_others_ub = 1+2*ub_array( [cost1, cost2] ); %% Multiply by 2 for a stronger LP relaxation
128 var int: cost_road = 286*c + cost_others_ub*(1-c);
129
130
131Useful Flattening Parameters
132~~~~~~~~~~~~~~~~~~~~~~~~~~~~
133
134The following parameters can be given on the command line or modified in ``share/minizinc/linear/options.mzn``:
135
136::
137
138 -D nSECcuts=0/1/2 %% Subtour Elimination Constraints, see below
139 -D fMIPdomains=true/false %% The unified domains feature, see below
140 -D float_EPS=1e-6 %% Epsilon for floats' strict comparison,
141 %% used e.g. for the following cases:
142 %% x!=y, x<y, b -> x<y, b <-> x<=y
143 -DfIndConstr=true -DfMIPdomains=false %% Use solver's indicator constraints, see below
144 -DMinMaxGeneral=true %% Send min/max constraints to the solver (Gurobi only)
145 -DQuadrFloat=false -DQuadrInt=false %% Not forward float/integer multiplications for MIQCP backends, see below
146 -DCumulative=false %% Not forward cumulative with fixed durations/resources (SCIP only)
147 --no-half-reifications %% Turn off halfreification (full reification was until v2.2.3)
148
149Some Solver Options and Changed Default Values
150~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
151
152The following command-line options affect the backend or invoke extra functionality. Note that some of them have default values which may be different from the backend's ones.
153For example, tolerances have been tightened to enable more precise solving with integer variables and objective. This slightly deteriorates performance on average, so when your model has moderate constant and bound magnitudes, you may want to pass negative values to use solver's defaults.
154
155::
156
157 -h <solver-tag> full description of the backend options
158 --relGap <n> relative gap |primal-dual|/<solver-dep> to stop. Default 1e-8, set <0 to use backend's default
159 --feasTol <n> primal feasibility tolerance (Gurobi). Default 1e-8
160 --intTol <n> integrality tolerance for a variable. Default 1e-8
161 --solver-time-limit-feas <n>, --solver-tlf <n>
162 stop after <n> milliseconds after the first feasible solution (some backends)
163 --writeModel <file>
164 write model to <file> (.lp, .mps, .sav, ...). All solvers support the MPS format
165 which is industry standard. Most support the LP format. Some solvers have own formats,
166 for example, the CIP format of SCIP ("constraint integer programming").
167 --readParam <file>
168 read backend-specific parameters from file (some backends)
169 --writeParam <file>
170 write backend-specific parameters to file (some backends)
171 --readConcurrentParam <file>
172 each of these commands specifies a parameter file of one concurrent solve (Gurobi only)
173 --keep-paths this standard flattening option annotates every item in FlatZinc by its "flattening history".
174 For MIP solvers, it additionally assigns each constraint's name as the first 255 symbols of that.
175 --cbcArgs '-guess -cuts off -preprocess off -passc 1'
176 parameters for the COIN-OR CBC backend
177
178All MIP solvers directly support multi-threading (option ``-p``). For COIN-BC to use it, it needs to be
179configured with ``--enable-cbc-parallel``.
180
181Subtour Elimination Constraints
182~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
183
184Optionally use the SEC cuts for the circuit global constraint.
185Currently only Gurobi, IBM ILOG CPLEX, and COIN-OR CBC (trunk as of Nov 2019).
186If compiling from source, this needs boost and cmake flag ``-DCOMPILE_BOOST_MINCUT=ON``
187(or ``#define`` it in ``lib/algorithms/min_cut.cpp``).
188Compile your model with the flag ``-DnSECcuts=<n>`` with the following possible ``<n>``:
1890,1: use MTZ formulation; 1,2: pass on circuit constraints
190to the SEC cut generator, so 1 would use both.
191
192Unified Domains (MIPdomains)
193~~~~~~~~~~~~~~~~~~~~~~~~~~~~
194
195The 'MIPdomains' feature of the Flattener aims at reducing the number of binary flags
196encoding linearized domain constraints, see the paper
197*Belov, Stuckey, Tack, Wallace. Improved Linearization of Constraint Programming Models. CP 2016.*
198
199By default it is on.
200To turn it off which might be good for some models, add option ``-D fMIPdomains=false`` during flattening.
201Some parameters of the unification are available, run with ``--help``.
202
203Indicator Constraints
204~~~~~~~~~~~~~~~~~~~~~
205
206Some solvers (IBM ILOG CPLEX, Gurobi, SCIP) have indicator constrains with greater numerical stability than big-M decomposition.
207Moreover, they can be applied to decompose logical constraints on *unbounded variables*. However, for reified comparisons with
208reasonable big-M bounds they perform worse because solvers don't include them in the LP relaxation.
209Add command-line parameters ``-D fIndConstr=true -D fMIPdomains=false`` when flattening
210to use them.
211
212Quadratic Constraints and Objectives (MIQCP)
213~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
214
215Gurobi 9.0 and SCIP support MIQCP (invoking non-convex global optimizer because MiniZinc translates multiplication to
216equality with an intermediate variable: whenever the model uses an expression x*y it is converted to z with z==x*y which is non-convex).
217While this is mostly advantageous for integer multiplication (which is linearly decomposed for other solvers), for float variables
218this is the only way to go. To switch off forwarding float/integer multiplications to the backend, run compiler with either or both of
219``-DQuadrFloat=false -DQuadrInt=false``.
220
221Pools of User Cuts and Lazy Constraints
222~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
223Some constraints in the model can be declared as user and/or lazy cuts and they will be added to the corresponding pools
224for the solvers supporting them. For that, apply annotations :mzn:`::MIP_cut` and/or :mzn:`::MIP_lazy` after a constraint.
225For Gurobi and IBM ILOG CPLEX, see ``share/minizinc/linear/options.mzn`` for their exact meaning.
226
227Warm Starts
228~~~~~~~~~~~
229
230For general information of warm start annotations, see :ref:`sec_warm_starts`.
231Warm starts are currently implemented for Gurobi, IBM ILOG CPLEX, XPRESS, and COIN-OR CBC.
232
233.. _ch-solvers-nonlinear:
234
235Non-Linear Solvers via NL File Format
236-------------------------------------
237
238MiniZinc has experimental support for non-linear solvers that conform to the AMPL NL standard. There are a number of open-source solvers, such as Ipopt, Bonmin and Couenne, that can be interfaced to MiniZinc in this way.
239
240You can download binaries of these solvers from AMPL (https://ampl.com/products/solvers/open-source/). In order to use them with MiniZinc, you need to create a solver configuration file. Future version of MiniZinc will make this easier, but for now you can follow these steps:
241
2421. Download the solver binary. For this example, we assume you chose the Couenne solver, which supports non-linear, non-convex, mixed discrete and continuous problems.
2432. Create a solver configuration file called ``couenne.msc`` in the ``share/minizinc/solvers`` directory of your MiniZinc installation, with the following contents:
244
245 .. code-block:: json
246
247 {
248 "id" : "org.coin-or.couenne",
249 "name" : "Couenne",
250 "executable" : "/Users/tack/Downloads/couenne-osx/couenne",
251 "version": "0.5.6",
252 "supportsFzn":false,
253 "supportsNL":true
254 }
255
256 You can adapt the ``version`` field if you downloaded a different version (it's only used for displaying).
257
2583. Run ``minizinc --solvers``. The Couenne solver should appear in the list of solvers now.
2594. Run ``minizinc --solver couenne model.mzn`` on some MiniZinc model, or use Couenne from the MiniZinc IDE.
260
261The AMPL NL support is currently experimental, and your MiniZinc model is translated to NL without regard
262for the capabilities of the target solver. For example, Ipopt only supports continuous variables, so translating
263a model with integer variables will result in a solver-level error message. There is currently no support for
264translating Boolean variables and constraints into 0/1 integer variables (as required by e.g. Couenne).
265You can experiment with the standard linearisation library, using the ``-Glinear [-DQuadrFloat=true -DQuadrInt=true]``
266flag. However, this will either
267linearise all integer constraints, even the ones that solvers like Couenne may support natively, or use non-convex
268representation. We will ship dedicated solver libraries for some NL solvers with future versions of MiniZinc.
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285