In my last post I described the general approach I used to draw orthogons using an SMT solver, but left some of the details as exercises. In this post I’ll explain the solutions I came up with.

Forbidding touching edges

One of the most important constraints to encode is that two non-adjacent edges of an orthogon shouldn’t touch at all. How can we encode this constraint in a way that the SMT solver will accept? In particular, given two horizontal or vertical edges and , we want to come up with a logical expression—using “and” and “or”, addition, comparisons like , , or , and the functions and —which is true if and only if the two edges don’t touch.

It turns out that we can simplify matters by thinking about how to test whether two axis-aligned rectangles intersect (though this might not seem simpler at first—trust me!).

By axis-aligned I mean that the edges of the rectangles are horizontal and vertical, as in the picture above. The rectangles in the bottom-right do not intersect; all the other pairs of rectangles do intersect (including the bottom-left pair, which only touch along an edge).

One way we can simplify things yet again is to think about each dimension independently: two rectangles intersect if and only if they overlap along the -axis and along the -axis. So imagine projecting the two rectangles down onto the -axis; this results in two intervals.

One thing we have to be careful about up front is that we don’t know which order the interval endpoints will be given in. Given an interval with endpoints at and , we can define and . Then we know that is the smaller (leftmost) endpoint and is the bigger (rightmost) endpoint.

So now suppose we have two intervals, and , where we have already “sorted” the endpoints using the above technique, so we know and . How can we tell if these intersect? One approach is to try writing down a bunch of cases: the intervals intersect if is in between the endpoints of the second interval, OR if is in between them, OR if … but this quickly gets tedious, and there is a better way: it is simpler to think about when the intervals don’t intersect. If they don’t intersect, as in the bottom-right example in the above diagram, there must be a gap between the end of the first (leftmost) interval and the start of the next. Put another way, the right end of the left interval must be strictly less than the left end of the right interval.

But how can we tell which interval is the “left” interval and which is the “right” interval? These designations might not even make sense if the intervals do intersect. The key is to realize that we don’t actually care about which interval is where, but only about the relative order of their endpoints: the “right end of the left interval” is really just the leftmost right end, that is, ; similarly the left end of the right interval is just the rightmost left end, that is, . Putting this together, the intervals do not intersect if and only if

Believe it or not, we’re almost done! We just need a couple more observations:

• We can similarly project the rectangles onto the -axis and analyze whether those intervals intersect. Two rectangles intersect if and only if their projections intersect along the -axis and the -axis. Conversely, two rectangles don’t intersect if and only their projections don’t intersect along the -axis or the -axis.
• But we wanted to test line segments, not rectangles, right? Well, line segments can be thought of as just infinitely thin rectangles! Nothing in our analysis breaks if we allow this. When we project onto an axis we might get a degenerate interval consisting of a single point (where the left and right endpoints are the same), but this is perfectly OK—everything still works.

Putting this all together, given two horizontal or vertical line segments and :

• We first define , , and so on for , , , , , and .

• Then the segments don’t intersect if they don’t intersect along either axis:

  

Of course this all depends crucially on the assumption that the segments are horizontal or vertical. (Can you see where it goes wrong if this assumption is false? That is, can you come up with an example involving non-axis-aligned segments where this procedure says they intersect when they actually don’t, or vice versa?)

Computing orthogon perimeters

I also mentioned writing down an expression for the perimeter of the generated orthogon, so we can tell the SMT solver to minimize it. Of course, given a segment we can just write down the formula for its length as , and then add all these up. But this is no good since the and are explicitly required to be integers, and we’d rather not make the SMT solver deal with arithmetic on real numbers, which we would have to if we wanted it to take square roots. (It can deal with floating-point numbers, but it’s best avoided unless really necessary). And intuitively, dealing with real numbers is definitely overkill here, because the length of each edge is going to be an integer. So we’d like to find a way to talk about the length without using square root.

Once again, the assumption that the edges are always horizontal or vertical comes to our rescue. Suppose the edge is horizontal: in that case, will be zero, and the distance formula simplifies to . Likewise, if the segment is vertical, its length is . So in general, we could express the length of the segment by writing a condition that checks whether and yields either or depending on the answer. But we can be slightly more clever than this: we don’t need any conditions if we simply write the length as

One of these will always be zero, leaving the other as the correct length.

You might be familiar with the above formula: it is known as the Manhattan or taxicab distance between and —so called because it corresponds to the distance between two points when you can only travel horizontally or vertically (such as in a city, like Manhattan, with a grid of streets). To use a fancier term, it’s the distance between the points in the metric (the usual distance formula is called the metric). The above discussion amounts to the observation that the and metrics are equal for horizontal or vertical segments, which makes sense: if you want to travel between two locations on the same street, you’ll travel the same distance no matter whether you take a taxi or a crow.