CP-SAT, breaking symmetries in graph coloring using lowest index color ordering

[fbahr]

Hello there...

I'd like to implement a symmetry breaking rule for the graph coloring problem which -- for a given graph G=(V,E) w/ V = {0,...,n} --basically requires that a color i (encoded by an integer 0 <= i <= m) can only be assigned to a vertex with index j if there's at least one other vertex with index k < j that is colored using color i+1.

Can this be achieved without introducing a "bunch" of binary variables `color[v,c]` encoding whether a vertex v is assigned color c. (Right now, I'm using integer variables w/ domain [0,...,m] to encode the coloring of a vertex. Hence, ideally, I'd be looking for something like:

"addImplication(x[v] == i, exists(x[w] == i+1 for w \in {0,v-1})").

Thanks in advance for your input,

FB

[Laurent Perron]

Remove the integer variable, and use the Boolean ones

 They will be created anyway, in addition to the integer variables. 

--
You received this message because you are subscribed to the Google Groups "or-tools-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/f25b5632-fb86-4b65-bc1b-7b98434a8240n%40googlegroups.com.

[fbahr]

I was afraid you'd say sth. like this ;-)

Well, it's a "bunch" of variables then...

Thanks for the advice!

On Thursday, July 21, 2022 at 6:23:53 PM UTC+2 Laurent Perron wrote:

Remove the integer variable, and use the Boolean ones

 They will be created anyway, in addition to the integer variables. 

Le jeu. 21 juil. 2022, 08:48, fbahr <floria...@gmail.com> a écrit :

Hello there...

I'd like to implement a symmetry breaking rule for the graph coloring problem which -- for a given graph G=(V,E) w/ V = {0,...,n} -- basically requires that a color i (encoded by an integer 0 <= i <= m) can only be assigned to a vertex with index j if there's at least one other vertex with index k < j that is colored using color i+1.

Can this be achieved without introducing a "bunch" of binary variables `color[v,c]` encoding whether a vertex v is assigned color c. (Right now, I'm using integer variables w/ domain [0,...,m] to encode the coloring of a vertex. Hence, ideally, I'd be looking for something like:

"addImplication(x[v] == i, exists(x[w] == i+1 for w \in {0,v-1})").

Thanks in advance for your input,

FB

[Laurent Perron]

Presolve will create them anyway. 

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/b17f1a41-a754-423f-a8e0-41108fd9eaa2n%40googlegroups.com.

[fbahr]

Sorry, for "nagging" you again... but:

Now, given both `x[v] = i` (`x` being a dict of IntVars, `v` a vertex index, and `i` the value assigned to `x[v]`) and `color[v,i]` (`color` being a dict of dicts of BoolVars, `color[v][i]` determining whether vertex `v` is assigned color `i`), the most basic way to relate those two "sets" of variables in a purely MIP setting clearly is to require

1) sum_i { color[v][i] } = 1 \forall v (or, in CP-SAT-speak: addExactlyOne)

2) x[v] = sum_i { i * color[v][i] } \forall v.

Is there a more elegant and/or efficient "CP-way" to achieve this (for instance -- not exactly sure what I'm talking about here -- maybe exploiting addElement)?

With kind regards,

FB

[Laurent Perron]

why do you need X, replace it with a list of Booleans

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/87f0db96-2804-4b8f-9884-87cd51b51259n%40googlegroups.com.