Constraint Circuit
The constraint Circuit ensures that the values taken by the variables of a specified list $x$ forms a circuit, with the assumption that each pair $(i,x[i])$ represents an arc. It is also possible to indicates that the circuit must be of a given size (greater than or equal to $2$).
The context is when problems involve graphs that are defined with integer variables (encoding called ``successors variables’’). Graph-based constraints, like Circuit, involve then a main list of variables $x$. The assumption is that each pair $(i,x[i])$ represents an arc (or edge) of the graph to be built; if $x[i]=j$, then it means that the successor of node $i$ is node $j$. Note that a loop, or self-loop, corresponds to a variable $x[i]$ such that $x[i]=i$.
Below, we give several illustrations corresponding to representative use cases of the constraint Circuit.
Case 1: Circuit of Any Size
We start with a case of Circuit without any form of restriction about the size. However, in order to be relevant, note that a circuit cannot be of size 0 (and so, its size is at least 2).
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 6 variables, each one with {0,1,2,3,4,5} as domain.
x = VarArray(size=6, dom=range(6))
We can display (the structure of) the array as well as the domain of the first variable.
print("Array of variable x: ", x)
print("Domain of any variable: ", x[0].dom)
Array of variable x: [x[0], x[1], x[2], x[3], x[4], x[5]]
Domain of any variable: 0..5
We simply post a single constraint Circuit on the variables of $x$:
satisfy(
Circuit(x)
);
By calling the function solve(), we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also print 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("Solution: ", values(x))
Solution: [0, 1, 2, 3, 5, 4]
One can see (actually, the output may depend on the used solver) that some loops are present. At the extreme case, the circuit is only of size 2.
To avoid loops, it is possible to post unary constraints:
satisfy(
x[i] != i for i in range(6)
);
Interestingly, we can display the internal representation of the posted constraints; although a little bit technical, we can see that the information is correctly recorded (note that ‘ne’ stands for ‘not equal’).
print(posted())
circuit(list:x[])
intension(function:ne(x[0],0))
intension(function:ne(x[1],1))
intension(function:ne(x[2],2))
intension(function:ne(x[3],3))
intension(function:ne(x[4],4))
intension(function:ne(x[5],5))
The number of circuits without any loop is $5! =120$. One can enumerate the 15 first solutions as follows:
if solve(sols=15) is SAT:
for i in range(n_solutions()):
print(f"Solution {i+1}: {values(x, sol=i)}")
Solution 1: [1, 2, 3, 4, 5, 0]
Solution 2: [1, 2, 3, 5, 0, 4]
Solution 3: [1, 2, 5, 4, 0, 3]
Solution 4: [1, 2, 4, 0, 5, 3]
Solution 5: [1, 2, 5, 0, 3, 4]
Solution 6: [1, 2, 4, 5, 3, 0]
Solution 7: [1, 3, 4, 2, 5, 0]
Solution 8: [1, 3, 5, 4, 2, 0]
Solution 9: [1, 4, 5, 2, 3, 0]
Solution 10: [1, 4, 3, 5, 2, 0]
Solution 11: [1, 4, 3, 0, 5, 2]
Solution 12: [1, 5, 3, 4, 0, 2]
Solution 13: [1, 5, 3, 0, 2, 4]
Solution 14: [1, 5, 0, 4, 2, 3]
Solution 15: [1, 3, 0, 5, 2, 4]
Case 2: Circuit of Specified Size
We consider now a case of Circuit with a specified size.
To start, we remove the posted constraints by calling the function unpost() with the parameter ALL.
unpost(ALL)
We can check that there are no more constraints.
print(posted())
[]
We post a single constraint Circuit on $x$, with the restriction that the circuit must be of size 3:
satisfy(
Circuit(x, size=3)
);
We can run the solver.
if solve() is SAT:
print("Solution: ", values(x))
Solution: [0, 1, 2, 4, 5, 3]
On can compute that the number of solutions (supports) for this constraint is: ${6 \choose 3} \times 2 = 40$.
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, 4, 5, 3]
Solution 2: [0, 1, 2, 5, 3, 4]
Solution 3: [0, 1, 3, 4, 2, 5]
Solution 4: [0, 1, 4, 2, 3, 5]
Solution 5: [0, 1, 4, 3, 5, 2]
Solution 6: [0, 1, 5, 3, 2, 4]
Solution 7: [0, 1, 5, 2, 4, 3]
Solution 8: [0, 1, 3, 5, 4, 2]
Solution 9: [0, 2, 3, 1, 4, 5]
Solution 10: [0, 3, 1, 2, 4, 5]
Solution 11: [0, 3, 2, 4, 1, 5]
Solution 12: [0, 4, 2, 1, 3, 5]
Solution 13: [0, 3, 2, 5, 4, 1]
Solution 14: [0, 5, 2, 1, 4, 3]
Solution 15: [0, 5, 2, 3, 1, 4]
Solution 16: [0, 4, 2, 3, 5, 1]
Solution 17: [0, 4, 1, 3, 2, 5]
Solution 18: [0, 2, 4, 3, 1, 5]
Solution 19: [0, 2, 5, 3, 4, 1]
Solution 20: [0, 5, 1, 3, 4, 2]
Solution 21: [1, 2, 0, 3, 4, 5]
Solution 22: [1, 3, 2, 0, 4, 5]
Solution 23: [1, 4, 2, 3, 0, 5]
Solution 24: [1, 5, 2, 3, 4, 0]
Solution 25: [2, 0, 1, 3, 4, 5]
Solution 26: [2, 1, 3, 0, 4, 5]
Solution 27: [2, 1, 5, 3, 4, 0]
Solution 28: [3, 1, 0, 2, 4, 5]
Solution 29: [5, 1, 0, 3, 4, 2]
Solution 30: [5, 0, 2, 3, 4, 1]
Solution 31: [5, 1, 2, 0, 4, 3]
Solution 32: [3, 1, 2, 5, 4, 0]
Solution 33: [3, 0, 2, 1, 4, 5]
Solution 34: [4, 1, 2, 0, 3, 5]
Solution 35: [3, 1, 2, 4, 0, 5]
Solution 36: [4, 0, 2, 3, 1, 5]
Solution 37: [4, 1, 2, 3, 5, 0]
Solution 38: [5, 1, 2, 3, 0, 4]
Solution 39: [2, 1, 4, 3, 0, 5]
Solution 40: [4, 1, 0, 3, 2, 5]
Variable Size
One can record the size of the circuit in a variable.
To start, we remove the posted constraint by calling the function unpost():
unpost()
We introduce a variable $y$.
y = Var(range(7))
We post a single constraint Circuit on $x$, with the restriction that the circuit must be of size $y$:
satisfy(
Circuit(x, size=y)
);
We can run the solver.
if solve() is SAT:
print("Solution: ", values(x), value(y))
Solution: [0, 1, 2, 3, 5, 4] 2
We can enumerate the 10 first solutions.
if solve(sols=10) is SAT:
for i in range(n_solutions()):
print(f"Solution {i+1}: {values(x, sol=i)} {value(y, sol=i)}")
Solution 1: [0, 1, 2, 3, 5, 4] 2
Solution 2: [0, 1, 2, 4, 5, 3] 3
Solution 3: [0, 1, 2, 5, 3, 4] 3
Solution 4: [0, 1, 2, 5, 4, 3] 2
Solution 5: [0, 1, 2, 4, 3, 5] 2
Solution 6: [0, 1, 3, 4, 2, 5] 3
Solution 7: [0, 1, 3, 4, 5, 2] 4
Solution 8: [0, 1, 3, 5, 2, 4] 4
Solution 9: [0, 1, 4, 5, 3, 2] 4
Solution 10: [0, 1, 4, 2, 5, 3] 4