[BUG] InvalidSolutionException on UndirectedGraphVar

[kevin-delmas]

Describe the bug
The following code is raising an InvalidSolutionException since the solver finds a solution that is not satisfying the isConnected constraint.
The bug is quite difficult to reproduce since it depends on the variable selection strategy.
The error message is:

FAILURE >> REIF_95 = 1=>connected ([PropConnected(q)]), !REIF_95 = 1=>OPPOSITE ([PropOpposite(q)])

To Reproduce
The following Scala code is providing the MWE (sorry, it is quite large but I failed to reduce it further).
https://github.com/onera/pml-analyzer/blob/73-develop-a-choco-backend/src/main/scala/onera/pmlanalyzer/views/interference/examples/MWEChocoError.scala

Expected behavior
The program should find exactly 90,112 solutions to this problem, all ensuring that isConnected is satisfied

Possible solution
I am a new user of Choco, so I may not use the API properly, nevertheless I "fixed" the issue by removing the runtime test (prod settings) and checking that solution satisfies the connectivity constraint.
Obviously, this fix is not satisfactory.

val  model: Model = Model(Settings.prod())
...
while (solver.solve() && isConnected.isSatisfied == ESat.TRUE) {}

Environment (please complete the following information):

• Choco-solver version: 5.0.0-beta.1
• JRE : 17.0.2

[jgFages]

Why would you reify the connected constraint if all solution should satisfy it ?
You should post it directly : model.connected(g).post(); without introducing the reification isConnected variable.
Would this solve your problem ?

[kevin-delmas]

In this specific case, all solutions fulfil the connected constraint, but in the general problem some solutions are not.
Is the reification a potentiel problem for resolution?
If so, I can try to reformulate the problem.
I let you know.
Thank you for your help.

[kevin-delmas]

Avoiding using the reification seems to solve the problem.
Is there a way to find somewhere in the Choco documentation the constraints that should not be reified? Or is this a good practice that must be met for all Choco models?
Thank you for your help.

[jgFages]

Reification should only be used when necessary (i.e. when the constraint may indeed not be satisfied in some solutions) and avoided otherwise. The more global a constraint, the less likely to be reified.

This being said, it is supposed to work. The problem is that i could not execute your mwe... Maybe a wrong sbt/scala setup on my side. So i could not investigate more

[kevin-delmas]

Ok, I will keep in mind the good practice w.r.t. reification.
My problem was easily transformable into subproblems that are not relying on constraint reification.
I will try to provide a Java version of the MWE if it can help.

[jgFages]

Thanks yes it would be easier for me to analyse

[kevin-delmas]

Here find a standalone Java file throwing the InvalidSolutionException.
In this case, posting directly the isConnected constraint solves the problem.
But I face other situations (more complex cases) where the solver is still throwing the exception even when avoiding reification.
Please let me know if you need extra information.

The exception is
FAILURE >> REIF_313 = 1=>connected ([PropConnected(q)]), !REIF_313 = 1=>OPPOSITE ([PropOpposite(q)])

MWEChocoError.java

[cprudhom]

I tested your code with Choco-solver version: 5.0.0-beta.1 and the version under development (aka, Choco-solver version: 5.0.0-beta.2) and it seems that the bug was fixed.
I can investigate a little bit, for the record, but I suppose that the best I can do is just to find time to prepare the release...

[cprudhom]

If I'm correct, the correction was pushed on df2e900 (on branch xcsp)

[kevin-delmas]

I tested a slightly different code (attached to this post) with the last commit of xcsp branch f29f80f.
I still have the same exception.
The occurrence of the exception seems to depend on the variable selection.
That is why it is difficult for me to provide a simple example.

Please let me know if you need further info to solve this issue.

MWEChocoError.java

[cprudhom]

I was able to reproduce the bug (thanx) and to find the origin of the bug.
It comes from the fact that iterators over sets are reusable.

Failing case:
G = {{2,11}, {2,3,5,6,11}}

In the case of PropConnected, l.77, an iterator over the potential nodes (UB = {2,3,5,6,11}) is initialized and the iteration starts.
Then, it happens that the graph becomes instantiated because 3, 5, and 6 are removed by the connected propagator.
At this point, the iterator is still in used, the next value to iterate on is 11 but since the variable is instantiated, its monitors are notified. On monitor is Dom/WDeg which check (for internal reason) that the variable is instantiated. This call executes an iteration of the upper bound of G. Which resets the (shared) iterator, goes to the end (11) and return true.
But, when it comes to the propagator again, the (shared) iterator has moved to 11 and the iteration stops before checking 11 (which should make the propagator fails).

Actually, this bug occurs also when debugging which makes the procedure quite unstable.

Conclusion:
We need to revamp the way iterators are shared. We can consider a pool of propagator, but a question needs to be clarified: how to recycle an iterator that stops early for good reason (failure, stop on correct conditions, etc) ?

[cprudhom]

This should be fixed when #1175 is fixed