[BUG] Choco does not check for timeout during initialization phase

[mstrojny]

trafficstars

Describe the bug The timeout has no effect with specific conditions, which make loop in PropagationEngine.propagate() run long. The Solver is stuck in initialize() method.

To Reproduce The example will have no solutions:

import org.chocosolver.solver.Model;
import org.chocosolver.solver.Solver;
import org.chocosolver.solver.constraints.Constraint;
import org.chocosolver.solver.variables.IntVar;

public class ChocoTimeout
{
    @SuppressWarnings("nls")
    public static void main(String [] args)
    {
        Model model = new Model();
        
        IntVar v7 = model.intVar("@v7", IntVar.MIN_INT_BOUND, IntVar.MAX_INT_BOUND, true);
        IntVar v7mi2 = model.sum("v7-2", v7, model.intVar(-2));
        
        Constraint arithm1 = model.arithm(v7, ">", v7);
        Constraint arithm2 = model.arithm(v7, "<", v7);
        Constraint arithm3 = model.arithm(v7, ">=", v7mi2);
        Constraint arithm4 = model.arithm(v7, "!=", model.intVar(5));
        model.post(arithm1, arithm2, arithm3, arithm4);
        
        Solver solver = model.getSolver();
        solver.limitTime(250);
        
        long start = System.currentTimeMillis();
        boolean solved = solver.solve();
        long took = System.currentTimeMillis() - start;
        
        System.out.println("Solved: " + solved);
        System.out.println("Time in measures: " + (solver.getMeasures().getTimeCount() * 1000));
        System.out.println("Time in solve(): " + took);
    }
}

the loop runs ~3 seconds on my machine with time limitation of 250 millis:

Solved: false
Time in measures: 3741.5261
Time in solve(): 3743

For more complicated models, it would run up to eternity.

Expected behavior Timeout works for all phases of solver.solve().

Environment:

• Choco-solver version: 4.10.13

[cprudhom]

The minimal working example is:

Model model = new Model();

IntVar v7 = model.intVar("@v7", IntVar.MIN_INT_BOUND, IntVar.MAX_INT_BOUND, true);

Constraint arithm1 = model.arithm(v7, ">", v7);
Constraint arithm2 = model.arithm(v7, "<", v7);
model.post(arithm1, arithm2);

Solver solver = model.getSolver();
solver.limitTime(250);
// to profile propagation
PropagationProfiler p = solver.profilePropagation();

long start = System.currentTimeMillis();
boolean solved = solver.solve();
long took = System.currentTimeMillis() - start;
// to print propagation
ByteArrayOutputStream baos = new ByteArrayOutputStream();
PrintWriter pw = new PrintWriter(baos);
p.writeTo(pw, true);
pw.flush();
System.out.printf("%s", baos);

System.out.println("Solved: " + solved);
System.out.println("Time in measures: " + (solver.getMeasures().getTimeCount() * 1000));
System.out.println("Time in solve(): " + took);

Actually, you are posting two contradictory constraints: v7 > v7 and v7 < v7. x < y-like constraint is able to bound the domain of x and y as:

1. ub(x) <-- ub(y) - 1
2. lb(y) <-- lb(x) + 1

So, in your case, each call to a constraint removes 2 values from v7, namely the lower and the upper bound, until the domain of v7 becomes empty. This requires 21,474,835 propagations and 42,949,668 bound modifications, which is not free.

There is nothing I can do but considering is to detect inconsistent constraint like v7 > v7 and turn them into false constraint.

[mstrojny]

I am not aware that those constraints are contradictory when I post them. It would be sufficient to me if choco could detect the contradiction right away. But from API perspective, having something like:

Solver solver = <init>;
solver.limitTime();
solver.solve();

I would expect that execution of method solve() takes no longer than the limit. There is a potentially long-lasting for loop in PropagationEngine.propagate() and it looks like a good candidate to be secured with a timeout check anyway.