Link Search Menu Expand Document
PyCSP3
Documentation Data GitHub XCSP3 About
download ipynb

Constraint Increasing

The constraint Increasing ensures that the values assigned to the variables of a specified list are in increasing order.

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

Case 1: Increasing on Variables

We consider the case where we have just a list of variables. If $r$ is the size of a list $x$ of variables, we have:

$x[i] \leq x[i+1], \forall i \in 0..r-1$

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 4 variables, each variable having {0,1,2,3} as domain.

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

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]]
Domain of any variable:  0..3

We simply post a single constraint Increasing on $x$ imposing that assigned values must be in increasing order.

satisfy(
    Increasing(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 to a specified list of variables.

if solve() is SAT:
    print("Values of x: ", values(x))
Values of x:  [0, 0, 0, 0]

We can enumerate the 8 first solutions as follows:

if solve(sols=8) is SAT:
    for i in range(n_solutions()):
        print(f"Solution {i+1}: {values(x, sol=i)}")
Solution 1: [0, 0, 0, 0]
Solution 2: [0, 0, 0, 1]
Solution 3: [0, 0, 0, 2]
Solution 4: [0, 0, 0, 3]
Solution 5: [0, 0, 1, 3]
Solution 6: [0, 0, 2, 3]
Solution 7: [0, 0, 3, 3]
Solution 8: [0, 0, 1, 1]

Strict Increasing

We now see how to impose a strict ordering.

To start, we remove the last posted constraint by calling the function unpost().

unpost()

We control that there are no more constraints.

print(posted())
[]

We post a single constraint Increasing with a strict ordering imposed on $x$.

satisfy(
    Increasing(x, strict=True)
);

We call the solver.

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

Case 2: Increasing with Lengths

Now, we consider the case where some lengths (durations) are associated with the variables of the list (except for the last one). If $r$ is the size of a list $x$ of variables, and $d$ a list of $r-1$ integers, we have:

$x[i] + d[i] \leq x[i+1], \forall i \in 0..r-1$

To start, we remove the last posted constraint by calling the function unpost().

unpost()

We post a single constraint Increasing with some arbitrary lengths associated with the three first variables

satisfy(
    Increasing(x, lengths=[1,0,1])
);

We call the solver.

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

We can enumerate all solutions:

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, 1, 2]
Solution 2: [0, 1, 1, 3]
Solution 3: [0, 1, 2, 3]
Solution 4: [0, 2, 2, 3]
Solution 5: [1, 2, 2, 3]