ILP Part 10 – Sort

This is the tenth part of the ILP series. For your convenience you can find other parts in the table of contents in Part 1 – Boolean algebra

Today we are going to use conditional operator to implement something similar to selection sort. Let’s begin.


Selection sort goes as follows:

In every iteration we look for the lowest element in the rest of the array and then we swap current element with the one we have just found. We are going to implement something similar. Because we don’t know yet how to define loop, we need to define order in different way. Basically, we will define requirements for element on every single position which will make sure that the array is sorted.


We will start with the following variables:

    \begin{gather*} n \in \mathbb{N_+}\\ x_1, x_2, \ldots, x_n \in \mathbb{Z} \\ k \in \mathbb{Z_+} |x_1|, |x_2|, \ldots, |x_n| \le k \\ x = \left(x_1, x_2, \ldots, x_n\right) \end{gather*}

We have a vector of n integer variables. We are going to compare values so we need to add constraints for maximum possible value for every variable.
We need another vector which will represent the sorted variables:

    \begin{gather*} y_1, y_2, \ldots, y_n \in x \\ y_1 \ge y_2 \ge \cdots \ge y_n \\ y = \left(y_1, y_2, \ldots, y_n\right) \end{gather*}

y is just a sorted vector x. Before we define the general formula, let us start with an example.

Sorting three variables

Imagine that we want to sort three variables x_1 = 5, x_2 = 2, x_3 = 3. For now let’s also assume that we have no duplicates, so x_1 \ne x_2, x_1 \ne x_3, x_2 \ne x_3.
First, we need to compare every pair and check the ordering. We calculate the following variables:

    \begin{gather*} x_{x_1 \ge x_2} = x_1 \stackrel{?}{\ge} x_2 = 5 \stackrel{?}{\ge} 2 = 1\\ x_{x_1 \ge x_3} = x_1 \stackrel{?}{\ge} x_3 = 5 \stackrel{?}{\ge} 3 = 1\\ x_{x_2 \ge x_1} = x_2 \stackrel{?}{\ge} x_1 = 2 \stackrel{?}{\ge} 5 = 0\\ x_{x_2 \ge x_3} = x_2 \stackrel{?}{\ge} x_3 = 2 \stackrel{?}{\ge} 3 = 0\\ x_{x_3 \ge x_1} = x_3 \stackrel{?}{\ge} x_1 = 3 \stackrel{?}{\ge} 5 = 0\\ x_{x_3 \ge x_2} = x_3 \stackrel{?}{\ge} x_2 = 3 \stackrel{?}{\ge} 2 = 1\\ \end{gather*}

We have compared all pairs and for each variable we know the number of smaller variables. Now we need to know the total count of not less variables:

    \begin{gather*} x_{s1} = x_{x_1 \ge x_2} + x_{x_1 \ge x_3} = 1 + 1 = 2 \\ x_{s2} = x_{x_2 \ge x_1} + x_{x_2 \ge x_3} = 0 + 0 = 0 \\ x_{s3} = x_{x_3 \ge x_1} + x_{x_3 \ge x_2} = 0 + 1 = 1 \\ \end{gather*}

We are almost there. We have compared the values and we know their ordering. Now we need to construct final vector. Value y_i is the i-th biggest value:

    \begin{gather*} y_0 = x_{s1} \stackrel{?}{=} 0\ ?\ x_1\ :\ x_{s2} \stackrel{?}{=} 0\ ?\ x_2\ :\ x_3\\ y_1 = x_{s1} \stackrel{?}{=} 1\ ?\ x_1\ :\ x_{s2} \stackrel{?}{=} 1\ ?\ x_2\ :\ x_3\\ y_2 = x_{s1} \stackrel{?}{=} 2\ ?\ x_1\ :\ x_{s2} \stackrel{?}{=} 2\ ?\ x_2\ :\ x_3 \end{gather*}

For every y_i we choose variable which is not less than i different values. We assumed that all x_i are different so there is only one value which satisfies the condition. However, if that is not be the case we might modify the formula to handle the duplicates:

    \begin{gather*} y_0 = \min \left(x_{s1} \stackrel{?}{\ge} 0\ ?\ x_1\ :\ k, x_{s2} \stackrel{?}{\ge} 0\ ?\ x_2\ :\ k, x_{s_3} \stackrel{?}{\ge} 0\ ?\ x_3\ :\ k \right)\\ y_1 = \min \left(x_{s1} \stackrel{?}{\ge} 1\ ?\ x_1\ :\ k, x_{s2} \stackrel{?}{\ge} 1\ ?\ x_2\ :\ k, x_{s_3} \stackrel{?}{\ge} 1\ ?\ x_3\ :\ k \right)\\ y_2 = \min \left(x_{s1} \stackrel{?}{\ge} 2\ ?\ x_1\ :\ k, x_{s2} \stackrel{?}{\ge} 2\ ?\ x_2\ :\ k, x_{s_3} \stackrel{?}{\ge} 2\ ?\ x_3\ :\ k \right) \end{gather*}

For every y_i we choose select values which are not less than at least i different values and then we choose the minimum. For instance, when x_1 = x_2 = x_3 = 5, every x_{x_i \ge x_j} is one, so the sums x_{si} are equal to 2, but we are still able to construct the final vector.

Final formula

General sorting formula goes as follows:

    \begin{gather*} \displaystyle\mathop{\forall}_{\substack{ i=0,\ldots,n \\ j=0, \ldots, n \\ j \ne i}} x_{x_i \ge x_j} = x_i \stackrel{?}{\ge} x_j \\ \displaystyle\mathop{\forall}_{i=0, \ldots, n} x_{si} = \sum_{\substack{j=0 \\ j \ne i }}^{n} x_{x_i \ge x_j}\\ \displaystyle\mathop{\forall}_{i=0, \ldots, n} y_i = \displaystyle\mathop{\min}_{j=0, \ldots, n} \left( x_{sj} \stackrel{?}{\ge} i\ ?\ x_j\ :\ k \right) \end{gather*}


We are now able to sort any integer variables. This algorithm requires O\left(n^2\right) temporary variables because we compare every possible pair so is rather memory-consuming but works quite well and solvers are able to calculate the results rather smoothly.

Bonus chatter

As an exercise you might want to implement counting sort. What is the space complexity of your solution?