Constraint Channel
The constraint Channel is used to make some connections between variables (from correspondances between their assigned values). Actually, there are three variants of the constraint Channel.
Variant 1
We consider the variant 1 of the constraint Channel. It is defined on a single list $x$ of variables, and ensures that if the ith variable of the list is assigned the value $j$, then the jth variable of the same list must be assigned the value $i$. We have:
$x_i = j \Rightarrow x_j=i$
To see how this constraint works, we need first to import the library PyCSP$^3$:
from pycsp3 import *
For our illustration, we introduce an array $x$ of $5$ variables.
x = VarArray(size=5, dom=range(5))
Now, we can post a single constraint Channel, as follows:
satisfy(
Channel(x)
);
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; we can call the function values() that collects the values assigned (in the last found solution) to a specified list of variables.
if solve() is SAT:
print(values(x))
[0, 1, 2, 3, 4]
By the way, how many solutions (supports) does there exist for our constraint taken alone? The reader can try to prove that it is 26. We can check this by calling solve() with the named parameter sols. Note how the named parameter sol of values() is used to indicate the index of a solution.
if solve(sols=ALL) is SAT:
for i in range(n_solutions()):
print(f"Solution {i+1}: {values(x, sol=i)}")
Solution 1: [0, 1, 2, 3, 4]
Solution 2: [0, 1, 2, 4, 3]
Solution 3: [0, 1, 4, 3, 2]
Solution 4: [0, 1, 3, 2, 4]
Solution 5: [0, 4, 3, 2, 1]
Solution 6: [0, 4, 2, 3, 1]
Solution 7: [0, 3, 2, 1, 4]
Solution 8: [0, 3, 4, 1, 2]
Solution 9: [0, 2, 1, 4, 3]
Solution 10: [0, 2, 1, 3, 4]
Solution 11: [1, 0, 2, 3, 4]
Solution 12: [1, 0, 4, 3, 2]
Solution 13: [2, 1, 0, 3, 4]
Solution 14: [4, 1, 2, 3, 0]
Solution 15: [2, 4, 0, 3, 1]
Solution 16: [4, 2, 1, 3, 0]
Solution 17: [3, 2, 1, 0, 4]
Solution 18: [1, 0, 3, 2, 4]
Solution 19: [3, 1, 2, 0, 4]
Solution 20: [2, 3, 0, 1, 4]
Solution 21: [4, 3, 2, 1, 0]
Solution 22: [3, 1, 4, 0, 2]
Solution 23: [3, 4, 2, 0, 1]
Solution 24: [1, 0, 2, 4, 3]
Solution 25: [2, 1, 0, 4, 3]
Solution 26: [4, 1, 3, 2, 0]
Variant 2
We consider the variant 2 of the constraint Channel, sometimes called Inverse or Assignment in the literature: it is defined from two separate lists $x$ and $y$ (of the same size) of variables. It ensures that the value assigned to the ith variable of the first list gives the position of the variable of the second list that is assigned to $i$, and vice versa. We have:
$x_i = j \Leftrightarrow y_j = i$.
First of all, we need to remove everything that has been introduced so far.
clear() # to clear previously posted variables and constraints
For our illustration, we introduce two arrays $x$ and $y$ of $4$ variables.
x = VarArray(size=4, dom=range(4))
y = VarArray(size=4, dom=range(4))
Now, we can post a single constraint Channel as follows:
satisfy(
Channel(x, y)
);
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), values(y))
[0, 1, 2, 3] [0, 1, 2, 3]
We can enumerate all solutions as follows:
if solve(sols=ALL) is SAT:
for i in range(n_solutions()):
print(f"Solution {i+1}: {values(x, sol=i)}, {values(y, sol=i)}")
Solution 1: [0, 1, 2, 3], [0, 1, 2, 3]
Solution 2: [0, 1, 3, 2], [0, 1, 3, 2]
Solution 3: [0, 3, 1, 2], [0, 2, 3, 1]
Solution 4: [0, 3, 2, 1], [0, 3, 2, 1]
Solution 5: [0, 2, 3, 1], [0, 3, 1, 2]
Solution 6: [0, 2, 1, 3], [0, 2, 1, 3]
Solution 7: [1, 2, 0, 3], [2, 0, 1, 3]
Solution 8: [1, 0, 2, 3], [1, 0, 2, 3]
Solution 9: [2, 1, 0, 3], [2, 1, 0, 3]
Solution 10: [2, 0, 1, 3], [1, 2, 0, 3]
Solution 11: [3, 0, 1, 2], [1, 2, 3, 0]
Solution 12: [3, 0, 2, 1], [1, 3, 2, 0]
Solution 13: [2, 0, 3, 1], [1, 3, 0, 2]
Solution 14: [1, 0, 3, 2], [1, 0, 3, 2]
Solution 15: [1, 2, 3, 0], [3, 0, 1, 2]
Solution 16: [2, 1, 3, 0], [3, 1, 0, 2]
Solution 17: [3, 1, 0, 2], [2, 1, 3, 0]
Solution 18: [3, 1, 2, 0], [3, 1, 2, 0]
Solution 19: [1, 3, 2, 0], [3, 0, 2, 1]
Solution 20: [2, 3, 1, 0], [3, 2, 0, 1]
Solution 21: [3, 2, 1, 0], [3, 2, 1, 0]
Solution 22: [1, 3, 0, 2], [2, 0, 3, 1]
Solution 23: [2, 3, 0, 1], [2, 3, 0, 1]
Solution 24: [3, 2, 0, 1], [2, 3, 1, 0]
It is also possible to use this form of Channel, with two lists of different sizes. The constraint then imposes restrictions on all variables of the first list, but not on all variables of the second list. The syntax is the same, but the semantics is the following (note that the equivalence has been replaced by an implication):
$x_i = j \Rightarrow y_j = i$
Variant 3
We consider the variant 3 of the constraint Channel: it is obtained by considering a list $x$ of 0/1 variables to be channeled with an integer variable $v$. This third form of constraint Channel ensures that the only variable of the list that is assigned to 1 is at an index (position) that corresponds to the value assigned to the stand-alone integer variable. We have:
$x_i = 1 \Leftrightarrow v = i$
First of all, we need to remove everything that has been introduced so far.
clear() # to clear previously posted variables and constraints
We introduce an array $x$ of 0/1 variables, and a stand-alone variable $v$ that will play the role of value.
x = VarArray(size=6, dom={0,1})
v = Var(range(6))
Now, we can post the constraint Channel:
satisfy(
Channel(x,v)
);
We can call the function solve().
if solve() is SAT:
print(values(x), value(v))
[0, 0, 0, 0, 0, 1] 5
We can enumerate all solutions:
if solve(sols=ALL) is SAT:
for k in range(n_solutions()):
print(f"Solution {k+1}: {values(x, sol=k)} {value(v, sol=k)} ")
Solution 1: [0, 0, 0, 0, 0, 1] 5
Solution 2: [0, 0, 0, 0, 1, 0] 4
Solution 3: [0, 0, 0, 1, 0, 0] 3
Solution 4: [0, 0, 1, 0, 0, 0] 2
Solution 5: [0, 1, 0, 0, 0, 0] 1
Solution 6: [1, 0, 0, 0, 0, 0] 0