(A ^ B) FALSE, while A and B are TRUE?

[Pierre Haessig]

Hello,

I'm facing a strange result with the attached Minizinc model (using Minizing IDE 2.9.3 on Linux). It contains piecewise linear expressions (a mixture of floats and bools, in the spirit of my previous message).

It is quite long, but it contains the following constraints:

constraint gen_ok = (gen_ok1 /\ gen_ok2);

constraint op = gen_ok /\ ....

constraint ... /\ not op;
solve satisfy;

When solved with HiGHS, I get the UNSATISFIABLE status, which I believe is the correct answer.

However, if I solve with Gecode, not only do I get a satisfiable result, but also I get the following strange result:

gen_ok=false ....
gen_ok1=true  gen_ok2=true

which is pretty strange, since it boils down to (A ^ B) FALSE, while A and B are TRUE...

Did I make a syntax error?

Thanks for your feedback.

Best,

Pierre

[krzysztof....@gmail.com]

Just put parentesisi for 

constraint op = gen_ok /\ ....

so it will be 

constraint op = (gen_ok /\ ....)

Best,

/Kris

[Pierre Haessig]

Thanks for the feedback. I had spent some time studying operator precedence at https://docs.minizinc.dev/en/stable/spec.html#operators, but still I had missed that one. I guess I still have some "imperative language" bias where "=" stands for assignment.

Now, having fixed this I wonder if I still have some syntax error, or if I'm just facing a solving tolerance issue.

Here is the result of running  the updated code:

• Gecode: doesn't converge after some seconds
• COIN-BC: UNSATISFIABLE (which I expect to be the true result)
• HiGHS: returns the following satisfiable result, which is really at the edge of the constraints

nl=100.0
gen=-2.524757246869761e-15  gen_max=0.0
batt=100.0  batt_min=-0.0 batt_max=100.0
shed=-2.524757246869761e-15  spill=-2.524757246869761e-15
Decision tree: dt=true  dtcase=DT_maxbatt
nl_neg=false  nl_l_batt_min=false  nl_le_batt_max=true  nlmbatt_le_gen_max=true
Operating constraints: op=false
gen_ok=true  batt_ok=true  shed_ok=true  spill_ok=true  balance_ok=false (deltaP=0.0)

In particular, the odd result is at the end

balance_ok=false (deltaP=0.0)

where the relevant variables and constraints are:

set of float: bfloat = -100.0..100.0;
var bfloat: deltaP = gen+batt-spill - (nl-shed); % generation - load, including spillage and load shedding
var bool: balance_ok;
constraint balance_ok = (deltaP == 0.0);

Best,

Pierre

[krzysztof....@gmail.com]

I have got the following result from Gecode (JaCoP result is similar). 

nl=-99.9999999999999

gen=-0.0 gen_max=0.0

batt=-99.9999999999999 batt_min=-99.9999999999999 batt_max=0.0

shed=-0.0 spill=-1.4210854715202e-14

Decision tree: dt=false dtcase=DT_spill

nl_neg=true nl_l_batt_min=false nl_le_batt_max=true nlmbatt_le_gen_max=true

Operating constraints: op=false

gen_ok=true batt_ok=false shed_ok=true spill_ok=false balance_ok=false (deltaP=1.4210854715202e-14)

----------

I guess this is due to rounding errors in floating-point numbers :( It has been pointed out in several discussions on minizinc with floating-points and constraint solvers.

BTW, I used the following annotation for search.

solve :: float_search([nl, gen, gen_max, batt, batt_min, batt_max, shed, spill],
                      1e-16, most_constrained, indomain_split) satisfy;

[Pierre Haessig]

OK. Thanks for the tip about the annotation search. This raises two questions:

First, how comes the solver doesn't return Unsatisfiable, while key constraint is

constraint dt /\ not op;

but the output display states that dt=false.

Second, about the rounding issue with floating-point numbers, is it possible to generate the MILP representation (in particular when using HiGHS), say in a MPS or LP file. This would allow discussing the issue in HiGHS forum? Is this possible, or is the lowest level code that Minizinc can produce is only the .fzn file?

Best,

Pierre

[David Lloyd]

MiniZinc compiles to an intermediate representation called `FlatZinc`.

That is then compiled by other things to the final representation.

I don't know if they can output code but:

```

C:\Program Files\MiniZinc\bin\fz-cp-sat.exe --helfull

```

...outputs a lot of help so they may be able to.

Do understand though that the middle translation is rather gnarly - at least to me. I guess if I could understand and write the OR-TOOLs or GeCODE code directly, and as efficiently as MiniZinc's DSL I might use them (at the very least I'd avoid MiniZinc's sometimes long and memory intensive compile time)..

DSL

--
You received this message because you are subscribed to the Google Groups "MiniZinc" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minizinc+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/minizinc/db3934bf-6418-4b2f-90db-95c28fbf2f44n%40googlegroups.com.

[krzysztof....@gmail.com]

You are right. It is strange that constraint dt /\ not op holds when both dt and op are false. I have checked fzn and ozn file and find out that both dt and op are not part of fzn file. This is the file that is taken by solver to evaluate a model. These variables are defined in ozn file used by minizinc when printing results but not for constraint evaluation. I think minizinc only computes the values based on definitions :( 

They are defined as follows.

bool: dt = if nl_neg then gen==0.0 /\ shed==0.0 /\ if nl_l_batt_min then batt==batt_min /\ spill==batt-nl /\ dtcase==DT_spill else batt==nl /\ spill==0.0 /\ dtcase==DT_renew endif else spill==0.0 /\ if nl_le_batt_max then gen==0.0 /\ batt==nl /\ shed==0.0 /\ dtcase==DT_load else batt==batt_max /\ if nlmbatt_le_gen_max then gen==nl-batt /\ shed==0.0 /\ dtcase==DT_maxbatt else gen==gen_max /\ shed==nl-batt-gen /\ dtcase==DT_shed endif endif endif;
bool: X_INTRODUCED_17_ = false;
bool: 'op' = X_INTRODUCED_17_;

I think this explains the problem.

Best,

/Kris

[Pierre Haessig]

Thanks Kris and David for your feedback.

As you pointed out the floating point tolerance issue, I made a simpler example which made me realize I had no control over the following equality constraint in my previous Dispatch_verification.mzn example;

var bfloat: deltaP = gen+batt-spill - (nl-shed); % generation - load, including spillage and load shedding
var bool: balance_ok;
constraint balance_ok = (deltaP == 0.0);

In the new simpler decision_tree_check2.mzn example, I'm using instead:

float: tol=1e-5; % tolerance for accepting delta_x==0.0

var bfloat: delta_x;

delta_x = xpos - xneg - x ; % should be zero because x = xpos-xneg

balance_ok = abs(delta_x) <= tol;

And good news, the model works with HiGHS (i.e. it is returned as UNSATISFIABLE) for tol greater than about 2e-6.

However, I'm not sure where this "experimental" threshold value comes from. Indeed:

• default tolerance values for HiGHS are 1e-07 (see *_tolerance options https://ergo-code.github.io/HiGHS/dev/options/definitions/#primal_feasibility_tolerance)
  • but this 1e-07 value cannot be directly compared to tol, since I'm bounding all floats to live in [-100.0, 100.0], and I guess that HiGHS tolerance is relative to this
• but also I see that the compiled FlatZinc file is full of hardcoded 1e-06 values, either directly or indirectly (with values such as -200.000001), and I'm not sure where these values come from.
  • also, oddly enough, I don't see where the value of the `tol` parameter appear in this compiled FlatZinc code

Best,

Pierre

[krzysztof....@gmail.com]

Regarding your comment on value  -200.000001 and that you do not know where this value comes from. I guess, it is basically the result of minizinc compiler internal computations and accumulation of rounding-up and rounding-down operations on floating-point numbers. BTW, this also creates problems for solvers when doing their constraints evaluation...