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.

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