this repo has no description
dekker.one
1FindMUS
2=======
3
4Version: 0.6.0
5
6FindMUS [1]_ lists unsatisfiable subsets of constraints in your MiniZinc
7model. These subsets, called Minimal Unsatisfiable Subsets can help
8you to find faults in your unsatisfiable constraint model. FindMUS uses
9the hierarchical structure provided by the model to guide its search.
10
11Basic Usage
12-----------
13
14To use FindMUS on the command line simply execute it on a model and set
15of data files by typing:
16
17``findMUS model.mzn data-1.dzn``
18
19This will perform a search for a single instance level MUS.
20To acquire a low level MUS the ``--paramset fzn`` argument can be used.
21To search for more than one MUS use the ``-a`` or ``-n <count>`` arguments.
22By default FindMUS will use ``gecode_presolver`` for checking the
23satisfiability of a subset of constraints. This can be changed using the
24``--subsolver`` argument. For example, given a model that is better
25suited to a Mixed Integer Programming solver, the argument
26``--solver cbc`` could be used to instruct FindMUS to flatten the model
27with the linear library and use the CBC solver for satisfiability checking.
28
29Note: FindMUS requires a fully instantiated constraint model.
30
31Commandline arguments
32^^^^^^^^^^^^^^^^^^^^^
33
34The FindMUS tool supports the following arguments:
35
36**Driver options**
37
38The driver creates the map solver and sub-solver and requests MUSes from
39FindMUS's enumeration algorithm HierMUS.
40
41``-n <count>`` Stop after the *n* th MUS is found (Default: 1)
42
43``-a`` Find all MUSes (equivalent to ``-n 0``)
44
45``-t`` or ``--timeout <s>`` Stop search after *s* seconds (Default: 1800)
46
47``--paramset hint,mzn,fzn``
48 Use a preset collection of parameters. (Default: mzn)
49 The ``mzn`` and ``fzn`` options can acquire MUSes in more detail.
50
51 ``hint`` --structure gen --depth mzn --shrink-alg map_lin
52
53 ``mzn`` --structure normal --depth mzn --shrink-alg map_qx
54
55 ``fzn`` --structure normal --depth fzn --shrink-alg map_qx
56
57``--no-leftover``
58 Do not print leftover candidate on timeout
59 If FindMUS is exploring an unsatisfiable subset when it runs out of time,
60 it behaves as if the set could not be reduced to a smaller set and prints
61 it as an MUS. The ``--no-leftover`` setting disables this behaviour as
62 these sets can sometimes be quite large.
63
64``--frequent-stats`` Print statistics after every MUS discovered.
65
66``--no-progress`` Disable ``%%%mzn-progress`` output
67
68``--no-stats`` Disable output of initial parsing stats and summary stats
69
70``--output-{html, json, brief, human}`` Changes output mode
71
72 ``html`` HTML output mode for use with the MiniZinc IDE
73
74 ``json`` Simple json output (each MUS should be parsed separately)
75
76 ``brief`` Same as the default output mode but without outputting the traces (paths)
77
78 ``human``
79 Tries to format the MUS in a more readable form grouping constraints by their constraint names
80
81
82**Compiler Options**
83
84``-g`` or ``--domains`` Record domain changes during compilation (same as ``minizinc -c -g``)
85
86``--verbose-compile`` Pass ``--verbose`` to MiniZinc compiler
87
88
89**Enumeration options**
90
91The enumeration algorithm (HierMUS) explores the constraint hierarchy
92provided in the user's model and proposes potential MUSes to the
93sub-solver. A ``shrink`` algorithm is used to reduce found UNSAT subsets
94to MUSes. There are currently four available shrink algorithms available
95with FindMUS.
96
97``--shrink-alg lin,map_lin,qx,map_qx,qx2``
98 Select shrink algorithm (Default: map_lin)
99
100 ``lin`` simple linear shrink algorithm.
101
102 ``map_lin`` alternative implementation of the linear algorithm that
103 updates a global map of explored subsets while shrinking the subset.
104
105 ``qx`` uses the ``QuickXplain`` [4]_ algorithm to shrink the subset
106 to a MUS.
107
108 ``map_qx`` is an alternative implementation of ``QuickXplain`` that
109 uses the global map to split subsets, and to avoid repeating any SAT
110 checks while shrinking
111
112 ``qx2`` a lightweight alternative to ``map_qx`` that only uses the
113 map to avoid repeating SAT checks.
114
115``--depth mzn,fzn,<n>``
116 How deep in the tree should search explore. (Default: mzn)
117
118 ``mzn`` expands the search as far as the point when the compiler
119 leaves the MiniZinc model.
120
121 ``fzn`` expands search as far as the FlatZinc constraints.
122
123 ``<n>`` expand search to the *n* level of the hierarchy.
124
125``--restarts`` Enable restart to flat mode (plain Marco) if large run of SAT sets encountered
126
127``--seed <n>`` Set the random seed used for splitting with ``map_qx``
128
129**Subsolver options**
130
131FindMUS can be used in conjunction with any FlatZinc solver. These
132options mimic the ``minizinc`` arguments ``--solver`` and
133``--fzn-flags``. The behavior of these arguments is likely to change
134in later versions of the tool.
135
136``--subsolver <s>``
137 Use solver *s* for SAT checking. (Default: "gecode")
138
139``--solver-flags <f>``
140 Pass flags *f* to sub-solver. (Default: empty)
141
142``--solver-timelimit <ms>``
143 Set hard time limit for solver in milliseconds. (Default: 1100)
144
145``--adapt-timelimit``
146 Automatically tighten solver timelimit based on
147 performance during initial sanity check (prove background is SAT,
148 background + entire foreground is UNSAT)
149
150**Filtering options**
151
152FindMUS can include or exclude constraints from its search based on the
153expression and constraint name annotations as well as properties of their
154paths (for example, line numbers). These filters are currently based on
155substrings but in future may support text spans and regular expressions.
156
157``--soft-defines``
158 Consider functional constraints as part of MUSes
159
160``--hard-domains``
161 Consider domain constraints (added by ``-g`` option) as background
162
163``--named-only``
164 Only consider constraints annotated with string annotations
165
166``--filter-mode fg,ex`` Filtering mode
167
168 ``fg`` Foreground: Excluded items go to the background
169
170 ``ex`` Exclusive: Excluded items are omitted entirely (Useful if they are
171 part of MUSes you are not interested in)
172
173``--filter-named <names>`` ``--filter-named-exclude <names>``
174Include/exclude constraints with names that match *sep* separated *names*
175
176``--filter-path <paths>`` ``--filter-path-exclude <paths>``
177Include/exclude based on *paths*
178
179``--filter-sep <sep>`` Separator used for named and path filters
180
181
182**Structure options**
183
184The structure coming from a user's model can significantly impact the
185performance of a MUS enumeration algorithm. The hierarchy is constructed
186in two steps. The first takes the existing model structure and can modify
187it in several ways. The second step adds extra binary structure.
188
189``--structure flat,gen,normal,mix``
190
191 Alters initial structure: (Default: ``gen``)
192
193 ``flat`` Remove all structure
194
195 ``gen`` Remove instance specific structure (merges constraints)
196
197 ``normal`` No change
198
199 ``mix`` Apply ``gen`` before ``normal``
200
201 ``idx`` Remove all location information
202
203 ``idxmix`` Apply ``idx`` before ``normal``
204
205
206``--no-binarize``
207
208 By default FindMUS will introduce extra binary structure to the
209 hierarchy. This option disables this behaviour (This is likely to be
210 the default in future since QX performs a type of binarization).
211
212**Verbosity options**
213
214``--verbose-{map,enum,subsolve} <n>`` Set verbosity level for
215different components. Currently ``n`` can only take values 0, 1, and 2;
216
217``--verbose`` Set verbosity level of all components to 1
218
219**Misc options**
220
221``--dump-dot <dot>`` Write tree in GraphViz format to file <dot>
222
223Example
224^^^^^^^
225
226The following demonstrates the basic usage of FindMUS on a simple example.
227Below, we see a model for the latin squares puzzle [2]_ with some
228incompatible symmetry breaking constraints added.
229
230
231.. literalinclude:: examples/latin_squares.mzn
232 :language: minizinc
233 :name: ex-mus-latin
234 :caption: Faulty model for Latin Squares (:download:`latin_squares.mzn <examples/latin_squares.mzn>`).
235
236Here we have used the new constraint and expression annotations
237added in MiniZinc 2.2.0. Note that these annotations are not
238necessary for FindMUS to work but may help with interpreting the
239output. The first two constraints: ``ADRows`` and ``ADCols`` define the
240``alldifferent`` constraints on the respective rows and columns of the
241latin square. The next two constraints ``LLRows`` and ``LGCols`` post
242``lex`` constraints that order the rows to be increasing and the columns
243to be increasing. Certain combinations of these constraints are going
244to be in conflict.
245
246Executing the command ``findMUS -n 2 latin_squares.mzn``
247returns the following output. Note that the ``-n 2`` argument requests
248that just the first two MUSes are found.
249
250.. code-block:: minizincdef
251
252 FznSubProblem: hard cons: 0 soft cons: 10 leaves: 10 branches: 11 Built tree in 0.02854 seconds.
253 MUS: 7 3 6 4 8
254 Brief: gecode_all_different_int;@{ADCols@AD(col 1)}:(j=1)
255 gecode_all_different_int;@{ADCols@AD(col 2)}:(j=2)
256 gecode_array_int_lt;@{LGCols@LG(cols 1 2)}:(j=1)
257 gecode_array_int_lt;@{LLRows@LL(rows 1 2)}:(i=1)
258 gecode_array_int_lt;@{LLRows@LL(rows 2 3)}:(i=2)
259
260 Traces:
261 latin_squares.mzn|18|5|20|9|ca|forall;latin_squares.mzn|18|5|20|9|ac;latin_squares.mzn|18|13|18|13|i=2;latin_squares.mzn|19|10|19|37|ca|lex_less
262 latin_squares.mzn|13|5|15|9|ca|forall;latin_squares.mzn|13|5|15|9|ac;latin_squares.mzn|13|13|13|13|j=1;latin_squares.mzn|14|10|14|30|ca|alldifferent
263 latin_squares.mzn|18|5|20|9|ca|forall;latin_squares.mzn|18|5|20|9|ac;latin_squares.mzn|18|13|18|13|i=1;latin_squares.mzn|19|10|19|37|ca|lex_less
264 latin_squares.mzn|13|5|15|9|ca|forall;latin_squares.mzn|13|5|15|9|ac;latin_squares.mzn|13|13|13|13|j=2;latin_squares.mzn|14|10|14|30|ca|alldifferent
265 latin_squares.mzn|22|5|24|9|ca|forall;latin_squares.mzn|22|5|24|9|ac;latin_squares.mzn|22|13|22|13|j=1;latin_squares.mzn|23|10|23|40|ca|lex_greater
266
267 MUS: 7 3 5 6 8 9
268 Brief: gecode_all_different_int;@{ADCols@AD(col 1)}:(j=1)
269 gecode_all_different_int;@{ADCols@AD(col 3)}:(j=3)
270 gecode_array_int_lt;@{LGCols@LG(cols 1 2)}:(j=1)
271 gecode_array_int_lt;@{LGCols@LG(cols 2 3)}:(j=2)
272 gecode_array_int_lt;@{LLRows@LL(rows 1 2)}:(i=1)
273 gecode_array_int_lt;@{LLRows@LL(rows 2 3)}:(i=2)
274
275 Traces:
276 latin_squares.mzn|18|5|20|9|ca|forall;latin_squares.mzn|18|5|20|9|ac;latin_squares.mzn|18|13|18|13|i=2;latin_squares.mzn|19|10|19|37|ca|lex_less
277 latin_squares.mzn|13|5|15|9|ca|forall;latin_squares.mzn|13|5|15|9|ac;latin_squares.mzn|13|13|13|13|j=1;latin_squares.mzn|14|10|14|30|ca|alldifferent
278 latin_squares.mzn|13|5|15|9|ca|forall;latin_squares.mzn|13|5|15|9|ac;latin_squares.mzn|13|13|13|13|j=3;latin_squares.mzn|14|10|14|30|ca|alldifferent
279 latin_squares.mzn|18|5|20|9|ca|forall;latin_squares.mzn|18|5|20|9|ac;latin_squares.mzn|18|13|18|13|i=1;latin_squares.mzn|19|10|19|37|ca|lex_less
280 latin_squares.mzn|22|5|24|9|ca|forall;latin_squares.mzn|22|5|24|9|ac;latin_squares.mzn|22|13|22|13|j=1;latin_squares.mzn|23|10|23|40|ca|lex_greater
281 latin_squares.mzn|22|5|24|9|ca|forall;latin_squares.mzn|22|5|24|9|ac;latin_squares.mzn|22|13|22|13|j=2;latin_squares.mzn|23|10|23|40|ca|lex_greater
282 Total Time: 0.39174 nmuses: 2 map: 40 sat: 21 total: 61
283
284The first line, starting with ``FznSubProblem:`` provides some useful
285information for debugging the ``findMUS`` tool. Next we have the list of MUSes.
286Each MUS is described with three sections:
287
288 #. ``MUS:`` lists the indices of the FlatZinc constraints involved in
289 this MUS.
290 #. ``Brief:`` lists the FlatZinc constraint name, the
291 expression name, the constraint name, and the loop index assignments
292 for each involved FlatZinc constraint.
293 #. ``Traces:`` lists the MiniZinc paths corresponding to the constraints
294 of the MUS.
295 Each path typically contains a list of path elements separated by
296 semi-colons ``;``. Each element includes a file path, a start line,
297 start column, end line and end column denoting a span of text from
298 the listed file. And finally, a description of the element.
299 In the examples above all paths point to calls to a forall on
300 different lines of the model. (``ca|forall``)
301
302The final line of output lists the ``Total Time``, the number of MUSes
303found, and some statistics about the number of times the internal map
304solver ``map`` was called, and the number of times the subproblem solver
305was called ``sat``.
306
307Interpreting these two MUSes we see that the ``lex`` constraints are
308incompatible with the ``alldifferent`` constraints.
309
310
311Using FindMUS in the MiniZinc IDE
312---------------------------------
313
314To use FindMUS in the MiniZinc IDE, upon discovering that a model is
315unsatisfiable. Select ``FindMUS`` from the solver configuration dropdown
316menu and click the solve button (play symbol).
317This will look for MUSes using the default ``--paramset mzn`` argument.
318
319.. image:: figures/findmus/ide_depth_mzn.png
320
321In this case we can see that the output pane shows the constraints
322involved in the MUS in terms of the expression annotations, grouped
323by the constraint annotations. Clicking on the MUS in the output pane
324will highlight the constraints in your model.
325
326If finding MUSes with ``--paramset mzn`` is prohibitively slow,
327you can try running instead with ``--paramset hint``.
328This merges many of the low level constraints into larger units
329and should be relatively fast and help locate the relevant constraint
330items. The following shows the result:
331
332.. image:: figures/findmus/ide_depth_1.png
333
334Selecting the returned MUS highlights three top level constraints as
335shown: ``ADRows``, ``LLRows`` and ``LGCols``.
336
337Alternatively, in some cases you may wish to look at the MUSes of your
338model in terms of the flattened FlatZinc program. To display these
339MUSes run FindMUS with the ``--paramset fzn`` argument.
340
341.. image:: figures/findmus/ide_depth_fzn.png
342
343In this figure you can see that the MUSes are expressed in terms of
344FlatZinc constraints along with any assignments to relevant loop variables.
345Clicking on this MUS also opens and highlights the source of the constraints
346in the MiniZinc library (in this case in Gecode's custom redefinition of
347``fzn_all_different_int``.
348
349How it works
350------------
351A simple explanation of the algorithm is presented here. For a more
352detailed exploration of an earlier version of the approach see the
353Debugging Unsatisfiable Constraint Models paper [1]_.
354
355The approach takes the full FlatZinc program and partitions the constraints
356into groups based on the hierarchy provided in the user's model. To
357begin with (at depth '1') we search for MUSes in the set of top level
358constraint items using the MARCO [3]_ MUS enumeration algorithm. If we
359are not at the target depth we recursively select a found MUS, split
360its constituent constraints into lower level constraints based on the
361hierarchy and begin another search for MUSes underneath this high-level
362MUS. If any MUSes are found we know that the high-level MUS is not minimal
363and so it should not be reported. This process is repeated on any found
364unsatisfiable subsets until we reach the required depth at which point
365we will start to report MUSes. If in the recursive search we return to a
366high-level MUS without finding any sub-MUSes we can report this MUS as
367a real MUS. This recursive process is referred to as HierMUS. At each
368stage when we request the enumeration of a set of MUSes underneath a
369high-level MUS we can use one of several MUS enumeration algorithms.
370
371
372Performance tips
373----------------
374
375If you are trying to find MUSes in a very large instance it is advised to
376make use of the filtering tools available. Use the default settings to
377find a very high-level MUS and then use the ``--depth`` option to find
378lower-level, more specific MUSes in conjunction with the ``--filter-name``
379and ``--filter-path`` options to focus on finding specific sub-MUSes of a
380found high-level MUS.
381
382When parameter tuning for FindMUS the oracle checker mode can speed up
383testing of different sets of parameters.
384
385 1. Run ``findMUS -a --paramset fzn --output-brief ... > muses.log`` to
386 save the output log to a file.
387
388 2. Run subsequent sets of parameters with
389 ``findMUS -a --paramset fzn --output-brief --oracle-only muses.log ...``.
390 The oracle mode will perform enumeration without making calls to the
391 sub-solver, instead deciding SAT/UNSAT based on the MUS log (omit
392 ``--oracle-only`` to call the sub-solver when the status of a
393 subset is unknown)
394
395
396Limitations / Future work
397-------------------------
398
399There are several features that we aim to include quite soon:
400
401 Solver core/MUS/IIS integration
402 Set shrinking can be accelerated by using problem specific
403 MUS extraction methods that some solvers provide.
404
405 Context-find
406 Once a MUS has been found flip the foreground + background
407 and narrow down the parts of the background that complete
408 the MUS
409
410 Regular expression based filtering
411 This will allow more complex filtering to be used.
412
413 Text span based filtering
414 This will allow a user to simply click-and-drag a selection around the
415 parts of a constraint model they wish to analyse.
416
417.. [1] Leo, K. et al., "Debugging Unsatisfiable Constraint Models", 2017.
418.. [2] https://en.wikipedia.org/wiki/Latin_square
419.. [3] Liffiton, M. H. et al., "Fast, Flexible MUS Enumeration", 2016.
420.. [4] Junker, U. et al., "QUICKXPLAIN: preferred explanations and relaxations for over-constrained problems", 2004.