Solving Skyscrapers using Z3

Using the fantastic Z3 for fun.

By Vamshi Jandhyala in Z3 python

October 28, 2019


Fill the grid with numbers, so that every number appears only once in every row and column. The numbers used range from $1$ upto the length of each row or column.

Imagine the grid is the aerial view of a city block of skyscrapers of varying heights, one within each cell in the grid. Each skyscraper is to be represented as a number indicating its height.A number outside the grid describes how many skyscrapers can be seen along that row or up/down that column from the perspective of that number on the ground. You can only see a skyscraper if smaller skyscrapers are in front of it; you cannot see one if a taller skyscraper is in front of it, blocking the view.

Here is a $6\times6$ Skyscraper puzzle

Python code using Z3

from z3 import *
from itertools import permutations
from collections import defaultdict

class SkyscrapersSolver:
    def __init__(self, n, puzzle):
        self.n = n
        self.input = puzzle
        self.perms = defaultdict(set)
        self.X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(n)]
                      for i in range(n)]
        self.s = Solver()
        self.s.add([And(1 <= self.X[i][j], self.X[i][j]<= n) for i in range(n) for j in range(n)])
        for i in range(n):
        for j in range(n):
            self.s.add(And(Distinct([self.X[i][j] for i in range(n)])))

    def classify_permutations(self):
        def num_of_visible_ss(arr, reverse=False):
            if reverse:
                arr = arr[-1::-1]
            v = 0
            for i in range(0, len(arr)):
                if arr[i] >= max(arr[0:i+1]):
                    v += 1
            return v

        for p in permutations(range(1, self.n+1)):
            self.perms[("R", num_of_visible_ss(p))].add(p)
            self.perms[("L", num_of_visible_ss(p, reverse=True))].add(p)

    def set_constraints(self):
        gl_consts = []
        for dr, rn, ns  in self.input:
            if dr == "R" or dr == "L":
                poss_perms = []
                for p in self.perms[(dr,ns)]:
                    poss_perms.append(And([self.X[rn-1][i] == v for i,v in enumerate(p)]))
                mdr = "R" if dr == "D" else "L"
                poss_perms = []
                for p in self.perms[(mdr, ns)]:
                    poss_perms.append(And([self.X[i][rn-1] == v for i,v in enumerate(p)]))

    def output_solution(self):
        m = self.s.model()
        for i in range(self.n):
            print("  ".join(['{:>2}'.format(str(m.evaluate(self.X[i][j])))
                    for j in range(self.n)]))

    def solve(self):
        if self.s.check() == sat:
            print("Failed to solve.")

puzzle = ([("R",3,4),("R",6,3),("D",3,2),("D",4,3),("D",6,2),("L",2,2),("L",5,3),
sss = SkyscrapersSolver(6, puzzle)


Here is the solution to the puzzle above

2   6   4   1   3   5

4   3   2   5   6   1

1   2   3   6   5   4

6   5   1   4   2   3

5   4   6   3   1   2

3   1   5   2   4   6