## Drawing orthogons with an SMT solver

I’m long overdue to finish up my post series on orthogons as promised. First, a quick recap:

Recall that we defined a “good” orthogon drawing as one which satisfies three criteria:

1. No two edges intersect or touch, other than adjacent edges at their shared vertex.
2. The length of each edge is a positive integer.
3. The sum of all edge lengths is as small as possible.

We know that good drawings always exist, but our proof of this fact gives us no way to find one. It’s also worth noting that good drawings aren’t unique, even up to rotation and reflection. Remember these two equivalent drawings of the same orthogon?

It turns out that they are both good drawings; as you can verify, each has a perimeter of 14 units. (I’m quite certain no smaller perimeter is possible, though I’m not sure how to prove it off the top of my head.)

So, given a list of vertices (convex or concave), how can we come up with a good drawing? Essentially this boils down to picking a length for each edge. The problem, as I explained in my previous post, is that this seems to require reasoning about all the edges globally. I thought about this off and on for a long time. Each new idea I had seemed to run up against this same local-global problem. Finally, I had an epiphany: I realized that the problem of making a good orthogon drawing can be formulated as an input appropriate for an SMT solver.

What is am SMT solver, you ask? SMT stands for “satisfiability modulo theories”. The basic idea is that you give an SMT solver a proposition, and it tries to satisfy it, that is, find values for the variables which make the proposition true. Propositions are built using first-order logic, that is, things like “and”, “or”, “not”, implication, as well as “for all” ($\forall$) and “there exists” ($\exists$). The “modulo theories” part means that the solver also supports various theories, that is, collections of extra functions and relations over certain sets of values along with axioms explaining how they work. For example, a solver might support the theory of integers with addition, multiplication, and the $\geq$ relation, as well as many other specialized theories.

Sometimes solvers can even do optimization: that is, find not just any solution, but a solution which gives the biggest (or smallest) value for some other function. And this is exactly what we need: we can express all the requirements of an orthogon as a proposition, and then ask the solver to find a solution which minimizes the perimeter length. SMT solvers are really good at solving these sorts of “global optimization” problems.

So, how exactly does this work? Suppose we are given an orthobrace, like XXXXXXVVXV, and we want to turn it into a drawing. First, let’s give names to the coordinates of the vertices: $(x_0, y_0), (x_1, y_1), \dots, (x_{n-1}, y_{n-1})$. (Note these have to be integers, which enforces the constraint that all edge lengths are integers.) Our job is to now specify some constraints on the $x_i$ and $y_i$ which encode all the rules for a valid orthogon.

We might as well start by assuming the first edge, from $(x_0, y_0)$ to $(x_1, y_1)$, travels in the positive $x$ direction. We can encode this with two constraints:

• $y_1 = y_0$
• $x_1 > x_0$

$y_1 = y_0$ means the edge is horizontal; $x_1 > x_0$ expresses the constraint that the second endpoint is to the right of the first (and since $x_0$ and $x_1$ are integers, the edge must be at least 1 unit long).

We then look at the first corner to see whether it is convex or concave, and turn appropriately. Let’s assume we are traveling counterclockwise around the orthogon; hence the first corner being convex means we turn left. That means the next edge travels “north”, i.e. in the positive $y$ direction:

• $x_2 = x_1$
• $y_2 > y_1$

And so on. We go through each edge (including the last one from $(x_{n-1}, y_{n-1})$ back to $(x_0, y_0)$), keeping track of which direction we’re facing, and generate two constraints for each.

There’s another very important criterion we have to encode, namely, the requirement that no non-adjacent edges touch each other at all. We simply list all possible pairs of non-adjacent edges, and for each pair we encode the constraint that they do not touch each other. I will leave this as a puzzle for you (I will reveal the solution next time): given two edges $(x_{11},y_{11})\text{---}(x_{12},y_{12})$ and $(x_{21},y_{21})\text{---}(x_{22},y_{22})$, how can we logically encode the constraint that the edges do not touch at all? You are allowed to use “and” and “or”, addition, comparisons like $>$, $<$, $\geq$ or $\leq$, and the functions $\mathrm{max}$ and $\mathrm{min}$ (which take two integers and tell you which is bigger or smaller, respectively). This is tricky in the general case, but made much easier here by the assumption that the edges are always either horizontal or vertical. It turns out it is possible without even using multiplication.

Finally, we write down an expression giving the perimeter of the orthogon (how?) and ask an SMT solver to optimize it subject to the constraints. I used the Z3 solver via the sbv Haskell library. It outputs specific values for all the $x_i$ and $y_i$ which satisfy the constraints and give a minimum perimeter; from there it’s a simple matter to draw them by connecting the points.

To see this in action, just for fun, let’s turn the orthobrace XVXXVXVVXVVXXVVXVVXXXXXXVVXXVX (which I made up randomly) into a drawing. This has 30 vertices (and 30 edges); hence we are asking the solver to find values for 60 variables. We give it two constraints per edge plus one (more complex) constraint for every pair of non-touching edges, of which there are 405 (each of the 30 edges is non-adjacent to 27 others, so $30 \times 27 = 810$ counts each pair of edges twice); that’s a total of 465 constraints. Z3 is able to solve this in 15 seconds or so, yielding this masterpiece (somehow it kind of reminds me of Space Invaders):