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

Constraint Element

The constraint Element ensures that the element of a specified list $x$ at a specified index $i$ has a specified value $v$. The semantics is $x[i] = v$. It is important to note that i is necessarily an integer variable of a constraint model (i.e., a variable of a CSP or COP model).

In Python, to post a constraint Element, we use the facilities offered by the language, meaning that we can write expressions involving relational and indexing ([]) operators.

Variant 1

We consider the variant 1 of the constraint Element: $x$ is a list of integer variables, $i$ is an integer variable and $v$ is an integer variable. Important: we refer here to variables of the constraint model.

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

from pycsp3 import *

We introduce an array $x$ of $4$ variables, and two stand-alone variables $i$ and $v$ that will play the role of index and value.

x = VarArray(size=4, dom=range(3))
i = Var(range(4))
v = Var(range(3))

We can display the structure of the array, as well as a few domains.

print("Array x: ", x)
print("A few domains: ", x[0].dom, " ", i.dom, " ", v.dom)
Array x:  [x[0], x[1], x[2], x[3]]
A few domains:  0..2   0..3   0..2

Now, we can post a single constraint Element, as follows:

satisfy(
    x[i] == v
);

This means that the equation must hold, once we have assigned a value to all variables.

By calling the function solve(), we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also display the values assigned to the variables in the solution that has been found.

if solve() is SAT:
    print(values(x), value(i), value(v))
[0, 0, 0, 0] 0 0

Clearly, the value in the first cell of $x$ (cell at index 0) is equal to the value of $v$.

One question that we may ask is: how many solutions (supports) does there exist for our constraint taken alone? Because at any time (when variables are assigned), only one variable of the array is constrained, it means that we have $27 \times 3 \times 4$ solutions ($3 \times 3 \times 3$ possibilities for “non concerned” variables of $x$, $3$ possible values, and $4$ possibles indexes). We can check this by calling solve() with the named parameter sols.

if solve(sols=ALL) is SAT:
    print("Last solution: ", values(x), value(i), value(v))
    print("Number of solutions: ", n_solutions())
Last solution:  [1, 0, 0, 0] 2 0
Number of solutions:  324

Variant 2

We consider the variant 2 of the constraint Element: $x$ is a list of integer variables, $i$ is an integer variable and $v$ is an integer (not a variable). Important: we refer here to variables of the constraint model.

First of all, we need to remove everything that has been introduced so far by calling the function clear().

clear()  # to clear previously posted variables and constraints

We introduce an array $x$ of $4$ variables, and one stand-alone variable $i$ that will play the role of index.

x = VarArray(size=4, dom=range(3))
i = Var(range(4))

Now, we can post a single constraint Element, with the arbitrary value 1, as follows:

satisfy(
    x[i] == 1
);

By calling the function solve(), we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also display the values assigned to the variables in the found solution.

if solve() is SAT:
    print(values(x), value(i))
[0, 0, 0, 1] 3

We should obtain 3 times less solutions than with the previous illustration (since the value is fixed), i.e., $27 \times 4$ solutions. We can check this by calling solve() with the named parameter sols.

if solve(sols=ALL) is SAT:
    print("Last solution: ", values(x), value(i))
    print("Number of solutions: ", n_solutions())
Last solution:  [1, 2, 0, 1] 3
Number of solutions:  108

Variant 3

We consider the variant 3 of the constraint Element: $x$ is a list of integers (not variables), $i$ is an integer variable and $v$ is an integer variable. Important: we refer here to variables of the constraint model.

Although this variant can be reformulated as a binary extensional constraint, it is often used when modeling.

First of all, we need to remove everything that has been introduced so far.

clear()  # to clear previously posted variables and constraints

We introduce an array $x$ of $4$ integers, and two stand-alone variables $i$ and $v$ that will play the role of index and value.

x = [2, 1, 0, 1] 
i = Var(range(4))
v = Var(range(3))

One may imagine to simply post the constraint Element, as follows:

satisfy(
    x[i] == v
);

However, this is invalid (an error occurs) because it is not possible to use a special object (here, an object Var) as an index of a list of integers in Python. We need to transform the list of integers into a more specific list with the function cp_array(). So we write:

x = cp_array(x)

Now, we can safely write:

satisfy(
    x[i] == v
);

We can call the function solve().

if solve() is SAT:
    print(value(i), value(v))
0 2

It works! The good news is that when the data is loaded from a file (which is the usual case), all lists of integers have this specific type of list (returned by cp_array()), and so, it is very rare to need to call this function explicitly.

If ever we want to count the number of solutions, we can proceed as follows. Note how the named parameter sol of values() is used to indicate the index of a solution.

if solve(sols=ALL) is SAT:
    for k in range(n_solutions()):
        print(f"Solution {k+1}: ({value(i, sol=k)},{value(v, sol=k)}) ")
Solution 1: (0,2) 
Solution 2: (2,0) 
Solution 3: (1,1) 
Solution 4: (3,1) 

Although this is not the most efficient way of doing that, an alternative is to iteratively add a constraint that forbids the last found solution and to call solve(). This way, after each solution, a new instance is generated and the solver is loaded (in the future, we plan to be able to let the solver alive). Hence, we can enumerate all solutions (supports) of the constraint as follows:

print("Supports are:")
while solve() is SAT:
    print(f"  ({value(i)},{value(v)})")
    satisfy(
        cp_array(i,v) != (value(i),value(v))
    )
Supports are:
  (0,2)
  (1,1)
  (2,0)
  (3,1)

A first remark is that once the four supports of the constraint have been computed (for a binary constraint, this is rather trivial), one can post a binary constraint Extension instead of a constraint Element, as follows:

satisfy(
    (i,v) in {(0,2),(1,1),(2,0),(3,1)}
);

A second remark is that we have used again the function cp_array(), this time to build a specific list of variables. If we do not call it, and simply write $(i,v)$ or $[i,v]$, an error will occur. However, most of the times, we directy use introduced arrays (or sub-arrays) of the model, after loading data from a file, and they have the right type of list, and so, it is very rare to need to call cp_array() explicitly.