[BUG] Incorrect UNSAT for sub_circuit when reified

[ThomSerg]

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:

public static void main(String[] args) { 
    int n = 3; 
    Model model = new Model(); 

    IntVar[] nodes = model.intVarArray(3, 0, n - 1); 
    IntVar length = model.intVar(0, n); 

    BoolVar a = model.subCircuit(nodes, 0, length).reify(); 
    model.arithm(a, "=", 1).post(); 

    model.arithm(nodes[0], "!=", 0).post(); 
    model.arithm(nodes[1], "=", 1).post(); 
    model.arithm(nodes[2], "!=", 2).post(); 

    Solver solver = model.getSolver(); 
    System.out.println(solver.findSolution()); 

    for(IntVar v : nodes) {System.out.println(v);} 
    System.out.println(length); 
}

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:

model.arithm(nodes[0], "=", 2).post(); 
model.arithm(nodes[1], "=", 1).post(); 
model.arithm(nodes[2], "=", 0).post(); 

But representing it like the following, which should give the same results, it returns UNSAT:

model.arithm(nodes[0], "!=", 0).post(); 
model.arithm(nodes[1], "=", 1).post(); 
model.arithm(nodes[2], "!=", 2).post(); 

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

[cprudhom]

Thank you for the bug reporting. I think I found the reason of the bug, I will push a patch ASAP

[cprudhom]

Explanations

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.