Constraint Extension

A constraint Extension is often referred to as a table constraint. It is defined by enumerating the tuples of values that are allowed (tuples are called supports) or forbidden (tuples are called conflicts) for a sequence of variables.

A positive table constraint is then defined by a scope (a sequence or tuple of variables) $\mathtt{\langle scope \rangle}$ and a table (a set of tuples of values) $\mathtt{\langle table \rangle}$ as follows:

$\mathtt{\langle scope \rangle\; \in\; \langle table \rangle}$

When the table constraint is negative (i.e., enumerates forbidden tuples), we have:

$\mathtt{\langle scope \rangle\; \notin\; \langle table \rangle}$

In PyCSP$^3$, we can directly write table constraints in mathematical forms, by using tuples, sets and the operators ‘in’ and ‘not in’. The scope is given by a tuple of variables on the left of the constraining expression and the table is given by a set of tuples of values on the right of the constraining expression. Although not recommended (except for huge tables), it is possible to write scopes and tables under the form of lists.

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

Case 1: Unary Tables

The first case is when the constraint is unary, meaning that only one variable is involved (in the scope of the constraint). We then have to indicate a list of values that are supported (or forbidden) by the variable.

To see how this constraint works, we need first to import the library PyCSP$^3$:

from pycsp3 import *


For our illustration, we introduce a stand-alone variable $x$ whose domain is $0..9$.

x = Var(range(10))


We simply post a single unary (positive) constraint Extension: $x$ must take a value among {1,3,5,7}.

satisfy(
x in {1,3,5,7}
);


Interestingly, we can display the internal representation of the posted constraints; we can see that the information is correctly recorded.

print(posted())

extension(list:[x], supports:1 3 5 7)


Without any surprise, the solutions for this constraint correspond to the specified supports.

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

Solution 1: 1
Solution 2: 3
Solution 3: 5
Solution 4: 7


Remark. Of course, we could have avoided the unary constraint by specifying a more precise domain. However, in some models, for clarity reasons, it may worthwhile to proceed with unary constraints.

To test the negative unary form of the constraint, we remove the one that has just been posted by calling the function unpost().

unpost()


We control that there are no more constraints.

print(posted())

[]


We now post a single unary (negative) constraint Extension: $x$ must not take a value among {1,3,5,7}.

satisfy(
x not in {1,3,5,7}
);


We print its internal representation.

print(posted())

extension(list:[x], conflicts:1 3 5 7)


And, once again, without any surprise, the solutions for this constraint correspond to the values that are not conflicts.

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

Solution 1: 0
Solution 2: 2
Solution 3: 4
Solution 4: 6
Solution 5: 8
Solution 6: 9


Case 2: Ordinary Tables

The second case is when the arity of the constraint is at least 2, meaning that at least two variables are involved (in the scope of the constraint). We then have to indicate a list of tuples that are supported (or forbidden) by the variables. We consider here ordinary tuples that do not contain any special symbol or structure.

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 an array $x$ of 4 variables, each one with {1,2,3} as domain.

x = VarArray(size=4, dom={1,2,3})


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:  1 2 3


We simply post a quaternary (positive) constraint Extension.

satisfy(
x in {(1,2,3,2), (2,1,1,2), (2,3,2,1), (3,1,2,3)}
);


We print its internal representation.

print(posted())

extension(list:[x[0], x[1], x[2], x[3]], supports:(1,2,3,2)(2,1,1,2)(2,3,2,1)(3,1,2,3))


The solutions for this constraint correspond to the specified supports.

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

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


To test the negative unary form of the constraint, we remove the one that has just been posted by calling the function unpost().

unpost()


We now post a quaternary (negative) constraint Extension. To show how scopes can be built from individual variables, we change the order of variables in the scope and write:

satisfy(
(x[3],x[1],x[0],x[2]) not in {(1,2,3,2), (2,1,1,2), (2,3,2,1), (3,1,2,3)}
);


We display its internal representation.

print(posted())

extension(list:[x[3], x[1], x[0], x[2]], conflicts:(1,2,3,2)(2,1,1,2)(2,3,2,1)(3,1,2,3))


We can anticipate thta the number of solutions is $3^4 - 4= 77$. We check it as follows:

if solve(sols=ALL) is SAT:
print("Number of solutions: ", n_solutions())

Number of solutions:  77


Case 3: Starred Tables

The third case is about starred table, which are tables containing the special symbol *, denoted by the constant ANY in PySCP$^3$. When the symbol * is present in a tuple, called starred or short tuple, it means that any value from the domain of the corresponding variable can be present at its position.

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

unpost()


We now post a ternary (positive) constraint Extension, with a table involving some starred tuples.

satisfy(
(x[0],x[1],x[2]) in {(1,ANY,2), (2,1,ANY), (3,1,3)}
);


We display its internal representation.

print(posted())

extension(list:[x[0], x[1], x[2]], supports:(1,*,2)(2,1,*)(3,1,3))


To be convinced about the semantics of ANY ($*$), we can enumerate the full set of solutions for this constraint.

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

Solution 1: [1, 1, 2]
Solution 2: [1, 2, 2]
Solution 3: [1, 3, 2]
Solution 4: [2, 1, 2]
Solution 5: [2, 1, 1]
Solution 6: [2, 1, 3]
Solution 7: [3, 1, 3]


Case 4: Hybrid Tables

The fourth case is about the introduction of auxiliary functions or structures to build tables. Currently, this is for simplifying the task of building ordinary tuples. However, in the next version of PyCSP$^3$, we shall offer the possibility of building hybrid/smart tables (see The Smart Table Constraint).

More specifically, when we build tables, we can use a compressed expression at any place inside a tuple by using one of the following structures or functions:

• (v1,v2,…, vk) corresponds to any specified value in this sub-tuple
• complement(v1,v2,…,vk) corresponds to any value not specified in this sub-tuple
• ne(v) corresponds to any value ‘not equal’ to v
• lt(v) corresponds to any value strictly ‘less than’ v
• le(v) corresponds to any value ‘less than or equal to’ v
• gt(v) corresponds to any value strictly ‘greater than’ v
• ge(v) corresponds to any value ‘greater than or equal to’ v

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

unpost()


We post a single constraint Extension by using a table which is specified from some compressed expressions.

satisfy(
x in {(ne(1),2,lt(3),2), (ge(2),1,(1,2),complement(1,2))}
);


The first compressed tuple encompasses any ordinary tuple such that the first value is not 1, the second value is 2, the third value is strictly less than 3, and the fourth value is 2. The second compressed tuple encompasses any ordinary tuple such that the first value is greater than or eqaul to 2, the second value is 1, the third value is either 1 or 2, and the fourth value is neither 1 nor 2.

By displaying the internal representation of the constraint, we can observe the set of ordinary tuples that are encompassed by one of the two compressed ones.

print(posted())

extension(list:[x[0], x[1], x[2], x[3]], supports:(2,1,1,3)(2,1,2,3)(2,2,1,2)(2,2,2,2)(3,1,1,3)(3,1,2,3)(3,2,1,2)(3,2,2,2))