minizinc 2.5.2 struggles with ground instances

[informarte]

minizinc 2.5.2 infers unsatisfiability for many ground instances (where all search variables have values assigned) which are verified by earlier minizinc versions.

minizinc-2.5.2-ground-instance-issue.tar.gz contains everything to reproduce the issue.

Reproduction steps:

tar xzvf minizinc-2.5.2-ground-instance-issue.tar.gz
cd minizinc-2.5.2-ground-instance-issue
ls
cd golomb
minizinc -I . solution.mzn

Expected output and what earlier minizinc versions produce:

Positions: [8, 0, 1, 2, 7, 6, 3, 4, 5]
Preferences satisfied: 8
----------
==========

Output from minizinc 2.5.2:

=====UNSATISFIABLE=====

Apart from photo, the archive contains four other instances where this issue occurs.

I also observed this issue with many problems from the minizinc-benchmarks library. So, if necessary, I could provide more test data.

[guidotack]

This is not in fact a bug in MiniZinc. The unsatisfiability is reported because your override of the symmetry breaking predicates doesn't work any longer.

The behaviour has changed due to a change in the Gecode MiniZinc library. When you run MiniZinc with one of the standard solvers, it uses the -G flag to locate its library. The -I flag however does not override the location given by -G, so you can't replace a solver's redefinitions-2.0.2.mzn file this way (this has always been the case). The reason why this worked in previous versions is that Gecode did not in fact have a redefinitions-2.0.2.mzn, this was only added in the latest version.

At the moment, there is no easy way to switch off symmetry breaking for solvers like Gecode without knowing where its library is located. You could create a copy of the library with your modified redefinitions file, e.g. call it gecode-nosym, and then run

minizinc -Ggecode-nosym solution.mzn

We'll have to think of some other way of switching off symmetry breaking, ideally with a library option that can be enabled easily without replacing any files. At the moment the only way I can see is to hard-code support for that into the compiler (so it would "know" about the special predicates and ignore them if symmetry breaking is switched off).

[informarte]

Thanks for the analysis!

It would be great to have a MiniZinc command-line option to switch off symmetry breaking! What about new keywords symmetry_breaking_constraint and redundant_constraint which can be used like constraint?

In the meanwhile, to make the copy approach work with my Yuck CI, I will probably proceed as follows:

1. Fork libminizinc on GitHub
2. Create a branch for testing
3. Change gecode/redefinitions-2.0.2.mzn in this branch
4. Provide this branch to the Yuck CI as a Git submodule in the Yuck source tree

[cyderize]

I believe this should now work in 2.5.3 by specifying -D mzn_ignore_redundant_constraints=true and -D mzn_ignore_symmetry_breaking_constraints=true during solution checking which should force redundant and symmetry breaking constraints to be ignored.