PyCSP³

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 that 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 PyCSP$^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 advanced tables called hybrid (or 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} or (v1, v2, …, vk) corresponds to any value in the specified set or tuple
range(a, b) corresponds to any value in the specified range
complement(v1, v2, …, vk) corresponds to any unspecified value
complement(range(a, b)) corresponds to any value not present in the specified range
op(v) with op being a relational operator in {ne, lt, le, gt, ge} so that:
- 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
op(col(i)) with op being a relational operator in {eq, ne, lt, le, gt, ge} and col(i) denoting the ‘column’ of the tuple at index i, so that:
- eq(col(i)) corresponds to the value at index i in the tuple
- ne(col(i)) corresponds to any value ‘not equal’ to the value at index i
- lt(col(i)) corresponds to any value strictly ‘less than’ the value at index i
- le(col(i)) corresponds to any value ‘less than or equal to’ the value at index i
- gt(col(i)) corresponds to any value strictly ‘greater than’ the value at index i
- ge(col(i)) corresponds to any value ‘greater than or equal to’ the value at index i
op(col(i) + v), defined similarly as above, with v added to the value at index i
op(col(i) - v), defined similarly as above, with v subtracted to the value at index i
op(col(i) + col(j)), defined similarly as above, with the values at index i and j being added

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

unpost()

In order to see how hybrid tables can be generated, and represented in XCSP$^3$, we need to set the option keephybrid as follows:

from pycsp3.dashboard import options
options.keephybrid = True

The first table involves unary restrictions only (meaning that col() is not used at all): this is level 1 of hybridisation.

table1 = {
    (range(4, 7), gt(7), ANY),
    (lt(3), ANY, ge(6)),
    (9, ne(2), ANY),
    ((3, 8), ANY, (6, 8)),
    (7, complement(range(2, 8)), complement(1, 3, 5, 7, 9))
}

satisfy(
    (x[0],x[1],x[2]) in table1
);

print(posted())

extension[TYPE: hybrid-1](list:[x[0], x[1], x[2]], supports:(9,≠2,*)(≤2,*,≥6)(7,∁2..7,∁{1,3,5,7,9})(4..6,≥8,*)({3,8},*,{6,8}))

Because above the table is a set, we cannot use {} for specifying subtuples. This is possible when the table is a list as follows:

table2 = [
    (range(4, 7), gt(7), ANY),
    (lt(3), ANY, ge(6)),
    (9, ne(2), ANY),
    ({3, 8}, ANY, {6, 8}),
    (7, complement(range(2, 8)), complement(1, 3, 5, 7, 9))
]


satisfy(
    (x[0],x[1],x[2]) in table2
);

We can observe the two tables are equivalent (although hybrid tuples are not systematically listed in the same order).

print(posted())

extension[TYPE: hybrid-1](list:[x[0], x[1], x[2]], supports:(9,≠2,*)(≤2,*,≥6)(7,∁2..7,∁{1,3,5,7,9})(4..6,≥8,*)({3,8},*,{6,8}))
extension[TYPE: hybrid-1](list:[x[0], x[1], x[2]], supports:(4..6,≥8,*)(≤2,*,≥6)(9,≠2,*)({3,8},*,{6,8})(7,∁2..7,∁{1,3,5,7,9}))

We can also generate a table with binary (and/or ternary) restrictions: this is level 2 of hybridation. Note that we call col(), which becomes % followed by the specified index in XCSP$^3$.

table3 = {
     (1, eq(3), 2),
     (ANY, eq(col(0) - 2), 2),
     (1, eq(col(2)), ANY),
     (ANY, 1, gt(col(0) + 2)),
     (eq(col(1) + 6), ANY, lt(col(1) + 5)),
     (0, 0, eq(2 + col(0) + 5 + 5)),
     (ANY, ANY, eq(col(0) + col(1)))
}

satisfy(
    (x[0],x[1],x[2]) in table3
);

print(posted())

extension[TYPE: hybrid-1](list:[x[0], x[1], x[2]], supports:(9,≠2,*)(≤2,*,≥6)(7,∁2..7,∁{1,3,5,7,9})(4..6,≥8,*)({3,8},*,{6,8}))
extension[TYPE: hybrid-1](list:[x[0], x[1], x[2]], supports:(4..6,≥8,*)(≤2,*,≥6)(9,≠2,*)({3,8},*,{6,8})(7,∁2..7,∁{1,3,5,7,9}))
extension[TYPE: hybrid-2](list:[x[0], x[1], x[2]], supports:(c1+6,*,﹤c1+5)(1,=3,2)(0,0,c0+12)(*,c0-2,2)(*,1,﹥c0+2)(*,*,c0+c1)(1,c2,*))

Note that these sophisticated tables are not, for the moment, recognized by many solvers. Currently, ACE supports most of these hybrid forms.

Sometimes, it is possible to convert an hybrid tuple into an ordinary/starred table. We illustrate this now.

unpost(ALL)

table = {(ne(1),2,lt(3),2), (ge(2),1,(1,2),complement(1,2))}

satisfy(
    x in table
)

options.keephybrid = False

satisfy(
    x in table
)

print(posted())

extension[TYPE: hybrid-1](list:[x[0], x[1], x[2], x[3]], supports:(≥2,1,{1,2},∁{1,2})(≠1,2,≤2,2))
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))

The first hybrid 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 hybrid tuple encompasses any ordinary tuple such that the first value is greater than or equal 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 two posted constraints, we can observe the correspondance between the hybrid and ordinary tuples.

Constraint Extension

Case 1: Unary Tables

Case 2: Ordinary Tables

Case 3: Starred Tables

Case 4: Hybrid Tables

Related Models