You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There seems to be an inconsistency when using the sub_circuit global constraint within a reified context and when enforcing a particular solution. In a non-reified context the constraint acts as expected, but in the reified setting it incorrectly returns UNSAT for certain formulations. I know it should be SAT, and when formulating the problem a bit differently Choco agrees.
We originally detected this bug though pychoco, but we were able to replicate it in the java version too.
To Reproduce
The issue can be replicated with the following minimal model:
It basically formulates a subcircuit over three nodes and places it in a reified context, i.e. a -> sub_circuit(x). We enforce a to be True so that we (should) get the same behaviour as posting sub_circuit at top level.
Next, I want to enforce the solution [2, 1, 0], thus a subcircuit between 0 and 2. When posting it like the following, everything is fine:
It does however work correctly when sub_circuit is in a non-reified context.
An additional strange behaviour is that I can get it to become satisfiable again by incorrectly setting the domain upper-bound for length to n-1 (no longer allowing for subcircuits over all nodes).
Expected behaviour
The two ways of enforcing the solution to be [2, 1, 0] should both return SAT, and thus have the same behaviour as when posted at top level.
With kind regards,
Thomas
The text was updated successfully, but these errors were encountered:
Because the constraint subCircuit is composed of 3 propagators, when the reification is activated (by setting the Boolean variable to true), each propagator is activated separately.
In your example, the PropAlldifferent propagator is able to remove values from nodes[0] and nodes[2], stacking the modifications into the propagation engine.
Then the PropSubcircuit propagator is activated, taking the modified domains as input.
Finally, the modifications stacked are popped and the concerned propagator (including PropSubcircuit) are scheduled for propagation. When PropSubcircuit is propagated, it receives events already managed and fails.
I fixed ReificationConstraint and ImpliedConstraint to call model.getSolver().getEngine().execute(propagators[p]); instead of propagators[p].propagate(PropagatorEventType.FULL_PROPAGATION.getMask()); to schedule propagators after each propagator activation which fixes the bug.
Hello choco team,
Describe the bug
There seems to be an inconsistency when using the
sub_circuit
global constraint within a reified context and when enforcing a particular solution. In a non-reified context the constraint acts as expected, but in the reified setting it incorrectly returns UNSAT for certain formulations. I know it should be SAT, and when formulating the problem a bit differently Choco agrees.We originally detected this bug though pychoco, but we were able to replicate it in the java version too.
To Reproduce
The issue can be replicated with the following minimal model:
It basically formulates a subcircuit over three nodes and places it in a reified context, i.e.
a -> sub_circuit(x)
. We enforcea
to be True so that we (should) get the same behaviour as postingsub_circuit
at top level.Next, I want to enforce the solution
[2, 1, 0]
, thus a subcircuit between 0 and 2. When posting it like the following, everything is fine:But representing it like the following, which should give the same results, it returns UNSAT:
It does however work correctly when
sub_circuit
is in a non-reified context.An additional strange behaviour is that I can get it to become satisfiable again by incorrectly setting the domain upper-bound for
length
ton-1
(no longer allowing for subcircuits over all nodes).Expected behaviour
The two ways of enforcing the solution to be
[2, 1, 0]
should both return SAT, and thus have the same behaviour as when posted at top level.With kind regards,
Thomas
The text was updated successfully, but these errors were encountered: