Improve performance of map clustering

[choefele]

The library we use for clustering, Google Maps Android API utility library has turned out to be too slow for ~6000 items. We need to evaluate faster alternatives.

The Google library has an alternative clustering algorithm that we could try. But we should also test alternative libraries.

• https://github.com/googlemaps/android-maps-utils with GridBasedAlgorithm
• https://github.com/mg6maciej/android-maps-extensions
• https://github.com/twotoasters/clusterkraf

[choefele]

See branch com.androidmapsextensions, which uses this library. Performance isn't perfect, but better than android-maps-utils (doesn't use animations, though)