(J. Waldmann, Leipzig) (Version of 29-October-2025)
The Skyline (Towers, Wolkenkratzer) puzzle asks to replace each dot with a number (the height of a house) from 1 to 7 such that
[1 .. 7][1 .. 7]example: left: instance, right: solution.
+ - - - - - - - - + + - - - - - - - - +
| . . . . . . . . | | 6 1 8 7 3 2 5 4 |
7 | . . . . . . . . | 7 | 1 2 3 4 6 7 8 5 |
6 | . . . . . . . . | 6 | 3 4 5 2 1 6 7 8 |
| . . . . . . . . | 7 | 5 8 7 6 4 3 2 1 | 7
6 | . . . . . . . . | 6 | 2 3 4 5 7 8 1 6 |
| . . . . . . . . | 7 | 8 7 6 1 5 4 3 2 | 7
| . . . . . . . . | | 4 5 2 3 8 1 6 7 |
| . . . . . . . . | | 7 6 1 8 2 5 4 3 |
+ - - - - - - - - + + - - - - - - - - +
5 2 5 2 The following shows the visible numbers (from the left) in the third row
6 | 3 4 5 2 1 6 7 8 |
V V V V V VInstances of this puzzle get published in several places, under several names
Variants are:
We consider here the challenge of building thin unique instances (thin = with few clues), for the standard case (no holes), and with outside clues only (empty grid).
Experiments (below) indicate that for (small) size n, there always is an instance with (n-1) clues (confirmed for n from 1 to 9), and this bound seems sharp (for these numbers). Asympotic behaviour is not at all clear.
The basis of our approach is an encoding the skyline problem (given an instance, find a solution) as a Boolean satisfiability problem. We represent numbers in unary (the one-hot encoding). To get the permutation property in each row and column, we use an exactly-one constraint. All constructions are standard, and are realized via the https://hackage.haskell.org/package/ersatz library (Kmett et al., 2010) and use the https://github.com/arminbiere/kissat solver (Biere, 2020)
I will publish my code, but not right now, since construction of the SAT encoding is student homework in my lecture on constraint programming.
We discuss here how to find thin unique instances by an evolutionary process, and we propose to use (approximate) model counting for selection.
The algorithm maintains a population of candidates. A candidate is a solvable (but not necessarily uniquely solvable) instance. Initially, this is just the empty instance (no clues, has many solutions). We iteratively pick one candidate c from the population, compute a random mutation m of c, and add m to the population. If m is uniquely solvable, we print it.
The interesting parts are
Mutation:
This creates a solvable instance. Mutation is fully random, the resulting instance might have a large number of solutions. This could be improved with guided mutation (do several tries, take the best one). We get a similar effect by adding the fully random mutant to the population, but select it with lower probability later.
Selection:
We select a group, preferring smaller number of solutions. From that, we select a sub-group, preferring smaller size. From that sub-group, we uniformly select a candidate (for mutation). Mutation creates another candidate (it does not change the one that we selected).
Number of solutions of a formula F is approximated very crudely: as long as F is satisfiable, add a random XOR clause (e.g., containing 3 variables). Let c be the number of clauses that were added. Then F is expected to have 2^c models. To improve accuracy, we may repeat this experiment, and take the average. To bound the work, we start the next experiment only if the total number of clauses used so far, does not exceed a threshold, say, 10. The experiment then will run until the end (possibly beyond the threshold).
There are better ways to approximately count models, cf. Soos 2018 https://www.msoos.org/2018/12/how-approximate-model-counting-works/, Sharma et al. 2019 https://www.ijcai.org/proceedings/2019/163.
Our approximation is naive. How good is it? The set of
solutions of an instance of width n with no clues is the set
of Latin Squares (each row and each column is a permutation
of [1 .. n]). The numbers of Latin squares of
small orders are known exactly (https://oeis.org/A002860).
The number or XOR clauses that need to be added before
unsatisfiability appear to be in the ranges
[14 .. 17], [35 .. 50],
[70 .. 80], respectively.
The experiments suggest that for (small) size n, there are uniquely solvable instances with (n-1) clues. Can we expect this to hold for large n?
The Skyline variant where clues might also be in the grid, trivially has unique instances of any size. That is why we consider the variant with external clues only (it is more interesting).
There are full instances (having all 4 * n external clues) that are ambiguous. A smallest such example is
1 2 2 4 1 2 2 4 1 2 2 4 1 2 2 4
+ - - - - + + - - - - + + - - - - + + - - - - +
1 | . . . . | 4 1 | 4 3 2 1 | 4 1 | 4 3 2 1 | 4 1 | 4 3 2 1 | 4
2 | . . . . | 2 2 | 3 4 1 2 | 2 2 | 3 1 4 2 | 2 2 | 3 c c 2 | 2
2 | . . . . | 2 2 | 2 1 4 3 | 2 2 | 2 4 1 3 | 2 2 | 2 c c 3 | 2
4 | . . . . | 1 4 | 1 2 3 4 | 1 4 | 1 2 3 4 | 1 4 | 1 2 3 4 | 1
+ - - - - + + - - - - + + - - - - + + - - - - +
4 2 2 1 4 2 2 1 4 2 2 1 4 2 2 1 It might happen that there is some (large) size n for which there are no unique instances (each full instance is either unsolvable, or ambiguous).
The following information-theoretic argument might
support this: the total number of latin squares is
(n * exp(-2))^n^2. This has
n^2 log(n) bits of information, but we can only
put 4 n log(n) bits in the clues. So, “on
average”, a large full instance is ambiguous. This does not
preclude the existence of large unique instances.
Perhaps we can prove that each large enough latin square
has a central area (sub-square) C and numbers x, y such that
all occurrences of x and y in C can be swapped, since all
occurrences of x in C are invisible from the outside. (In
the above, x = 1, y = 4, and C is marked by
c)
There are unsolvable instances, for any size, just by this pattern
l | . . . . . . . . . | r
where l + r > n + 1. Proof: consider the position p of the largest number n. Clearly, l <= p (looking from the left, we see at most p roofs) and r <= (n + 1 - p) (from the right)
Ruling out these situations, we still have unsolvable instances like this (n = 9)
7 | . . . . . . . . . |
+ - - - - - - - - - +
a b cwhere a, b, c are numbers > 1. Proof: number 9 must be at position 7 or later, but then, one of a, b, c must be 1.
3 3 : 3 3
+ - - - - + : + - - - - +
| . . . . | : | 3 2 4 1 |
| . . . . | : | 4 1 2 3 |
| . . . . | : | 2 3 1 4 |
| . . . . | 3 : | 1 4 3 2 | 3
+ - - - - + : + - - - - + 4 4 4 4 4 : 4
+ - - - - - + + - - - - - + + - - - - - + : + - - - - - +
4 | . . . . . | 4 | 2 3 1 4 5 | | . . . . . | 4 : | 2 5 4 3 1 | 4
| . . . . . | | 3 5 2 1 4 | | . . . . . | : | 3 4 2 1 5 |
4 | . . . . . | 4 | 1 2 4 5 3 | 4 | . . . . . | : 4 | 1 2 3 5 4 |
| . . . . . | | 4 1 5 3 2 | | . . . . . | : | 4 1 5 2 3 |
| . . . . . | | 5 4 3 2 1 | | . . . . . | : | 5 3 1 4 2 |
+ - - - - - + + - - - - - + + - - - - - + : + - - - - - +
4 : 4 + 4 + + 4 + + 4 3 4 +
. . . . . 4 . . . . . 4 . . . . .
. . . . . 4 . . . . . . . . . .
. . . . . . . . . . . . . . .
. . . . . 4 . . . . . . . . . .
. . . . . . . . . . 4 . . . . .
+ 4 + + 4 + + + 4 3 4
+ 4 4 + + + + - - - - - +
. . . . . . . . . . 4 | . . . . . |
3 . . . . . . . . . . | . . . . . |
. . . . . . . . . . | . . . . . |
. . . . . 3 4 . . . . . | . . . . . | 4
. . . . . 4 . . . . . | . . . . . |
+ + + 4 + + - - - - - + + 5 + + + + +
. . . . . . 5 . . . . . . 5 . . . . . .
. . . . . . 3 . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 5
. . . . . . . . . . . . 2 . . . . . .
. . . . . . 5 4 . . . . . . . . . . . .
. . . . . . 5 . . . . . . . . . . . .
+ 5 4 + + 5 + + 4 5 4 + + + + + + 5 5 +
. . . . . . 4 . . . . . . 3 5 . . . . . .
. . . . . . . . . . . . 5 . . . . . .
. . . . . . 5 . . . . . . 5 . . . . . .
. . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 4 . . . . . .
. . . . . . 4 . . . . . . . . . . . .
+ 5 4 + + 4 5 + + 4 ++ 5 +
. . . . . . 5
. . . . . .
. . . . . .
. . . . . .
5 . . . . . .
. . . . . . 3
+ 5 ++ 6 2 + + 4 6 +
. . . . . . . 5 . . . . . . .
. . . . . . . 6 . . . . . . .
. . . . . . . 6 . . . . . . .
. . . . . . . . . . . . . .
6 . . . . . . . . . . . . . .
. . . . . . . . . . . . . .
. . . . . . . 5 5 . . . . . . .
+ + + 5 6 + 6 6 6 5
+ - - - - - - - + + - - - - - - - +
6 | . . . . . . . | | . . . . . . . |
| . . . . . . . | | . . . . . . . |
| . . . . . . . | | . . . . . . . | 6
| . . . . . . . | 5 | . . . . . . . |
| . . . . . . . | 5 | . . . . . . . |
| . . . . . . . | 5 | . . . . . . . |
| . . . . . . . | 5 | . . . . . . . |
+ - - - - - - - + + - - - - - - - +
6 5 + 6 7 +
. . . . . . . .
. . . . . . . . 7
. . . . . . . .
. . . . . . . .
. . . . . . . . 4
. . . . . . . . 6
. . . . . . . .
. . . . . . . .
+ 6 6 +
+ - - - - - - - - + + - - - - - - - - +
| . . . . . . . . | | 6 1 8 7 3 2 5 4 |
7 | . . . . . . . . | 7 | 1 2 3 4 6 7 8 5 |
6 | . . . . . . . . | 6 | 3 4 5 2 1 6 7 8 |
| . . . . . . . . | 7 | 5 8 7 6 4 3 2 1 | 7
6 | . . . . . . . . | 6 | 2 3 4 5 7 8 1 6 |
| . . . . . . . . | 7 | 8 7 6 1 5 4 3 2 | 7
| . . . . . . . . | | 4 5 2 3 8 1 6 7 |
| . . . . . . . . | | 7 6 1 8 2 5 4 3 |
+ - - - - - - - - + + - - - - - - - - +
5 2 5 2 4 5 7 5 4 5 7 5
+ - - - - - - - - + + - - - - - - - - +
| . . . . . . . . | | 4 5 2 7 1 8 3 6 |
| . . . . . . . . | | 5 8 3 6 2 7 4 1 |
| . . . . . . . . | | 7 1 6 8 3 5 2 4 |
| . . . . . . . . | | 8 2 7 1 4 6 5 3 |
| . . . . . . . . | | 1 7 8 3 5 4 6 2 |
| . . . . . . . . | | 6 4 1 2 7 3 8 5 |
| . . . . . . . . | | 3 6 5 4 8 2 1 7 |
7 | . . . . . . . . | 7 | 2 3 4 5 6 1 7 8 |
+ - - - - - - - - + + - - - - - - - - +
2 7 2 7 6 6
+ - - - - - - - - - + + - - - - - - - - - +
8 | . . . . . . . . . | 8 | 2 3 4 5 1 6 7 8 9 |
8 | . . . . . . . . . | 8 | 1 2 3 4 5 7 8 9 6 |
| . . . . . . . . . | | 8 6 2 3 4 9 1 7 5 |
| . . . . . . . . . | 8 | 5 9 8 7 6 4 3 2 1 | 8
| . . . . . . . . . | 7 | 6 1 9 8 7 5 4 3 2 | 7
| . . . . . . . . . | 5 | 3 7 1 9 8 2 6 5 4 | 5
| . . . . . . . . . | 7 | 9 8 7 6 2 1 5 4 3 | 7
| . . . . . . . . . | | 7 4 5 1 9 3 2 6 8 |
5 | . . . . . . . . . | 5 | 4 5 6 2 3 8 9 1 7 |
+ - - - - - - - - - + + - - - - - - - - - + 8 8
+ - - - - - - - - - + + - - - - - - - - - +
| . . . . . . . . . | 5 | 3 7 1 9 8 2 6 5 4 | 5
| . . . . . . . . . | | 8 5 6 2 4 3 1 9 7 |
| . . . . . . . . . | 8 | 5 9 8 7 6 4 3 2 1 | 8
5 | . . . . . . . . . | 5 | 4 6 2 1 3 5 7 8 9 |
| . . . . . . . . . | 6 | 7 1 9 8 2 6 5 4 3 | 6
| . . . . . . . . . | | 6 4 5 3 9 7 2 1 8 |
| . . . . . . . . . | 8 | 9 8 7 6 5 1 4 3 2 | 8
6 | . . . . . . . . . | 6 | 2 3 4 5 1 8 9 7 6 |
6 | . . . . . . . . . | 6 | 1 2 3 4 7 9 8 6 5 |
+ - - - - - - - - - + + - - - - - - - - - +