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):

Advertisements
Posted in computation, geometry | Tagged , , , , , , , , , | Leave a comment

Chromatic number of the plane roundup

I’ve had fun writing about the Hadwiger-Nelson problem to determine the chromatic number of the plane, but I think this will be my last post on the topic for now!

More 7-colorings

Of course, the original point of the hexagonal 7-coloring in my last two posts is that it establishes an upper bound of CNP \leq 7 (although it turns out it’s also just a really cool pattern). Again, there is a balancing act here: we have to give each hexagon a diameter of < 1, so no two points in the same hexagon will be 1 unit apart; but we also have to make the hexagons big enough that same-colored hexagons are more than 1 unit from each other. This is indeed possible, since same-colored hexagons always have two “layers” of other hexagons in between them. Denis Moskowitz made a really nice graphic illustrating this:

In a comment on my previous post, Will Orrick pointed out that if you tile 3-dimensional space with cubes and color them with seven colors so that each cube is touching six others with all different colors, then take a diagonal slice through that space, you get this!

This is the same as the 7-colored hexagonal tiling I showed before, but with extra triangles in between the hexagons (and the colors of the triangles follow a pattern similar to the hexagons). I could stare at this all day! Here’s a version with numbers if you find it helpful. (If you support me on Patreon you can get automatic access to bigger versions of all the images I post—though to be honest if there’s a particular image you want a bigger version of, you can just ask nicely!)

What is CNP?

So, we know CNP is either 5, 6, or 7. So which is it? No one is really sure. With some unsolved problems, there is widespread agreement in the mathematical community on what the right answer “should be”, it’s just that no one has managed to prove it. That isn’t the case here at all. If you ask different mathematicians you will probably get different opinions on which number is correct. Some mathematicians even think the “right” answer might depend on which axioms we choose as a foundation of mathematics!—in particular that the answer might change depending on whether you allow the axiom of choice (a topic for another post, perhaps).

Posted in geometry | Tagged , , , , , , , , | 7 Comments

Some words on PWW #22

There are lots of patterns to be found in the picture from my previous post!

This is a really remarkable tiling. Here are a few special properties I know of:

  1. First of all, I hope you realized that the pattern can be extended infinitely to cover the whole plane with a hexagonal tiling. One way to convince yourself of this is to look at the horizontal strips of hexagons labelled 6 \dots 0. Each row of hexagons will just have 6 \dots 0 repeating forever; and each row is a copy of the row below it, offset by two and a half hexagons.

  2. Of course, there are seven different colors used (also indicated by the numbers 0 \dots 6).

  3. Instead of seeing it as made up of a bunch of repeating strips, you can also see it as made of a bunch of repeating parallelograms:

    Each parallelogram has four zeros at its corners, and contains one of every other color/number in its interior. (There’s actually nothing special about zero; you can make parallelograms using any number you choose for the corners.)

  4. Every hexagon touches six other hexagons, exactly one with each other color/number. For example, a hexagon labelled 1 will touch six hexagons labelled 0, 2, 3, 4, 5, and 6. (Can you see how to prove this? Think about how the whole tiling is built out of copies of the strip 6 \dots 0.) This explains what’s so special about having seven colors!

  5. If you pick any color and look at all the hexagons of that color, they are always arranged in the same pattern, at the vertices of an equilateral triangular grid. For example, below I have arbitrarily chosen to highlight all the number 3 hexagons:

    This means that if you pick any two colors/numbers, there is always some translation that will move all the hexagons of one color to the places that used to be occupied by the hexagons of the other color.

    Here’s what it looks like if we draw all these triangular grids overlaid on top of each other (with brighter colors just for fun). I think it’s remarkable that seven equilateral triangular grids fit together so precisely!

  6. In fact, since each hexagon touches one of each other color, for any two colors we can move all the hexagons of one color to those of the other by translating just one “hexagon unit”—that is, each hexagon will move to a hexagon next to it. For example, if we want to move all the number 3 hexagons so they match up with where the number 5 hexagons used to be, just move everything one hexagon down and to the right.

    I’ll reproduce the original image here so you can refer to it while thinking about this and the following properties:

  7. Each of the six directions we can translate corresponds to adding by a different number mod seven. For example, it’s easy to see that moving to the left corresponds to adding 1 (adding 1 to 6 wraps back around to 0 because we take the remainder when dividing by 7). In other words, pick any hexagon and look at its number; the hexagon to its left will have a number which is 1 bigger (mod 7). Moving down and to the right is adding 2: for example, starting at the 0 in the middle and following the line of hexagons down and to the right, we find 0, 2, 4, 6, 1, 3, 5, 0, where each number is two more than the previous (mod 7). Down and to the left is adding 3; and so on. I’ll let you work out the other three directions.

  8. As pointed out in a comment by Will, rotating corresponds to multiplication mod 7! For example, rotating 60 degrees counterclockwise around 0 corresponds to multiplying by 3 (mod 7). In counterclockwise order, the six numbers we find around 0 are 1, 3, 2, 6, 4, 5. We can check that 1 \times 3 = 3, and 3 \times 3 = 9 \equiv 2 \pmod 7, 2 \times 3 = 6, 6 \times 3 = 18 \equiv 4 \pmod 7, and so on. Rotating the other direction is multiplying by 5. Rotating by 120 degrees is multiplying by 2 or 4; rotating by 180 degrees is multiplying by 6.

  9. Pick a hexagon; say it contains the number n. We already know that none of the hexagons it touches contain n. But in fact, none of the hexagons those hexagons touch contain n either (except for the original hexagon we chose). This is because each hexagon touches exactly one copy of every other color/number. So, in other words, each hexagon is contained in two layers of hexagons, none of which share the same color with the central hexagon. For example, if we pick a zero hexagon and go two layers out from there, we can see that the zero in the middle is the only zero (and there are exactly 3 copies of each other number):

Let me know in the comments if you see any other patterns that I missed!

Posted in geometry, pattern | Tagged , , , | 9 Comments

Post without words #22

Image | Posted on by | Tagged , , , , , | 13 Comments

The Math Less Traveled on Patreon!

tl;dr: I’ve just created a Patreon page where you can pledge to support The Math Less Traveled with a small monthly donation and become part of a community that will help shape future posts and topics!

I’ve been writing this blog for almost twelve years (!). Over that time I’ve published more than 400 posts totaling almost 200,000 words. Writing The Math Less Traveled is not my job and I’ve never gotten paid for it; I just love to explore beautiful ideas and find creative ways to explain them to others.

Normally this is the place where I would say how The Math Less Traveled won’t be able to continue to exist without your support, and how I need to feed my family, and so on. But the honest truth is that my family is doing just fine, and I will probably continue writing The Math Less Traveled no matter what! It would just be nice to be rewarded for my hard work, and to at least be able to offset the cost of the frequent writing sessions in my favorite local coffee shop (where I’m writing this right now), buy some relevant books now and then, and upgrade my WordPress plan to have ads removed. I’m also excited to use Patreon as a platform to build a closer, more collaborative relationship with my readers: I will consult patrons at the $5/month level for things like feedback on drafts, research help, and ideas for topics, posts, and visualizations.

If you find my writing valuable, I hope you’ll consider becoming a patron, even at just a few dollars a month. Of course, there are also some cool rewards, like high-resolution versions of any graphics I make for the blog, and access to patron-only content (likely full of my random mathematical musings and stories about math conversations with my kids).

Thanks for reading regardless, and here’s to the next twelve years! Next up: how to color the plane using only seven colors (aka pretty pictures made by mathematically-minded bees!).

Posted in meta | Tagged , , | Leave a comment

The chromatic number of the plane, part 4: an upper bound

In my previous posts I explained lower bounds for the Hadwiger-Nelson problem: we know that the chromatic number of the plane is at least 5 because there exist unit distance graphs which we know need at least 5 colors. Someday, perhaps someone will succeed in constructing an even bigger unit distance graph that requires 6 colors, and then we’ll know CNP \geq 6.

But what about an upper bound? Can we say for sure that the CNP has to be smaller than some limit? Indeed, we can: we know that CNP \leq 7. Today I want to explain how we can show that CNP \leq 9; in another post I’ll show the proof that CNP \leq 7.

Proving an upper bound for the chromatic number of the plane is very different than proving a lower bound. A lower bound is all about showing that you can’t color the plane with a certain number of colors. An upper bound, on the other hand, is all about showing that you can. We know that CNP \leq 7 because there is a specific, valid way to color the plane using only seven colors! It might be possible to do it with fewer colors, using a very clever pattern, which is why 7 is only an upper bound. But at least we know it can be done with 7.

Let’s start with something simpler. Imagine coloring the whole plane with a repeating pattern like this:

Can this be a valid coloring of the plane? (Of course, we already know it can’t because it only uses four colors, and CNP > 4; but let’s see if we can give a more direct argument why this is not valid). First of all, the squares can’t be too big: we don’t want any pair of points inside the same square to be 1 unit apart. This means the diagonal of each square has to be less than 1.

So if the diagonals of the squares are less than 1, the sides of the squares have to be less than 1 / \sqrt 2. But the problem is that squares of the same color also have to be far enough apart so that no two points in same-colored squares are 1 unit apart. But in this scenario same-colored squares are separated by only one other square; if the sides of the squares is < 1 / \sqrt 2 \approx 0.707 then they are too close.

This idea can be easily salvaged, however: we just need more colors!

Now we are using nine colors, with a 3 \times 3 repeating pattern instead of 2 \times 2. Let’s see if we can make this work. Once again, the squares can’t be too big (lest two points inside the same square can be 1 unit apart) but same-color squares can’t be too close (lest two points in different same-color squares can be 1 unit apart). Call s the side length of the squares. The first condition once again gives us s < 1/\sqrt 2. What about the second condition? The shortest distance between two same-colored squares is now 2s, if you travel straight east-west or north-south. (You can confirm for yourself that any other line between same-colored squares is longer.) So we must have 2s > 1.

Can we pick a value of s that makes s < 1/\sqrt 2 and 2s > 1 both true? Yes! Rearranging a bit, this just says 1/2 < s < 1/\sqrt 2. Since 1/2 < 1/\sqrt 2 this gives us a valid range of values for s; any such value for s gives us a valid 9-coloring of the plane.

Hence, it is possible to color the plane using 9 colors, such that no two points at distance 1 from each other have the same color! We don’t know if this is the best way to color the plane (in fact, it isn’t!), but at least we know it is a way. So this shows that CNP \leq 9.

In my next post I’ll explain how we know that CNP \leq 7: the proof is similar in spirit, but more complex (and, of course, more efficient) due to its use of hexagons instead of squares.

Posted in geometry, proof | Tagged , , , , , , | Leave a comment

Iterating squared digit sums in other bases

In a previous post I wrote about iterating the squared digit sum function, which adds up the sum of the squares of the digits of a number; for example, s(149) = 1^2 + 4^2 + 9^2 = 1 + 16 + 81 = 98. Denis left a comment asking about other bases—what happens if we write a number in a base other than base ten and add up the squares of its digits in that base? It’s a good question, because the choice of adding up the squares of base ten digits, while natural from a human point of view, is mathematically quite arbitrary. We can sum the squares of the digits of a number written in any base.

As Denis noted in his comment, the argument from my previous post happily applies in any base, not just base 10! That is, if we consider a d-digit number in base b, the largest it can be is if it consists of d copies of the largest possible digit, which is b-1. In that case the sum of squares of its digits would be d(b-1)^2. For example, the largest sum of squares we could get with a six-digit number in base 5 is 444444, which gives us a sum of squares of 6 \cdot 4^2 = 96. But the claim is that this will be less than b^{d-1} as long as d \geq 4 and b \geq 2—which means that taking the sum of squares of the base-b digits of any number with four or more such digits will always result in a shorter base-b number. We can check that this is true when b = 2 and d = 4, since 4 \cdot 1^2 = 4 < 2^3 = 8; and intuitively, increasing either b or d will make the right-hand side increase more than the left-hand side, so it will always be true for b \geq 2 and d \geq 4. (This is an informal, hand-wavy argument—if you think you know of a way to prove it formally I would love to hear about it!)

The upshot is that for any base b \geq 2 we only have to try numbers with up to three digits to look for loops, since any bigger numbers will reduce until they have at most three digits. (One might wonder it will ever suffice to consider only two-digit numbers, when b gets large enough. The answer, perhaps surprisingly, is no. We would be looking for a base b such that 3(b-1)^2 < b^2—that is, a base for which three-digit numbers always reduce to two-digit numbers. As you can verify for yourself, the only solutions to this inequality are when b < 2! So four digits is the magic cutoff for every base b \geq 2. (I’m not going to consider negative bases here; maybe in another post.))

So I wrote a program which, for each base b, finds all the loops that happen on base-b numbers from 1 to b^3-1. It turns out that only a few bases have a single nontrivial loop, like base 10 (perhaps this is not surprising). The ones I have found are as follows. (After base 10 we quickly run out of digits; I use lowercase letters a to z to stand for digits 10 through 35, and then uppercase letters A to Z to stand for digits 36 through 61.)

  • Base 6: 32 \to 21 \to 5 \to 41 \to 25 \to 45 \to 105 \to 42
  • Base 10: 4 \to 16 \to 37 \to 58 \to 89 \to 145 \to 42 \to 20
  • Base 16: a9 \to b5 \to 92 \to 55 \to 32 \to d
  • Base 20: e9, dh, 12i, g9, gh, 175, 3f, be, fh, 15e, b2, 65, 31, a, 50, 15, 16, 1h, ea, eg, 12c, 79, 6a, 6g, ec, h0
  • Base 26: o1 \to m5 \to jf \to me \to 104 \to h \to b3 \to 50 \to p
  • Base 40: 3p \to fy \to yl \to DB \to 1wa \to s5 \to k9 \to c1

Base 20 is particularly magnificent: there is a single nontrivial loop, and it has length 26!

I let my program run all the way up to base 150 (which took about 3.5 minutes on my admittedly not-so-fast laptop). Here’s some trivia:

  • After base 40, I didn’t find any more bases with only a single nontrivial loop. I conjecture there aren’t any more.
  • There are two bases tied for longest loop: base 119 and base 146 both have a loop of length 110.
  • The record holder for most loops is base 73, which has twenty-nine distinct loops into which iterating squared digit sum can fall, many of which consist of a single number: in addition to 1, each of 82, 234, 533, 1125, 1640, 2080, 2665, 2738, 3321, 3757, 4264, 4840, 5125, and 5265 is equal to the sum of squares of its own digits when written in base 73. For example, 82_{10} = 19_{73}, and sure enough, 1^2 + 9^2 = 82.

Since each number involved in a loop has at most three digits, we can think of them as coordinates in a 3d space; I wonder what the trajectories of the loops would look like! Someone should do this. A data file containing all loops up to base 150 can be found here (note that after base 61 I just start writing the numbers in base 10 again).

The program I used to search can be found here. I think my program is fairly efficient but it could probably be sped up in various ways to search much farther.

Posted in arithmetic, computation, proof | Tagged , , , , | 7 Comments