this repo has no description
dekker.one
1Globalizer
2==========
3
4Globalizer [1]_ analyses a model and set of data to provide suggestions of
5global constraints that can replace or enhance a user's model.
6
7Basic Usage
8-----------
9
10To use Globalizer simply execute it on a model and set of data files:
11
12``minizinc --solver org.minizinc.globalizer model.mzn data-1.dzn data-2.dzn``
13
14Note: Globalizer may also be executed on a non-parameterised model with
15no data files.
16
17The following demonstrates the basic usage of Globalizer.
18Below, we see a simple model for the car sequencing problem [2]_, ``cars.mzn``.
19
20
21.. literalinclude:: examples/cars.mzn
22 :language: minizinc
23 :name: ex-glob-cars
24 :caption: Model for the car sequencing problem (:download:`cars.mzn <examples/cars.mzn>`).
25
26And here we have a data file ``cars_data.dzn``.
27
28.. literalinclude:: examples/cars_data.dzn
29 :language: minizinc
30 :name: ex-glob-cars-data
31 :caption: Data for the car sequencing problem (:download:`cars_data.dzn <examples/cars_data.dzn>`).
32
33Executing Globalizer on this model and data file we get the following output:
34
35.. code-block:: minizincdef
36
37 % minizinc --solver globalizer cars.mzn cars_data.dzn
38 cars.mzn|33|12|33|69 [ ] gcc(class,cars_in_class)
39 cars.mzn|33|35|33|68 [ ] count(class,c,cars_in_class[c])
40 cars.mzn|28|27|28|65;cars.mzn|29|9|30|32 [ ] sliding_sum(0,max_per_block[p],block_size[p],used[_, p])
41
42Each line of output is comprised of three elements.
43
44#. Expression locations (separated by semicolon ';') that the constraint might be able to replace.
45#. (Between square brackets '[' ']') the context under which the constraint might replace the expressions of 1.
46#. The replacement constraint.
47
48From the example above we see that a ``gcc`` constraint and a ``sliding_sum``
49constraint can replace some constraints in the model. Taking the ``sliding_sum``
50case, we see that it replaces the expression ``cars.mzn|28|27|28|65`` which
51corresponds to ``i in 1..(n_cars - (block_size[p] - 1))`` and ``cars.mzn|29|27|28|65``
52which corresponds to the ``<=`` expression including the ``sum``.
53The original constraint can be replaced with:
54
55.. code-block:: minizincdef
56
57 constraint forall (p in options) (
58 sliding_sum(0, max_per_block[p], block_size[p], used[..,p]));
59
60Caveats
61-------
62
63**MiniZinc syntax support.**
64Globalizer was implemented with support for a subset of an early version
65of the MiniZinc 2.0 language. As a result there are some limitations.
66First, Globalizer does not support ``set`` variables or ``enum`` types.
67The array slicing syntax supported in MiniZinc was not decided upon when
68Globalizer was implemented so it uses an incompatible syntax. Globalizer
69uses ``_`` instead of ``..``. This can be seen above in the translation
70of ``used[_,p]`` to ``used[..,p]``.
71
72
73**New constraint.**
74A special two argument version of the ``global_cardinality`` constraint
75called ``gcc`` has been added which is not in the standard library. It is
76defined as follows:
77
78.. code-block:: minizincdef
79
80 predicate gcc(array[int] of var int: x, array[int] of var int: counts) =
81 global_cardinality(x,
82 [ i | i in index_set(counts) ],
83 array1d(counts));
84
85Supported Constraints
86---------------------
87Globalizer currently supports detection of the following constraints:
88
89.. code-block:: minizincdef
90
91 alldifferent alldifferent_except_0 all_equal_int
92 bin_packing bin_packing_capa bin_packing_load
93 binaries_represent_int binaries_represent_int_3A binaries_represent_int_3B
94 binaries_represent_int_3C channel channelACB
95 count_geq cumulative_assert decreasing
96 gcc global_cardinality inverse
97 lex_lesseq_int_checking lex2_checking maximum_int_checking
98 minimum_int_checking member nvalue
99 strict_lex2_checking subcircuit_checking true
100 atleast atmost bin_packing_load_ub
101 circuit_checking count diffn
102 distribute element increasing
103 lex_less_int_checking sliding_sum sort_checking
104 unary value_precede_checking
105
106
107Using Globalizer in the MiniZinc IDE
108------------------------------------
109
110To use the Globalizer in the MiniZinc IDE, open a model, and several
111data files.
112Select ``Globalizer`` from the solver configuration dropdown menu.
113Click the solve button (play symbol).
114If you did not select any data file, a dialog should pop up that allows
115you to select data files.
116To select multiple data files hold the ``Ctrl`` or ``Cmd`` key while
117clicking on each data file.
118
119.. image:: figures/globalizer/ide_select_data.png
120
121Click run. While processing your model and data files the MiniZinc IDE
122will display a progress bar on the toolbar.
123
124.. image:: figures/globalizer/ide_globalized.png
125
126Any discovered global constraints will be listed in the output pane
127of the IDE. Clicking on one of these constraints will highlight in the
128model the expressions that might be replaceable or strengthened by the
129constraint.
130
131
132How it works
133------------
134A summary of the algorithm is presented here. For a more detailed
135exploration of the approach see the Globalizing Constraint Models paper [1]_.
136
137- **Normalize.**
138 In this step the model is transformed to make analysis easier.
139
140 - Conjunctions of constraints are broken into individual constraints.
141 For example: ``C1 /\ C2;`` becomes ``C1; C2``;
142
143 - Conjunctions under ``forall`` constraints are broken into individual
144 ``forall`` constraints. For example: ``forall(...) (C1 /\ C2);``
145 becomes ``forall(...) (C1); forall(...) (C2)``
146
147- **Generate submodels.**
148 In this step all subsets containing 1 or 2 constraints (this can be
149 configured using ``--numConstraints`` argument) are enumerated.
150
151- **Instantiate and unroll into groups.**
152 Each submodel is instantiated with the provided data files. These
153 instantiated submodels are further used to produce more submodels
154 by unrolling loops. For example, a constraint such as
155 ``forall(i in 1..n) (c(i));`` will be used to produce the constraints:
156 ``c(1)`` and ``c(n)`` for each instantiation of n in the data files.
157 All instantiated submodels are then grouped together.
158
159- **Process groups.**
160 For each submodel in a group a set of 30 random solutions are found.
161 (configurable using the ``--randomSolutions`` argument).
162 A template model with all of these random solutions is created.
163
164 The different variables (including arrays and array accesses) and
165 parameters used by a submodel are collected into a set of potential
166 arguments along with the constant 0 and a special blank symbol
167 representing an argument that can be inferred based on others used.
168
169 The list of constraints above is filtered based on the arguments
170 available. For example, the ``alldifferent`` constraint will
171 be removed from the list of candidates if the submodel does not
172 reference any arrays of variables.
173
174 Finally the set of constraints are filtered by adding them to the
175 template and solving it. If the template is satisfiable, the
176 constraint accepts all of the random solutions.
177
178 30 sample solutions for each candidate constraint are generated.
179 (configurable using the ``--sampleSolutions`` argument).
180 The candidate is then ranked based on how many of these solutions
181 are also solutions to the original submodel. If its score is less
182 than some threshold the candidate is removed from the set of
183 candidates for this group and will not be tested on later
184 submodels.
185
186- **Report.**
187 The remaining candidates are presented to the user.
188
189Performance tips
190----------------
191Globalizing constraint models can be a time consuming task. If
192
193- **Use small or relatively easy instances.**
194 Globalizer solves many subproblems while processing your model and data files. Using easier instances can speed up the process considerably.
195
196- **Disable the initial pass.**
197 As discussed above, Globalizer performs two passes. The first pass tries to detect alternate viewpoints that can be added to your model. If you are confident that this will not be useful we recommend disabling this first pass using the ``--no-initial-pass`` argument.
198
199- **Narrow search using filters.**
200 Globalizer attempts to match a large selection of global constraints to subproblems in your model.
201 If you wish to check if only a few specific constraints are present you can focus Globalizer using the ``--constraintFilter`` or ``-f`` arguments followed by a comma separated list of strings.
202 Only global constraints where one of the strings is a substring will be included in the search.
203
204- **Disable implies check.**
205 The implication check can also be disabled to improve performance. This results in less accurate results but may still help a user to understand the structure of their model.
206
207- **Free-search.**
208 To improve accuracy and to avoid false positives, subproblems solved by Globalizer are solved using a random heuristic and restarts. If the subproblems are particularly difficult to solve a random heuristic may be prohibitive and the solver may not be able to produce enough samples within the solving timelimit.
209 In these circumstances a user can either increase the solver timeout using the ``-t`` argument followed by the number of milliseconds a solver should be given to find samples.
210 Alternatively the ``--free-search`` argument can be used to force Globalizer to use the solver's free search to find samples.
211 This has the downside of reducing the diversity of samples but allows enough samples to be found to allow suggested globals to be found.
212
213Limitations / Future work
214-------------------------
215- Globalizer supports only a subset of the MiniZinc language and as such
216 cannot be executed on all MiniZinc models.
217- There are some relatively cheap syntactic approaches that should
218 be performed before Globalization that currently is not implemented.
219 For example, there are several common formulations of an ``alldifferent``
220 constraint that can be detected syntactically. This would be much
221 cheaper than using Globalizer.
222
223
224.. [1] Leo, K. et al., "Globalizing Constraint Models", 2013.
225.. [2] http://www.csplib.org/Problems/prob001/