Open mstrojny opened 9 months ago
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:
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.
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.
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:
the loop runs ~3 seconds on my machine with time limitation of 250 millis:
For more complicated models, it would run up to eternity.
Expected behavior Timeout works for all phases of solver.solve().
Environment: