Usage of findMUS solver

[SantiagoQUINTANA]

How can we implement ['/Applications/MiniZincIDE.app/Contents/Resources/minizinc', '--solver', '[email protected]', '--named-only', ...]?

I can use the argument when using '/Applications/MiniZincIDE.app/Contents/Resources/bin/findMUS' instead but I was wondering if there is a cleaner way of doing so when running with '--solver', '[email protected]'.

I also found that in driver.py the solver configuration ( arg = ["--allow-multiple-assignments"]) causes an error when creating an instance of findMUS solver. In addition I found an issue in instance.py in: 'self._driver.run(["--model-interface-only"]' .

Am I doing something wrong or it is python Minizinc not ready for findMUS solver?

[Dekker1]

Currently MiniZinc Python is not designed for FindMUS usage.

FindMUS is a very different from a normal MiniZinc solver (and MiniZinc Python has really been designed for solving MiniZinc instances). When you call MiniZinc --solver finds ... it doesn't actually call the MiniZinc compiler, instead everything passed on to the FindMUS (mzn) driver. Currently FindMUS does not support all the same flags as MiniZinc, including (--allow-multiple-assignments).

Although we could probably work around those issues, the bigger problem is that the output of FindMUS does not correspond to the normal MiniZinc solving output format (or it at least is not yet part of any standard). This means that MiniZinc Python currently doesn't contain any functionality to parse the output of FindMUS.

Although this could potentially be improved in the future, it would heavily depend on the development of a standard in the reporting of MUS/IIS. I haven't heard of any usage of FindMUS from MiniZinc Python and would be interested to hear in what way you are trying to use it and what the expected output from the library would be.

[SantiagoQUINTANA]

Thanks for the quick response @Dekker1 . I am using findMUS to obtain a list of conflicts (MUSes) and possible relaxations when we have an unfeasible schedule. I have created a parser of the output of findMUS and made some changes to MiniZinc Python to avoid errors with certain flags. I will clean the code and send a pull request so that others could continue with the development of findMUS.

[Dekker1]

That sounds great! We'll have to have a discussion in the MiniZinc team how we want to handle these kinds of solvers and in particular the output of MUS/IIS (which might also happen when you solve with a normal solver like Gurobi). Although it sounds like the parsed output for findMUS could already be a big help, in the end I would prefer generalised standards over special case handling for certain solvers.

[e-mugdan]

I want to use findMUS as well. However, I have the same problems as mentioned above.
Has there been any progress on the subject, or is there anything available that I could use to parse the output correctly?