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

Last time we implemented a selection sort in ILP. Today we are going to do something similar: we are going to implement counting sort.

Introduction

As you probably remember from your classes, counting sort is useful when we try to sort values from small and finite set. It is for instance great for sorting people by their age because there are no people older than 200 years so we have at most two hundred possible values (and we can confine this range even more). What’s more, counting sort time complexity is linear so in theory it should work faster than selection sort. So let’s begin.

Problem definition

First, let’s define necessary variables:

We have variables to sort. Every variable has a value from set . Set has variables . Variables represents the final result.
We are going to sort variables using the knowledge that they all come from the set .

Algorithm

Our algorithm will have the following steps:

• Compare every with every
• Sum results of comparisons to know how many values are there actually
• Construct the final vector

Comparing

We define the following variables:

We basically try to find them number of values in vector . After this step we have different variables.

Summing results

Now we need to know how many values are there so we define the following variables:

Now we know that there are exactly values in vector . We now need to aggregate the results to be able to reconstruct the vector, so we define the partial sums:

This value tells us that there are exactly elements not greater than . This might be a bit tricky so let’s consider an example first.

Example

Let’s imagine that we want to sort the following vector:

We can see that and we have values. We also assume the following set of possible values:

Basically we assumed that our values are not greater than and not less than . It is worth noting that in there is no variables equal to but this is how counting sort works. We now have the following results of comparisons:

Now we need to aggregate these values:

Right now we know that there are exactly variables in vector equal to . Now we sum the results:

And now we know that there are exactly values not greater than in vector , values not greater than and so on.

Constructing the result

Every variable tells us how many values not greater than there are in the original vector. We can utilize this knowledge to put values in correct places:

In our example it is:

This works in the following way: for every position we ask whether there are at least elements not greater than and we choose minimum of values. So we basically try to insert values in their places and we need to use function to select lowest possible value for every place.

Complexity

As you can see, this algorithm needs temporary variables. Assuming that our algorithm uses linear space. If it is not true that then it makes no sense using this algorithm but the same happens with casual counting sort. There is no use to sort numbers using this algorithm when the domain is really big.

Summary

We already know two sorting algorithms. Their implementation is rather straightforward and really resembles the imperative counterparts. As an exercise you might want to implement other imperative algorithms using similar approach.

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.

Algorithm

Selection sort goes as follows:

for i from 0 to array.length
    find minimum in array[i+1..array.length]
    swap found element with array[i]

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.

Variables

We will start with the following variables:

We have a vector of 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:

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

Sorting three variables

Imagine that we want to sort three variables . For now let’s also assume that we have no duplicates, so .
First, we need to compare every pair and check the ordering. We calculate the following variables:

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:

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

For every we choose variable which is not less than different values. We assumed that all 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:

For every we choose select values which are not less than at least different values and then we choose the minimum. For instance, when , every is one, so the sums are equal to , but we are still able to construct the final vector.

Final formula

General sorting formula goes as follows:

Summary

We are now able to sort any integer variables. This algorithm requires 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?