Constraint LexIncreasing
The constraint Increasing can be naturally lifted to lists, by considering the so-called lexicographic order: it is then called LexIncreasing and ensures that the tuple formed by the values assigned to the variables of a first list is lexicographically less than (or equal to) the tuple formed by the values assigned to the variables of a second list.
Below, we give several illustrations corresponding to representative use cases of the constraint LexIncreasing.
Case 1: LexIncreasing on Two Lists
To see how this constraint works, we need first to import the library PyCSP$^3$:
from pycsp3 import *
For our illustration, we introduce two arrays $x$ and $y$ of 3 variables, each variable having {0,1} as domain.
x = VarArray(size=3, dom=range(2))
y = VarArray(size=3, dom=range(2))
We can display (the structure of) the arrays as well as the domain of a variable.
print("Array of variable x: ", x)
print("Array of variable y: ", y)
print("Domain of any variable: ", x[0].dom)
Array of variable x: [x[0], x[1], x[2]]
Array of variable y: [y[0], y[1], y[2]]
Domain of any variable: 0 1
We simply post a single constraint LexIncreasing that imposes $x \leq_{lex} y$:
satisfy(
LexIncreasing(x,y)
);
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))
print("Values of y: ", values(y))
Values of x: [0, 0, 0]
Values of y: [0, 0, 0]
Here, we obtain a rather trivial solution. To get all solutions when x is, for example equal to [0, 1, 0], we can write:
satisfy(
x == [0,1,0]
)
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, 0] [0, 1, 0]
Solution 2: [0, 1, 0] [0, 1, 1]
Solution 3: [0, 1, 0] [1, 1, 1]
Solution 4: [0, 1, 0] [1, 1, 0]
Solution 5: [0, 1, 0] [1, 0, 0]
Solution 6: [0, 1, 0] [1, 0, 1]
Strict LexIncreasing
We now see how to impose a strict ordering.
To start, we remove the posted constraints by calling the function unpost() with a parameter set to the constant ALL.
unpost(ALL)
We control that there are no more constraints.
print(posted())
[]
We post a single constraint LexIncreasing that imposes $x <_{lex} y$ (this is a strict ordering):
satisfy(
LexIncreasing(x, y, strict=True)
);
Interestingly, we can display the internal representation of the posted constraint; although a little bit technical, we can see that the information is correctly recorded (note that ‘lt’ stands for ‘strictly less than’).
print(posted())
lex(list:[[x[0], x[1], x[2]], [y[0], y[1], y[2]]], operator:lt)
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)} {values(y, sol=i)}")
Solution 1: [0, 0, 0] [0, 0, 1]
Solution 2: [0, 0, 0] [0, 1, 1]
Solution 3: [0, 0, 0] [0, 1, 0]
Solution 4: [0, 0, 0] [1, 1, 0]
Solution 5: [0, 0, 0] [1, 0, 0]
Solution 6: [0, 0, 0] [1, 0, 1]
Solution 7: [0, 0, 0] [1, 1, 1]
Solution 8: [0, 0, 1] [1, 1, 1]
Case 2: LexIncreasing on $k$ Lists
Actually, we can impose a lexicographic order on a sequence of $k$ lists with $k \ge 2$. We give an illustration for $k=3$.
We first remove all posted constraints.
unpost(ALL)
We introduce a third array $z$ of 3 variables.
z = VarArray(size=3, dom=range(2))
We post a single constraint LexIncreasing that imposes $x <{lex} y <{lex} z$:
satisfy(
LexIncreasing(x, y, z, strict=True)
);
We dsiplay its internal representation.
print(posted())
lex(list:[[x[0], x[1], x[2]], [y[0], y[1], y[2]], [z[0], z[1], z[2]]], operator:lt)
We enumerate the 8 first solutions:
if solve(sols=8) is SAT:
for i in range(n_solutions()):
print(f"Solution {i+1}: {values(x, sol=i)} {values(y, sol=i)} {values(z, sol=i)}")
Solution 1: [0, 0, 0] [0, 0, 1] [0, 1, 0]
Solution 2: [0, 0, 0] [0, 0, 1] [0, 1, 1]
Solution 3: [0, 0, 0] [0, 0, 1] [1, 1, 1]
Solution 4: [0, 0, 0] [0, 0, 1] [1, 1, 0]
Solution 5: [0, 0, 0] [0, 0, 1] [1, 0, 0]
Solution 6: [0, 0, 0] [0, 0, 1] [1, 0, 1]
Solution 7: [0, 0, 0] [0, 1, 1] [1, 0, 1]
Solution 8: [0, 0, 0] [0, 1, 0] [1, 0, 1]
Case 3: LexIncreasing on Matrices
We are now interested in the matrix variant of LexIncreasing. It means that we impose a lexicographic order on the sequence of rows and also on the sequence of columns of a two-dimensional array of variables.
We first clear (remove) variables and constraints.
clear()
Then, we introduce a two-dimensional array of variables $x$, each variable having {0,1} as domain.
x = VarArray(size=[3,3], dom={0,1})
We can display the structure of the array:
print("Array of variable x: ", x)
Array of variable x: [
[x[0][0], x[0][1], x[0][2]]
[x[1][0], x[1][1], x[1][2]]
[x[2][0], x[2][1], x[2][2]]
]
We post a single matrix constraint LexIncreasing on $x$ that imposes:
- $x[0] \leq_{lex} x[1] \leq_{lex} x[2]$
- $x[:,0] \leq_{lex} x[:,1] \leq_{lex} x[:,2]$
where $x[:j]$ denotes the jth column of $x$
satisfy(
LexIncreasing(x, matrix=True)
);
We enumerate the 3 first solutions:
if solve(sols=3) is SAT:
for i in range(n_solutions()):
print(f"Solution {i+1}: {values(x, sol=i)}")
Solution 1: [
[0, 0, 0]
[0, 0, 0]
[0, 0, 0]
]
Solution 2: [
[0, 0, 0]
[0, 0, 0]
[0, 0, 1]
]
Solution 3: [
[0, 0, 0]
[0, 0, 0]
[0, 1, 1]
]
We can also impose a strict ordering:
unpost()
satisfy(
LexIncreasing(x, matrix=True, strict=True)
);
if solve(sols=3) is SAT:
for i in range(n_solutions()):
print(f"Solution {i+1}: {values(x, sol=i)}")
Solution 1: [
[0, 0, 0]
[0, 0, 1]
[0, 1, 0]
]
Solution 2: [
[0, 0, 0]
[0, 0, 1]
[0, 1, 1]
]
Solution 3: [
[0, 0, 0]
[0, 1, 1]
[1, 0, 1]
]