I am writing a code that should solve a solitaire in MiniZinc. I have been asked to return a message "This solitaire cannot be solved" if the conditions are unsatisfiable.
Unfortunately, I could not find a solution to this problem in the Internet. Does anyone have an idea on how can I do that?
I don't know a fool-proof version to do this, in fact it's a bit tricky. But here are some thoughts.
The standard response when a model is not satisfied is "=====UNSATISFIABLE=====". You might write a wrapper program to replace this string to "This solitaire cannot be solved". This is probably what I would have done myself.
This string can be changed via the program "solns2out" (the program in the MiniZinc tool chain that does the pretty print of a solution) which has the parameter "--unsat-msg" where you can state your own message.
The parameter to solns2out is - what I know of - not available via MiniZincIDE so you have to roll your own tool chain so you have to write the complete chain of programs for using this such as
flatzinc model.mzn -some_parameters | solver model.fzn -with_some_parameters | solns2out model.ozn --unsat-msg "This solitaire cannot be solved"
It can be quite tricky dependent on how flexible you want it to be, e.g. what parameters you need etc.
(Sometimes it's easier to use the "minizinc" program instead of the "flatzinc" program. Run the programs with their -help option to see the different parameters.)