Sweep based DiffN Propagator

[dannem1337]

A Sweep based DiffN Propagator created within this master thesis.

What's been added

• DiffN propagator with explanations
• Integrations with minizinc
• Optimizations: Merge, Overhang and Sources and Targets
• Evaluations comparing with decomposition

TODOs

• BUG: From what I have seen, whenever a propagation determines the model to be unsatisfiable, it is deemed that we are constructing an empty conflict. Although, looking at the logs, the explanations seem valid. The regression test test_diffn_unsat and bug.mzn should capture this error. The following show the explanations for when this error could occur.

   0.005409190s TRACE propagate{level=0}:diffn: huub::constraints::int_diffn: reason of obj 0 in dimension 0 [1..1] >= 1
   0.005414600s TRACE propagate{level=0}:diffn: huub::constraints::int_diffn: reason of obj 0 in dimension 1 [1..1] < 2
   0.005417645s TRACE propagate{level=0}:diffn: huub::constraints::int_diffn: reason of obj 0 in dimension 1 [1..1] >= 1
   0.005420625s TRACE propagate{level=0}:diffn: huub::constraints::int_diffn: reason of obj 1 in dimension 0 [1..1] < 5
   0.005440054s TRACE propagate{level=0}:diffn: huub::constraints::int_diffn: reason of obj 1 in dimension 0 [1..1] >= -2
   0.005457176s TRACE propagate{level=0}:diffn: huub::constraints::int_diffn: reason of obj 1 in dimension 1 [1..1] < 5
   0.005463746s TRACE propagate{level=0}:diffn: huub::constraints::int_diffn: reason of obj 1 in dimension 1 [1..1] >= -2

• The explanation for conflict could probably be improved. Currently conflict is only reasoned about in one dimensions though, it occurs in all dimensions since a conflict only occurs when a forbidden regions fully overlaps the active object.
• all_fr in generate_fr could be moved to self to reduce the number of allocations

[dannem1337]

Sorry for the delay, this should fix everything we discussed during the meeting! :D What has been added:

• Non-strict testcase
• store sizes and origins in one Dimstore struct
• Remove unused case coalesce

[Dekker1]

Sorry that this took a lot longer than it probably should have. I finally freed up some time to refactor the code base. I've updated it to the latest changes in the solver, and I've made a few changes to the data structures. (I think I put you on the wrong track with the DimStore. That was not what I meant). Furthermore, I went through some of the naming and documentation and tried to improve where I could.

@dannem1337, I would appreciate it if you could have another look through the codebase, just to see whether there are any obvious problems that you can find or whether there are any misunderstandings that made it into the documentation.

Afterwards, I think this will be ready to merge.

[dannem1337]

A bug seems to have been introduced in 683c6a6 that didn't exist before

The following model gives a result where some rectangles are overlapping, my guess is that is that something something is wrong when checking conflict. I will continue to investigate this tomorrow

include "diffn.mzn";

int: n = 14;
int: maxLen = 100;
array[1..n] of 1..n: Squares = [i | i in 1..n];

var n..maxLen: w;
var n..maxLen: h;
var int: rec = w*h;
array [1..n] of var 0..maxLen: X;
array [1..n] of var 0..maxLen: Y;
constraint forall(i in 1..n) (X[i] <= w-Squares[i] /\ Y[i] <= h-Squares[i]);
constraint diffn(X, Y, Squares, Squares);
solve minimize rec;
output ["w:\(w) h:\(h) X:\(X) Y:\(Y) rec: \(rec) squares: \(Squares)"];

Here's a picture of what it generates

[Dekker1]

Great catch! I think I found the problem. It appears that I thought that I rewrote Region::coalensce to return similar to .cmp, but it was the other way around. I've pushed a fix, which for me works on the instance you posted. I checked using the following extra output:

output
[ let {array[int] of bool: overlap = [fix(X[i]) + Squares[i] <= fix(X[j]), fix(Y[i]) + Squares[i] <= fix(Y[j]), fix(X[j]) + Squares[j] <= fix(X[i]), fix(Y[j]) + Squares[j] <= fix(Y[i])] } in if not(exists(overlap)) then "\(i) overlaps with \(j)\n" else "" endif | i,j in 1..n  where i < j];

That initially gave me the overlap, and after the fix no longer does. (I didn't have the fancy visualizations).

[CervEdin]

• a possible bug identified
• a possible fix of TODO proposed

also, fixed a typo here:
dannem1337#3