[algorias]

The tricky task of label placement could be outsourced to a SAT solver.

The way it works is that for every city, town etc you generate a few placement candidates (4 positions around the point like you do seems fine) and then calculate all the pairs of placements that collide. For each collision you add a clause to a SAT formula that forbids this combination from occurring. Every solution of this formula will be a clean labeling of your map.

[klipt]

That seems like a way of changing a nice, convex problem into a much harder to solve NP-complete problem...

[algorias]

I think you underestimate how hard the original problem is. Small decisions can cascade and have effects very far away on the map. Also, in what exact sense do you mean convex?

Furthermore, SAT is hard in theory but the kind of very structured instances found in practice tend to respond well to heuristics.