Constraint NValues

The constraint NValues ensures that the number of distinct values taken by the variables of a specified list $x$ respects a numerical condition. For example, the number of distinct values in $x$ must be less than or equal to a constant.

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

Case 1: Number of Distinct Values as a Constant

The first case is when the number of distinct values taken by a list of variables is constrained by a constant (limit).

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 5 variables, each one with {0,1,2,3} as domain.

x = VarArray(size=5, 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], x[4]]
Domain of any variable:  0..3

We simply post a single constraint NValues: the number of distinct values assigned to the variables of $x$ must be less than or equal to 2:

satisfy(
    NValues(x) <= 2
);

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 (in the last found solution) to a specified list of variables.

if solve() is SAT:
    print("Solution: ", values(x))

Solution:  [0, 0, 0, 0, 0]

On can check that the number of solutions (supports) for our constraint is $4 + {4 \choose 2} \times 2 \times ({5 \choose 1} + {5 \choose 2})$.

if solve(sols=ALL) is SAT:
    print("Last found solution: ", values(x))
    print("Number of solutions: ", n_solutions())

Last found solution:  [2, 0, 2, 2, 0]
Number of solutions:  184

Case 2: Number of Distinct Values as a Variable

The second case is when the number of distinct values taken by a list of variables is constrained by a variable (limit).

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 introduce a stand-alone variable $y$ that will be useful to “compute” the number of distinct values in $x$.

y = Var(range(1, 6))

We post a single constraint NValues:

satisfy(
    NValues(x) == y
);

And we run the solver to find a first solution.

if solve() is SAT:
    print("Solution: ", values(x), value(y))

Solution:  [0, 0, 0, 0, 0] 1

One can prove rather easily that the number of solutions is $4^5$. We can display the last ten solutions.

if solve(sols=ALL) is SAT:
    print("Number of solutions: ", n_solutions())
    for i in range(1, 10):
        print(f"Solution {n_solutions()-i+1}: x={values(x, sol=-i)}  y={value(y,sol=-i)}")

Number of solutions:  1024
Solution 1024: x=[3, 0, 1, 3, 2]  y=4
Solution 1023: x=[2, 0, 1, 3, 2]  y=4
Solution 1022: x=[2, 0, 3, 3, 1]  y=4
Solution 1021: x=[2, 0, 1, 3, 1]  y=4
Solution 1020: x=[2, 0, 0, 3, 1]  y=4
Solution 1019: x=[2, 3, 0, 3, 1]  y=4
Solution 1018: x=[2, 3, 1, 3, 0]  y=4
Solution 1017: x=[2, 0, 1, 3, 0]  y=4
Solution 1016: x=[2, 1, 1, 3, 0]  y=4

Case 3: Number of Distinct Expressions

The third case is when the number of distinct values taken by a list of expressions is constrained by a constant.

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 5 variables, each one with {0,1,2,3} as domain.

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

We post a single constraint NValues on expressions:

satisfy(
    NValues(x[0]+x[1], x[1]+x[2], x[2]+x[3], x[3]+x[4]) > 2
);

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 ‘gt’ stands for ‘(strictly) greater than’).

print(posted())

nValues(list:[add(x[0],x[1]), add(x[1],x[2]), add(x[2],x[3]), add(x[3],x[4])], condition:(gt,2))

We can run the solver

if solve() is SAT:
    print("Solution: ", values(x), value(y))

Solution:  [0, 0, 0, 1, 1] 4

Related Models

• BoardColoration