PyCSP³

Posting constraints

When constraints must be imposed on variables, we say that these constraints must be satisfied. To impose (post) them, we call the PyCSP$^3$ function satisfy(). Several constraints can be posted together, by using comprehension lists and/or several parameters (with commas used as a separator between parameters).

To illustrate how it works, we need first to import the library PyCSP$^3$:

from pycsp3 import *

For our illustration, let us declare an array x of 4 variables, each one with {0,1,2,3} as domain.

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

Let us suppose that we want that:

the distance between any two successive values (assigned to variables) of $x$ is greater than or equal to 2
all values of $x$ are different.

We can decide to post each constraint independently. This gives:

for i in range(3):
    satisfy(abs(x[i] - x[i+1]) >= 2)
    
satisfy(
    AllDifferent(x)
);

We can display the internal representation of the 4 posted constraints; this way, although a little bit technical, we can see that the constraints are correctly built. Note that ‘ge’ stands for ‘greater than or equal to’.

print(posted())

intension(function:ge(dist(x[0],x[1]),2))
intension(function:ge(dist(x[1],x[2]),2))
intension(function:ge(dist(x[2],x[3]),2))
allDifferent(list:[x[0], x[1], x[2], x[3]])

By calling the function solve(), we can check that the problem is satisfiable (SAT). Here, to enumerate all solutions, we use the constant ALL as value of the named parameter sols. Note also that we print the found solutions by calling the function values() that collects the values assigned to a specified list of variables, for a solution whose index is given by the value of the named parameter sol.

if solve(sols=ALL) is SAT:
    for i in range(n_solutions()):
        print(f" Solution {i}: {values(x, sol=i)}")

 Solution 0: [1, 3, 0, 2]
 Solution 1: [2, 0, 3, 1]

We now discard all posted constraints:

unpost(ALL)

We can check that there are no more constraints:

print(posted())

[]

We show now that we can use a comprehension list (actually, a generator) to post the three binary constraints. This gives:

satisfy(
    abs(x[i] - x[i+1]) >= 2 for i in range(3)
)

satisfy(
    AllDifferent(x)
);

We check that the result is the same in term of posted constraints:

print(posted())

intension(function:ge(dist(x[0],x[1]),2))
intension(function:ge(dist(x[1],x[2]),2))
intension(function:ge(dist(x[2],x[3]),2))
allDifferent(list:[x[0], x[1], x[2], x[3]])

And of course, we obtain the two same solutions:

if solve(sols=ALL) is SAT:
    for i in range(n_solutions()):
        print(f" Solution {i}: {values(x, sol=i)}")

 Solution 0: [1, 3, 0, 2]
 Solution 1: [2, 0, 3, 1]

Again, we discard all posted constraints.

unpost(ALL)

We show now that we can post all constraints with a single call to satisfy():

satisfy(
    [abs(x[i] - x[i+1]) >= 2 for i in range(3)],
    
    AllDifferent(x)
);

We check that the result is the same in term of posted constraints:

print(posted())

intension(function:ge(dist(x[0],x[1]),2))
intension(function:ge(dist(x[1],x[2]),2))
intension(function:ge(dist(x[2],x[3]),2))
allDifferent(list:[x[0], x[1], x[2], x[3]])

And we have the two same solutions:

if solve(sols=ALL) is SAT:
    for i in range(n_solutions()):
        print(f" Solution {i}: {values(x, sol=i)}")

 Solution 0: [1, 3, 0, 2]
 Solution 1: [2, 0, 3, 1]