Constraint Sum
The constraint Sum is one of the most important constraint. This constraint involves variables (and possibly coefficients), and is subject to a numerical condition. For example, a sum of variables in a list must be equal to a constant. Note that a form of Sum, sometimes called subset-sum or Knapsack involves the operator $\mathtt{in}$, and ensures that the computed sum belongs to a specified interval.
Below, we give several illustrations corresponding to representative use cases of the constraint Sum.
Case 1: Simple Sum
A basic form of the constraint Sum simply involves a list $x$ of variables.
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 {1,2,3} as domain.
x = VarArray(size=5, dom=range(1, 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: 1..3
We simply post a single constraint Sum: the sum of the values assigned to the variables of $x$ must be equal to 10:
satisfy(
Sum(x) == 12
);
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: [1, 2, 3, 3, 3]
If ever we want to count the number of solutions, we can set the value ALL to the named parameter sols.
if solve(sols=ALL) is SAT:
print("Number of solutions: ", n_solutions())
Number of solutions: 30
Suppose now that we arbitrarily assign $x[0]$ to 1.
satisfy(
x[0] == 1
);
The number of solutions is drastically reduced. Note how the named parameter sol of values() is used to indicate the index of a solution.
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, 3, 3]
Solution 2: [1, 3, 3, 2, 3]
Solution 3: [1, 3, 2, 3, 3]
Solution 4: [1, 3, 3, 3, 2]
And one can logically think that additionally arbitrarily assigning $x[1]$ to 1 makes the problem instance unsatisfiable.
satisfy(
x[1] == 1
);
We can check that no more solution exists because the result is now UNSAT.
print("Result: ", solve())
Result: UNSAT
Case 2: Weighted Sum
It is rather frequent to have variables accompanied with coefficients when performing a sum (we say that we deal with a weighted sum).
First of all, we need to remove everything that has been introduced so far.
clear() # to clear previously posted variables and constraints
As earlier, we introduce an array $x$ of 5 variables, each one with {1,2,3} as domain.
x = VarArray(size=5, dom=range(1, 4))
and we put some arbitrary coefficients in a list.
c = [3, 2, 1, 4, 2]
We can post a weighted constraint Sum: the weighted sum of the values assigned to the variables of $x$ must be strictly greater than 28:
satisfy(
Sum(x[i] * c[i] for i in range(5)) > 28
);
We can display the internal representation of the posted constraint; although a little bit technical, we can see that the weighted sum has been recognized (note that ‘gt’ stands for ‘(strictly) greater than’).
print(posted())
sum(list:[x[0], x[1], x[2], x[3], x[4]], coeffs:[3, 2, 1, 4, 2], condition:(gt,28))
We enumerate the 15 first solutions as follows:
if solve(sols=15) is SAT:
for i in range(n_solutions()):
print(f"Solution {i+1}: {values(x, sol=i)}")
Solution 1: [1, 3, 2, 3, 3]
Solution 2: [1, 3, 3, 3, 3]
Solution 3: [2, 3, 3, 3, 3]
Solution 4: [2, 3, 3, 3, 1]
Solution 5: [2, 3, 3, 3, 2]
Solution 6: [2, 3, 1, 3, 2]
Solution 7: [2, 3, 2, 3, 2]
Solution 8: [2, 3, 2, 3, 3]
Solution 9: [2, 3, 1, 3, 3]
Solution 10: [2, 2, 1, 3, 3]
Solution 11: [2, 2, 2, 3, 3]
Solution 12: [2, 2, 3, 3, 3]
Solution 13: [2, 1, 3, 3, 3]
Solution 14: [2, 2, 3, 3, 2]
Solution 15: [3, 2, 3, 3, 2]
The curious reader can see the value 1 is never present in any solution fo the variable $x[3]$. Technically, this means that this value can be deleted by a filtering algorithm associated with the constraint Sum.
Weighted Sum by Dot Product
Now, we are going to post the same constraint, but this time by using a dot product notation.
We start by deleting the currently posted constraint by calling the function unpost() that discards the last call to satisfy().
unpost()
We control that there are no more constraints.
print(posted())
[]
We can use a dot notation to post the constraint:
satisfy(
x * c > 28
);
We check that everything is fine.
print(posted())
sum(list:[x[0], x[1], x[2], x[3], x[4]], coeffs:[3, 2, 1, 4, 2], condition:(gt,28))
We still have 44 solutions.
if solve(sols=ALL) is SAT:
print("Number of solutions: ", n_solutions())
Number of solutions: 44
Importantly, if we write $c * x$ instead of $x * c$, an error occurs. This is because it is not possible to use in this context the operator $*$ on lists of integers in Python. We need to transform the list of integers into a more specific list with the function cp_array(). So it would be correct to write:
satisfy(
cp_array(c) * x > 28
);
However, most of the times, we directy use arrays (or sub-arrays) coming from the data of the model, loaded from a file, and they have the right type of list, and so, it is very rare to need to call cp_array() explicitly.
Case 3: Sum of Expressions
Sometimes, sums are built from general expressions. We give an illustration below.
First of all, we need to remove everything that has been introduced so far.
clear()
Then, we introduce an array $x$ of 4 variables, each one with {0,1,2,3} as domain.
x = VarArray(size=4, dom=range(4))
Although there exist other ways of expressing this, let us suppose that we want to guarantee that the number of variables in $x$ with a value greater than or equal to 1 is at least 3. We can write:
satisfy(
Sum(x[i] >= 2 for i in range(4)) >= 3
);
We can enumerate the first 10 solutions satisfying that constraint:
if solve(sols=10) is SAT:
for i in range(n_solutions()):
print(f"Solution {i+1}: {values(x, sol=i)}")
Solution 1: [0, 2, 2, 2]
Solution 2: [0, 2, 2, 3]
Solution 3: [0, 2, 3, 3]
Solution 4: [0, 2, 3, 2]
Solution 5: [0, 3, 3, 2]
Solution 6: [0, 3, 3, 3]
Solution 7: [0, 3, 2, 3]
Solution 8: [0, 3, 2, 2]
Solution 9: [1, 3, 2, 2]
Solution 10: [1, 3, 2, 3]