Convert sequence to succession matrix with CP-SAT

Question

Say I have a sequence [3,1,0,2], where each element is a decision variable, i.e. I decide upon an optimal sequence of numbers. Is there an appropriate way to convert this sequence to a 2D succession matrix without introducing too many auxiliary variables?

Example

[3,1,0,2] becomes

[[0, 0, 1, 0],

[1, 0, 0, 0],

[0, 0, 0, 0],

[0, 1, 0, 0]]

Read as "0 is followed by 2" for the first row, "1 is followed by 0" in the second row etc. I need this matrix as a decision variable, at the premise that it is equal to the sequence.

If it is any help, I work with Python, using OR-tools version V9.8

Answer 1

Your matrix has n X n entries, you will need n x n x 2 Boolean variables.

One nxn matrix of variables for the mapping of integer variables to Boolean variables, and another matrix for the result (called succ below).

The rest is easy, for each variable, create the n Boolean variables, one per value.

Then encode

x[i] == j and x[i+1] == k <=> succ[j][k] 

and add for all j

at_most_one(succ[j])

See https://github.com/google/or-tools/blob/main/ortools/sat/docs/channeling.md for more details.

And

https://github.com/google/or-tools/blob/main/ortools/sat/docs/boolean_logic.md

Answer 2

Based on the suggestion, i came up with this, which seems to work.

X[i] is the order of integers with elements i

Z[j,k] is the succesion matrix, i.e. if j is followed by k

for i in range(n - 1):
    for j in range(n):
        for k in range(n):

            
            condition_j = model.NewBoolVar(f'condition_j_{i}_{j}')
            condition_k = model.NewBoolVar(f'condition_k_{i}_{k}')
            
           
            model.Add(x[i] == j).OnlyEnforceIf(condition_j)
            model.Add(x[i] != j).OnlyEnforceIf(condition_j.Not())
            
            model.Add(x[i+1] == k).OnlyEnforceIf(condition_k)
            model.Add(x[i+1] != k).OnlyEnforceIf(condition_k.Not())
            
            model.AddBoolOr([condition_j.Not(), condition_k.Not()]).OnlyEnforceIf(z[j, k].Not())
            

    
for j in range(n):
    model.AddAtMostOne(z[j, k] for k in range(n))
    
for k in range(n):
    model.AddAtMostOne(z[j, k] for j in range(n))
```