disjoint on fixed start times

[MaxOstrowski]

Would it be possible to allow for integers directly in the start times of the disjoint constraints ? I my general encoding I sometimes get instances where one of the start times is already set to a specific value, resulting in the grounding: &disjoint{(0@1),c19988,0; ("X_INTRODUCED_623_"@17),c19988,1; ("X_INTRODUCED_626_"@1),c19988,2; ("X_INTRODUCED_677_"@1),c19988,3; ("X_INTRODUCED_683_"@1),c19988,4}. which results in the ambigious error: *** ERROR: (clingcon): Invalid Syntax: invalid disjoint statement

[rkaminsk]

If I remember correctly, I restricted this to variables to make my life a little easier. I did not implement a translational approach for terms because this is tricky to do correctly (or at all) due to the implicit max/minint constraints. Feel free to implement support for a wider class of constraints but note that it will make reason generation more complicated. For your specific case, you should just introduce a variable and assign it to a fixed value. If there is no crazy amount of fixed values, then there should be almost no performance impact. The propagation will be the same in any case.

PS: I don't think this is a bug (but a wider class of supported constraints is always nice). I am going to remove myself as an assignee because I won't touch this.

[MaxOstrowski]

@rkaminsk Thanks a lot, I just added you s.t. you get the notification :smile: I'm unsure how I could distinguish numbers and other terms (variables) in gringo to actually do this in the encoding. disjoint {V@D : in(C, 0, I, V), in(C, 1, I, D)} :- constraint(C, "flatzingo_fixed_disjunctive").

[rkaminsk]

It's a bit messy. But there are some ways to test if something is an integer.

1. use gringo's total order: MININT <= V, V <= MAXINT,
2. use gringo's "undefined" term handling: is_int(V+0) :- in(C, 0, I, V), or
3. use scripting to implement an @is_int(V) function.

PS @MaxOstrowski: The @-syntax is better in this case. An assignee is probably the one to implement this. :wink: I am also watching clingcon now. So I will see all new issues.

[MaxOstrowski]

Neither using #sup and #inf as MAXINT/MININT, nor tempvar(C,I,V+0) :- in(C,0,I,V), constraint(C, "flatzingo_fixed_disjunctive"). works. For the latter, i simply get the output:

tempvar(c19988,0,0).
tempvar(c19988,1,"X_INTRODUCED_623_").
tempvar(c19988,2,"X_INTRODUCED_626_"). 
tempvar(c19988,3,"X_INTRODUCED_677_").
tempvar(c19988,4,"X_INTRODUCED_683_").

[MaxOstrowski]

So +0 does not work, but +1 :smile:

tempvar(C,I,V+1) :- in(C,0,I,V), constraint(C, "flatzingo_fixed_disjunctive").
&sum{tempvar(C,I)} = V-1 :- tempvar(C,I,V).
&disjoint {V@D : in(C, 0, I, V), in(C, 1, I, D), not tempvar(C,I,V+1); tempvar(C,I)@D : tempvar(C,I,V), in(C, 1, I, D)} :- constraint(C, "flatzingo_fixed_disjunctive").

[rkaminsk]

You cannot use #sup and #inf because these are the largest and smallest terms. Everything is smaller or equal to #sup and larger or equal to #inf. The +0 thing is a bug in clingo.

var_or_int(1).
var_or_int("a").

is_int_arith(V+X) :- var_or_int(V), X=0.
is_var_arith(V)   :- var_or_int(V), not is_int_arith(V).

is_int_comp(V) :- var_or_int(V), -2147483648<=V, V<=2147483647.
is_var_comp(V) :- var_or_int(V), V>2147483647.
is_var_comp(V) :- var_or_int(V), V<-2147483648.

[rkaminsk]

See potassco/clingo#218.