findMUS: two objective functions, different outputs

[cprudhom]

Hello

With @JolanPhilippe, we have a software stack that generates MiniZinc models.
Sometimes, the model generated is not consistent, so we use findMUS.
There was some unexpected behaviour and we realised that it was due to the declaration of the objective function.

Here are the two versions tested with MiniZincIDE version 2.8.3.
We don't understand why we have to declare the intermediate variable scost.
Can anyone help us with this?
Obviously, we can provide a model, if that helps.

Thank you

First version

model.mzn

% the model ...
solve minimize sum(cost);

comand line

/Applications/MiniZincIDE.app/Contents/Resources/bin/findMUS model.mzn

results in:

SubSolver: hard cons: 214 soft cons: 154 leaves: 154 branches: 169 Built tree in 0.05303 seconds.
SubSolver: Exception during sub-solving: GecodeSolverInstance::processFlatZinc: Error: Unbounded variable: X_INTRODUCED_104_, rerun with --allow-unbounded-vars to add arbitrary bounds.
: error

IDE
With the IDE, it results in:

Command: minizinc --json-stream --param-file-no-push /private/var/folders/14/7lwdz4lx3fn922xmc1kv0g600000gr/T/mzn_LBsEnF.mpc /Users/kyzrsoze/Downloads/model.mzn --output-html
Configuration:
{
    "intermediate-solutions": true,
    "solver": "[email protected]"
}
SubSolver: hard cons: 214 soft cons: 154 leaves: 154 branches: 169 Built tree in 0.05376 seconds.
MiniZinc:   

Finished in 296msec.

Second version

If I change the model to:

% the model ...
var int: scost;
constraint scost = sum(cost);
solve minimize scost;

I get:
comand line

SubSolver: hard cons: 214 soft cons: 154 leaves: 154 branches: 169 Built tree in 0.04780 seconds.
%%%mzn-progress 0.00
MUS: 104
Brief: int_eq_reif;:(i=11)

Traces:
/Users/kyzrsoze/Downloads/model.mzn|43|12|43|88|ca|forall;/Users/kyzrsoze/Downloads/model.mzn|43|12|43|88|ac;/Users/kyzrsoze/Downloads/model.mzn|43|20|43|20|i=11;/Users/kyzrsoze/Downloads/model.mzn|43|35|43|87|bin|'<->';/Users/kyzrsoze/Downloads/model.mzn|43|68|43|87|bin|'=';/Users/kyzrsoze/Downloads/model.mzn|43|68|43|87|ca|int_eq;/Users/kyzrsoze/Downloads/model.mzn|43|68|43|87|ca|int_eq_reif

%%%mzn-progress 100.00
%%%mzn-progress 100.00
Total Time: 0.19920	nmuses: 1	map:     11	sat:     10	total:     21

IDE

Command: minizinc --json-stream --param-file-no-push /private/var/folders/14/7lwdz4lx3fn922xmc1kv0g600000gr/T/mzn_LBsEnF.mpc /Users/kyzrsoze/Downloads/model.mzn --output-html
Configuration:
{
    "intermediate-solutions": true,
    "solver": "[email protected]"
}
SubSolver: hard cons: 214 soft cons: 154 leaves: 154 branches: 169 Built tree in 0.05527 seconds.
The following constraints are incompatible:
Uncategorised:
- model.mzn|43|68|43|87|ca|int_eq_reif ( i=11 )


----------
%%%mzn-stat: map=11
%%%mzn-stat: nmuses=1
%%%mzn-stat: sat=10
%%%mzn-stat: time=0.19706
%%%mzn-stat: total=21
%%%mzn-stat-end

[JolanPhilippe]

Hi all,

I would like to provide some additional details about the issues we are facing using FindMUS and Minizinc:

• an additional issue with the declaration of variables and constraints
• minzinc version issue

Declaration of variable and constraint

For convenience, we have preferred to eliminate global variables in our model. However, by removing the count global variable, we have encountered the same issue as outlined above, necessitating the decomposition of constrained variable definitions. Below are three models for comparison:

• Model v1 mirrors cprudhom's original model, utilizing 'count'.
• Model v2 removes count and decomposes it accordingly using sum
• Model v3 separates the declaration of the variable, and its constraints.

Model v1: Use of count global variable

constraint count (v in states) (v = deployed) > 0;

I get:

command line

SubSolver: hard cons: 131 soft cons: 96 leaves: 96 branches: 113 Built tree in 0.03669 seconds.
%%%mzn-progress 0.00
MUS: 59
Brief: int_eq_reif;:(i=13)

Traces:
/home/jolan/Documents/Projects/SeMaFor/Ballet/model.mzn|28|12|28|95|ca|forall;/home/jolan/Documents/Projects/SeMaFor/Ballet/model.mzn|28|12|28|95|ac;/home/jolan/Documents/Projects/SeMaFor/Ballet/model.mzn|28|20|28|20|i=13;/home/jolan/Documents/Projects/SeMaFor/Ballet/model.mzn|28|43|28|94|bin|'<->';/home/jolan/Documents/Projects/SeMaFor/Ballet/model.mzn|28|75|28|94|bin|'=';/home/jolan/Documents/Projects/SeMaFor/Ballet/model.mzn|28|75|28|94|ca|int_eq;/home/jolan/Documents/Projects/SeMaFor/Ballet/model.mzn|28|75|28|94|ca|int_eq_reif

%%%mzn-progress 100.00
%%%mzn-progress 100.00
Total Time: 0.05697	nmuses: 1	map:     12	sat:     11	total:     23

IDE

The following constraints are incompatible:
Uncategorised:
- Playground.mzn|43|68|43|87|ca|int_eq_reif ( i=11 )

----------
%%%mzn-stat: map=11
%%%mzn-stat: nmuses=1
%%%mzn-stat: sat=10
%%%mzn-stat: time=0.06592
%%%mzn-stat: total=21
%%%mzn-stat-end

Which are the expected outputs from cprudhom's example.

Model v2: Decomposed the global variable count

var int: count_deployed = sum(v in states) (v = deployed);
constraint count_deployed > 0;

I get:

command line

Warning: model inconsistency detected

SubSolver: hard cons: 1 soft cons: 0 leaves: 1 branches: 0 Built tree in 0.03684 seconds.
Background is not satisfiable, exiting. Try using --soft-defines.

IDE

Warning: model inconsistency detected

SubSolver: hard cons: 1 soft cons: 0 leaves: 1 branches: 0 Built tree in 0.04441 seconds.
Background is not satisfiable, exiting. Try using --soft-defines.

It seems findMUS is not able to construct/explore the tree.

Model v3: Decomposed counted value

var int: count_deployed;
constraint count_deployed = sum(v in states) (v = deployed);
constraint count_deployed > 0;

I get:

command line

SubSolver: hard cons: 223 soft cons: 154 leaves: 154 branches: 169 Built tree in 0.04085 seconds.
%%%mzn-progress 0.00
MUS: 104
Brief: int_eq_reif;:(i=11)

Traces:
/home/jolan/Documents/Projects/SeMaFor/Ballet/mm.mzn|43|12|43|88|ca|forall;/home/jolan/Documents/Projects/SeMaFor/Ballet/mm.mzn|43|12|43|88|ac;/home/jolan/Documents/Projects/SeMaFor/Ballet/mm.mzn|43|20|43|20|i=11;/home/jolan/Documents/Projects/SeMaFor/Ballet/mm.mzn|43|35|43|87|bin|'<->';/home/jolan/Documents/Projects/SeMaFor/Ballet/mm.mzn|43|68|43|87|bin|'=';/home/jolan/Documents/Projects/SeMaFor/Ballet/mm.mzn|43|68|43|87|ca|int_eq;/home/jolan/Documents/Projects/SeMaFor/Ballet/mm.mzn|43|68|43|87|ca|int_eq_reif

%%%mzn-progress 100.00
%%%mzn-progress 100.00
Total Time: 0.07015	nmuses: 1	map:     11	sat:     10	total:     21

IDE

SubSolver: hard cons: 223 soft cons: 154 leaves: 154 branches: 169 Built tree in 0.04526 seconds.
The following constraints are incompatible:
Uncategorised:
- Playground.mzn|43|68|43|87|ca|int_eq_reif ( i=11 )


----------
%%%mzn-stat: map=11
%%%mzn-stat: nmuses=1
%%%mzn-stat: sat=10
%%%mzn-stat: time=0.06299
%%%mzn-stat: total=21
%%%mzn-stat-end

which is now the expected output again.

MiniZinc versions

All the proceeded tests described in cprudhom's and this comment are made using Minizinc 2.7.6 and Minizinc 2.8.2.
However, using Minizinc 2.8.4, findMUS seems not working anymore... For the same models presented above, running FindMUS using terminal or MiniZincIDE returns

multiple errors: 

with no additional output.