Link Search Menu Expand Document
PyCSP3
Models & Data GitHub XCSP3 About

Constraint AllDifferentMatrix

The constraint AllDifferentMatrix ensures that the variables in each row and each column of a specified matrix take different values.

Below, we give several illustrations corresponding to representative use cases of the constraint AllDifferentMatrix.

Case 1: Simple AllDifferentMatrix

To see how this constraint works, we need first to import the library PyCSP$^3$:

from pycsp3 import *

For our illustration, we introduce a two-dimensional array $x$ of $4\times4$ variables, each one with {0,1,2,3} as domain.

x = VarArray(size=[4,4], dom=range(4))

We can display the structure of the array, and the domain of the first variable.

print("Matrix of variables: ", x)
print("Domain of the first variable: ", x[0][0].dom)
Matrix of variables:  [
  [x[0][0], x[0][1], x[0][2], x[0][3]]
  [x[1][0], x[1][1], x[1][2], x[1][3]]
  [x[2][0], x[2][1], x[2][2], x[2][3]]
  [x[3][0], x[3][1], x[3][2], x[3][3]]
]
Domain of the first variable:  0..3

Now, we simply post a single constraint AllDifferentMatrix on the variables of $x$. This is possible by calling AllDifferent while setting the value of the named parameter matrix to True:

satisfy(
    AllDifferent(x, matrix=True)
);

We can display the internal representation of the constraint that we have just posted.

print(posted())
allDifferent(matrix:(x[0][0],x[0][1],x[0][2],x[0][3])(x[1][0],x[1][1],x[1][2],x[1][3])(x[2][0],x[2][1],x[2][2],x[2][3])(x[3][0],x[3][1],x[3][2],x[3][3]))

By calling the function solve(), we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also display the values assigned to the variables in the found solution.

if solve() is SAT:
    print(values(x))
[
  [0, 1, 2, 3]
  [1, 0, 3, 2]
  [2, 3, 0, 1]
  [3, 2, 1, 0]
]

If ever we want to count the number of solutions, we can use the named parameter sols.

if solve(sols=ALL) is SAT:
    print("Last solution: ", values(x))
    print("Number of solutions: ", n_solutions())
Last solution:  [
  [3, 2, 0, 1]
  [0, 1, 2, 3]
  [2, 3, 1, 0]
  [1, 0, 3, 2]
]
Number of solutions:  576

Finally, note that this matrix form of AllDifferent is equivalent to post two groups (lists) of basic AllDifferent constraints, as follows:

satisfy(
    [AllDifferent(x[i]) for i in range(4)],
    [AllDifferent(x[:,j]) for j in  range(4)],
);

We can display the internal representation of all posted constraints. But, of course, only the constraint AllDifferentMatrix is necessary, and should be posted.

print(posted())
allDifferent(matrix:x[][])
allDifferent(list:[x[0][0], x[0][1], x[0][2], x[0][3]])
allDifferent(list:[x[1][0], x[1][1], x[1][2], x[1][3]])
allDifferent(list:[x[2][0], x[2][1], x[2][2], x[2][3]])
allDifferent(list:[x[3][0], x[3][1], x[3][2], x[3][3]])
allDifferent(list:[x[0][0], x[1][0], x[2][0], x[3][0]])
allDifferent(list:[x[0][1], x[1][1], x[2][1], x[3][1]])
allDifferent(list:[x[0][2], x[1][2], x[2][2], x[3][2]])
allDifferent(list:[x[0][3], x[1][3], x[2][3], x[3][3]])

Case 2: AllDifferentMatrix with Exceptions

A variant of AllDifferentMatrix enforces variables to take distinct values on each row and each column, except those that are assigned to some specified values (often, the single value 0). We use a named parameter called excepting for indicating the value(s) that must be ignored.

First of all, we need to remove everything that has been introduced so far by calling the function clear().

clear()  # to clear previously posted variables and constraints

We control that there are no more constraints.

print(posted())
[]

For our illustration, we introduce a two-dimensional array $x$ of $3\times3$ variables, each one with {0,1,2} as domain.

x = VarArray(size=[3,3], dom=range(3))

Now, we simply post a single constraint AllDifferentMatrix on the variables of $x$, while indicating that the value 0 must be ignored.

satisfy(
    AllDifferent(x, matrix=True, excepting=0)
);
We can run the solver.
if solve() is SAT:
    print(values(x))
[
  [0, 0, 0]
  [0, 0, 0]
  [0, 0, 0]
]

And we can count the number of solutions.

if solve(sols=ALL) is SAT:
    print("Last solution: ", values(x))
    print("Number of solutions: ", n_solutions())
Last solution:  [
  [1, 2, 0]
  [2, 0, 1]
  [0, 1, 2]
]
Number of solutions:  781