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

- An
*orthogon*is a polygon with only right angles. Two orthogons are considered the same if you can turn one into the other by rotation, reflection, and changing edge lengths. - Every orthogon has an even number of vertices, which can be classified as either convex or concave. There are always exactly four more convex vertices than concave.
- An
*orthobrace*is a sequence of X’s and V’s with exactly four more X’s than V’s, with two orthobraces considered the same if they are rotations or reflections of each other. Orthobraces are in 1-1 correspondence with orthogons. - Listing orthobraces naively is inefficient, but there is a (surprisingly complicated) algorithm for listing them efficiently.
- To draw all possible orthogons, we want to list orthobraces and turn them into good drawings, but this turns out to be surprisingly difficult.

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

- No two edges intersect or touch, other than adjacent edges at their shared vertex.
- The length of each edge is a positive integer.
- 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” () and “there 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 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: . (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 and which encode all the rules for a valid orthogon.

We might as well start by assuming the first edge, from to , travels in the positive direction. We can encode this with two constraints:

means the edge is horizontal; expresses the constraint that the second endpoint is to the right of the first (and since and 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 direction:

And so on. We go through each edge (including the last one from back to ), 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 and , 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 , , or , and the functions and (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 and 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 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):

Pingback: SMT solutions | The Math Less Traveled