ShortTable decomposition#997
Conversation
WoutPiessens
force-pushed
the
short_table_decomp
branch
from
792e4e3 to
dac7060
Compare
tias
left a comment
tias
left a comment
There was a problem hiding this comment.
request for discussion, I'm not sure the current version is worth it
|
|
||
| # Since the tables use auxiliary variables not used anywhere else, they always admit a solution | ||
| # The ShortTable constraint is satisfied iff at least one channelling constraint is satisfied | ||
| return [cp.sum(channelling_cons) != 0], tables |
There was a problem hiding this comment.
mip solvers will appreciate that you write > 0 (we might do ugly things, because they dont support !=)
There was a problem hiding this comment.
actually, isn't this cp.exists??
There was a problem hiding this comment.
because of this part, I'm not sure its actually going to be faster...
an exists over all(iv==iv) requires an additional boolean variable for each aux==iv, and you already introduced all these aux's...
if you think about the MDD encoding of each of those tables, would the real flow encoding not have an in flow of 1, then unlabelled branches to the sources of each projected table's MDD, then (in parallel) the flow constraints on those mdds with the original variables, then from each of the sink nodes again unlabbeled branches to the real sink node, with the requirement that out flow=1 from this sink, e.g. over this parallel MDD (always using the original variables)?
I'm not sure we have an easy way to build this, I'm also not sure if you want to actually do it : ) but I wonder
| groups: defaultdict[tuple[int, ...], list[list[int]]] = defaultdict(list) | ||
|
|
||
| for row in tab.tolist(): # converts to Python ints | ||
| # Determine STAR pattern |
There was a problem hiding this comment.
I need a bit more pedagogical documentation here...
the 'star pattern' is the columns in this row that contain a star?
so why do you group by pattern?
then you will project those out and create shadow variables? and... one of those tables must match?
does this also contain the rows without star?
|
To explain the current decomposition: For every row in the ShortTable, consider the columns in which a STAR appears as a tuple, e.g. () for a row with no STARs, (2), (3,4), ... I call these the "patterns". All rows in the ShortTable with the same pattern are grouped together, and all the columns in the tuple of the pattern can be skipped over (this is the reason for grouping by pattern) : as a consequence we obtain a (normal) Table for every group. For example: [[1, STAR], [2, STAR], [STAR, 3], [0,0]] results in three tables: [[1], [2]] and [[3]] and [[0,0]], with respective patterns (1), (0), (). Now all these Table constraints use an auxiliary variable array. Then it must hold that the original array is equal to at least one auxiliary array (for all columns in the original array that are included in the auxiliary array). An alternative decomposition is to construct one MDD, namely the MDD obtained by decomposing the Table that is equivalent with the ShortTable. This will likely only work well if the MDD is reduced, otherwise a very large number of paths in the MDD may exist. I'm looking into a way to do this without having to construct the full Table / non-reduced MDD first, but it's not trivial. Essentially it comes down to performing reduce steps already during construction of the MDD. But I will further look into implementing this. I think the advantage of the current method compared to the alternative method is the fact that STARs can be fully skipped over, and the disadvantage is the use of auxiliary variables and channelling constraints. But when I have them both I would like to compare them and choose one. |
|
Implementing the alternative decomposition (with one MDD) will likely be significantly easier if we have a non-deterministic MDD, where in any node, there can be multiple outgoing edges with the same value. However, this raises the question if we want to support this for the current MDD global, or if it should be a separate global (presumably only in the competition branch). |
|
right, I'm not sure we should actually go all that way... we might be going a bit too far in a rabbit hole here, given that shorttable is rarely used... for the current decomposition; I'm not going to put it in master. We would need an experiment that shows that it is worth increasing our codebase (anything added must be maintained). You can add it in the xcsp3 branch if you wish... |
2 participants
This branch continues on #981 and implements a linear decomposition of the ShortTable global constraint into Tables, which can then be further decomposed into MDDs.
For every "star pattern" (set of columns in which STAR appears) occurring in the original ShortTable, an auxiliary table is constructed with auxiliary variables, which are channelled back to the original variables. The advantage of this is that in the auxiliary table, the columns containing STAR can be ignored.