Constraint ElementMatrix
The constraint ElementMatrix ensures that the element of a specified matrix
In Python, to post a constraint ElementMatrix, we use the facilities offered by the language, meaning that we can write expressions involving relational and indexing ([]) operators.
Variant 1
We consider the variant 1 of the constraint ElementMatrix:
To see how this constraint works, we need first to import the library PyCSP
from pycsp3 import *
We introduce a two-dimensional array
x = VarArray(size=[3, 2], dom=range(4))
i = Var(range(3))
j = Var(range(2))
v = Var(range(4))
We can display the structure of the array, as well as a few domains.
print("Array x: " ,x)
print("A few domains: ", x[0][0].dom, " ", i.dom, " ", j.dom, " ", v.dom)
Array x: [
[x[0][0], x[0][1]]
[x[1][0], x[1][1]]
[x[2][0], x[2][1]]
]
A few domains: 0..3 0..2 0 1 0..3
Now, we can post a single constraint ElementMatrix, as follows:
satisfy(
x[i][j] == v
);
This means that the equation must hold, once we have assigned a value to all variables.
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 solution that has been found.
if solve() is SAT:
print(values(x))
print(value(i), value(j), value(v))
[
[0, 0]
[0, 0]
[0, 0]
]
0 0 0
Clearly, the value in the first cell of
One question that we may ask is: how many solutions (supports) does there exist for our constraint taken alone? Because at any time (when variables are assigned), only one variable of the array is constrained, it means that we have
if solve(sols=ALL) is SAT:
print("Last solution: ", values(x), value(i), value(j), value(v))
print("Number of solutions: ", n_solutions())
Last solution: [
[2, 3]
[1, 2]
[0, 1]
] 2 0 0
Number of solutions: 24576
Variant 2
We consider the variant 2 of the constraint ElementMatrix:
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 introduce a two-dimensional array
x = VarArray(size=[3, 2], dom=range(4))
i = Var(range(3))
j = Var(range(2))
Now, we can post a single constraint ElementMatrix, with the arbitrary value 1, as follows:
satisfy(
x[i][j] == 1
);
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), value(i), value(j))
[
[0, 0]
[0, 0]
[0, 1]
] 2 1
We should obtain 4 times less solutions than with the previous illustration (since the value is fixed), i.e.,
if solve(sols=ALL) is SAT:
print("Last solution: ", values(x), value(i), value(j))
print("Number of solutions: ", n_solutions())
Last solution: [
[2, 2]
[0, 0]
[1, 3]
] 2 0
Number of solutions: 6144
Variant 3
We consider the variant 3 of the constraint ElementMatrix:
Although this variant can be reformulated as a ternary extensional constraint, it is often used when modeling.
First of all, we need to remove everything that has been introduced so far.
clear() # to clear previously posted variables and constraints
We introduce a two-dimensional array
x = [
[2, 1],
[0, 1],
[3, 2]
]
i = Var(range(3))
j = Var(range(2))
v = Var(range(4))
One may imagine to simply post the constraint ElementMatrix, as follows:
satisfy(
x[i][j] == v
);
However, this is invalid (an error occurs) because it is not possible to use a special object (here, an object Var) as an index of a list of integers in Python. We need to transform the list of integers into a more specific list with the function cp_array(). So we write:
x = cp_array(x)
Now, we can safely write:
satisfy(
x[i][j] == v
);
We can call the function solve().
if solve() is SAT:
print(value(i), value(j), value(v))
0 0 2
It works! The good news is that when the data is loaded from a file (which is the usual case), all lists of integers have this specific type of list (returned by cp_array()), and so, it is very rare to need to call this function explicitly.
If ever we want to count the number of solutions, we can proceed as follows. Note how the named parameter sol of values() is used to indicate the index of a solution.
if solve(sols=ALL) is SAT:
for k in range(n_solutions()):
print(f"Solution {k+1}: ({value(i, sol=k)},{value(j, sol=k)},{value(v, sol=k)}) ")
Solution 1: (0,0,2)
Solution 2: (0,1,1)
Solution 3: (1,1,1)
Solution 4: (1,0,0)
Solution 5: (2,0,3)
Solution 6: (2,1,2)
Although this is not the most efficient way of doing that, an alternative is to iteratively add a constraint that forbids the last found solution and to call solve(). This way, after each solution, a new instance is generated and the solver is loaded (in the future, we plan to be able to let the solver alive). Hence, we can enumerate all solutions (supports) of the constraint as follows:
print("Supports are:")
while solve() is SAT:
print(f" ({value(i)},{value(j)},{value(v)})")
satisfy(
cp_array(i,j,v) != (value(i),value(j),value(v))
)
Supports are:
(0,0,2)
(0,1,1)
(1,0,0)
(2,0,3)
(1,1,1)
(2,1,2)
A first remark is that once the six supports of the constraint have been computed, one can post a ternary constraint Extension instead of a constraint ElementMatrix, as follows:
satisfy(
(i,j,v) in {(0,0,2),(0,1,1),(1,0,0),(1,1,1),(2,0,3),(2,1,2)}
);
A second remark is that we have used again the function cp_array(), this time to build a specific list of variables. If we do not call it, and simply write