Usage of findMUS solver about minizinc-python HOT 3 OPEN

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.

from minizinc-python.

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.

from minizinc-python.

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.

from minizinc-python.