Problem Magic Sequence

A magic sequence of order $n$ is a sequence of integers $x_0,\dots,…x_{n-1}$ between 0 and $n-1$, such that each value $i \in 0..n-1$ occurs exactly $x_i$ times in the sequence. For example,

6 2 1 0 0 0 1 0 0 0

is a magic sequence of order 10 since 0 occurs 6 times, 1 occurs twice, $\dots$ and 9 occurs 0 times.

To build a CSP (Constraint Satisfaction Problem) model, we need first to import the library PyCSP$^3$:

from pycsp3 import *

Then, we need some data. Actually, we just need an integer $n$.

n = 10

We start our CSP model by introducing an array $x$ of variables.

# x[i] is the ith value of the sequence
x = VarArray(size=n, dom=range(n))

We can display the structure of the array, as well as the domain of the first variable (remember that all variables have the same domain).

print("Array x: ", x)
print("Domain of any variable: ", x[0].dom)

Array x:  [x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9]]
Domain of any variable:  0..9

Concerning the constraints, the constraint Cardinality is exactly what we need here. Here, it simply states that each value $i$ in $0..n-1$ must occur exactly $x[i]$ times; a required named parameter called occurrences is given as value a Python dictionary for storing that information.

satisfy(
   # each value i occurs exactly x[i] times in the sequence
   Cardinality(x, occurrences={i: x[i] for i in range(n)}),
);

Interestingly, by calling the function solve(), we can check that the problem is satisfiable (SAT. We can also display the found solution. Here, we call the function values() that collects the values assigned to a specified list of variables.

if solve() is SAT:
    print(values(x))

[6, 2, 1, 0, 0, 0, 1, 0, 0, 0]

One may wonder how many solutions exist. The answer is given by executing the following code:

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

Number of solutions:  1

One can mathematically prove that every solution respects the two following equations:

$x_0 + x_1 + x_2 + x_3 + \dots + x_{n-1} = n$

$-1x_0 + 0x_1 + 1x_2 + 2x_3 + \dots + (n-2)x_{n-1} = 0$

Hence, it may be a good idea of posting them:

satisfy(
   # tag(redundant-constraints)
   [
      Sum(x) == n,
      Sum((i - 1) * x[i] for i in range(n)) == 0
   ]
);

Note that these two constraints are put inside a tagged list, which clearly informs us that they are redundant (i.e., do not change the set of solutions). Tags can also be possibly exploited by solvers. Tagging is made possible by putting in a comment line an expression of the form tag(), with a token (or a sequence of tokens separated by a white-space) between parentheses.

If we run again the solver, one can still find the solution.

if solve() is SAT:
    print(values(x))

[6, 2, 1, 0, 0, 0, 1, 0, 0, 0]

Finally, we give below the model in one piece. Here the data is expected to be given by the user (in a command line).

from pycsp3 import *

n = data

# x[i] is the ith value of the sequence
x = VarArray(size=n, dom=range(n))

satisfy(
   # each value i occurs exactly x[i] times in the sequence
   Cardinality(x, occurrences={i: x[i] for i in range(n)}),

   # tag(redundant-constraints)
   [
      Sum(x) == n,

      Sum((i - 1) * x[i] for i in range(n)) == 0
   ]
)