Fun and Games with CRV: Einstein's Puzzle (Revisited)

Two weeks ago, Aurelian from AMIQ published a post on how to solve the so-called Einstein's puzzle using e. At the end, he challenged us readers to try and improve on his solution. Not being one to shy away, I rolled up my sleeves and got to work.

He started out by defining a struct to hold the information about a resident:

<'
struct resident {
  nationality : nationality_t;
  house_color : house_color_t;
  cigarette : cigarette_t;
  pet : pet_t;
  drink : drink_t;
};
'>

He gave up on this idea after he tried to constrain the residents to have unique nationalities, house colors, etc. Here's what he tried:

<'
struct neighborhood {
  keep residents.nationality.is_a_permutation(all_values(nationality_t));
  // ...
};
'>

This looks reasonable, right? Why didn't it work then? That's because even though residents.nationality returns a list of all residents' nationalities, it isn't generative. I didn't find anything normative in the Language Reference or the Generation User Guide that explicitly states this, but this seems to be the case. The proper way of ensuring all nationalities are unique is to use the all_different(...) pseudo-method:

<'
struct neighborhood {
  keep residents.all_different(it.nationality);
  // ...
};
'>

Now that we've got our infrastructure set up, it's time to start converting the 15 facts into code. There are three types of facts given to us. The first type only involves individual residents. For example, we know that the one living in the red house is English. This can be represented as a constraint inside the resident class itself:

<'
extend resident {
  keep nationality == ENGLISH => house_color == RED; // #1
};
'>

There are seven more such constraints, but I won't show them here, since they are very similar to this one. You can find the complete code on SourceForge.

The second type of fact we know about our residents describes a characteristic of the resident living in a particular house. For example, we know that the resident in the first house is Norwegian. This kind of constraint needs to be added to the neighborhood:

<'
extend neighborhood {
  keep residents[0].nationality == NORWEGIAN; // #9
};
'>

The third type of fact gives hints about residents in relation to their neighbors. For example, we know that the green house is located to the left of the white house. Here we need to loop over all elements of the list. Per definition, the green house can't be the last one in the list, because then it wouldn't be located to the left of anything:

<'
extend neighborhood {
  // #4
  keep for each (resident) in residents {
    resident.house_color == GREEN =>
      index < 4 and residents[index+1].house_color == WHITE;
  };
};
'>

The fact that the Blend smoker lives next to the cat owner is a bit more involved, but it follows the same principle. This means that the Blend smoker is either located to the left (which is the same situation as before) or is located to the right, in which case the respective house can't be the first one:

<'
extend neighborhood {
  // #10
  keep for each (resident) in residents {
    resident.cigarette == BLEND =>
      index < 4 and residents[index+1].pet == CAT or
        index > 0 and residents[index-1].pet == CAT;
  };
};
'>

Since we have three more such constraints to write, we could save ourselves some typing by defining a macro:

<'
define <neighbors'statement> "<first'exp> neighbors <second'exp>" as {
  extend neighborhood {
    keep for each (resident) in residents {
      resident.<first'exp> =>
        index < 4 and residents[index+1].<second'exp> or
          index > 0 and residents[index-1].<second'exp>;
    };
  };
};
'>

The macro "call" would look like this:

<'
cigarette == BLEND neighbors pet == CAT; // #10
'>

With these three types of constraints we can model all fifteen facts and solve the puzzle. I was pretty surprised that it worked the first time and gave the right solution - the German keeps the fish. When I solved the zebra puzzle in SystemVerilog (which is essentially the same puzzle as this one, just with slightly different facts about the residents) I ran into problems because I used the implication operator. Basically, saying that the English resident lives in the red house doesn't just mean that nationality == ENGLISH => house_color == RED, but that at the same time house_color == RED => nationality == ENGLISH. There isn't any equivalence operator (also called double implication) in e, but this can be expressed using the equality operator, "==":

<'
extend resident {
  keep (nationality == ENGLISH) == (house_color == RED); // #1
};
'>

I've shown you my solution. Now it's time to pass the baton to you and challenge you to improve it even more.

Fun and Games with CRV: Draw This Without Lifting Your Pencil

It's time for another installment in the "Fun and Games with CRV" series. I love doing these posts because there's something very engaging in modeling all sorts of problems as constraints. This time we're going to look at how to draw a barn without lifting our pencil from the paper and without doubling back. This wikiHow post shows us two ways how we could do that. Now lets see if we can write a solver that can find either of these solutions.

This problem is different from the other puzzle we've looked at before because it has a "time" component. We make moves one after the other and the order in which we make them limits what we can do in the next step. We know exactly how many moves we need to make; this is the number of edges the drawing has. This makes it easier to model, in comparison to more difficult problems where the number of steps is unknown.

While we are looking at how to draw a barn, this kind of puzzle is pretty widespread. Why not implement a more generic solver that can draw any type of figure? We can do this by splitting the solver part (the constraints) from the actual drawing we want to make. Such a drawing is merely a collection of edges, which connect two vertices each. These edges and vertices form a graph and what we want is to traverse it, by taking each edge exactly once. While for the drawing itself the direction of the edges doesn't matter (which is the start or the end vertex), it is important for how we draw the figure. We'll see how this impacts the solver later.

We'll encapsulate the task of modeling such a graph and the constraints needed to traverse it inside an own class. This drawer class (not the best of names, I admit) will provide a protected method that subclasses can call to define the edges of the drawing:

virtual class drawer;
  typedef struct {
    rand vertex_t v1;
    rand vertex_t v2;
  } edge_t;

  protected function void add_edge(vertex_t vertex1, vertex_t vertex2);
    // ...
  endfunction

  // ...
endclass

My first try was to store all of the edges inside an array and add a constraint to try and randomly select one from the list:

virtual class drawer;
  local edge_t edges[$];
  local edge_t dummy_edge;

  constraint choose_existing_edges {
    dummy_edge inside { edges };
  }
endclass

This would have been too easy and probably have made for too short a post. "Fortunately", the SystemVerilog LRM doesn't allow this kind of construct, restricting us to using only singular types with the inside operator (integers, bit vectors, enums, etc.). We'll need to store the connected vertices in some other way if we want to be able to solve this problem. The best way (I could think of) is an associative array of queues indexed by the vertex and containing a list of all other vertices it's connected to directly via edges:

virtual class drawer;
  typedef int unsigned vertex_t;
  typedef vertex_t connections_t[$];

  local connections_t connections[vertex_t];
endclass

Let's look at an example:

In the drawing above, this is what the connections matrix would contain:

1 : { 2, 3, 4 }
2 : { 1 }
3 : { 1 }
4 : { 1, 5 }
5 : { 4 }

We can add to this data structure from the add_edge(...) function:

virtual class drawer;
  protected function void add_edge(vertex_t vertex1, vertex_t vertex2);
    if (connections.exists(vertex1) && vertex2 inside { connections[vertex1] })
      $fatal(0, "Connection %0d -> %0d already exists", vertex1, vertex2);

    connect_vertices(vertex1, vertex2);
    connect_vertices(vertex2, vertex1);

    begin
      edge_t e;
      e.v1 = vertex1;
      e.v2 = vertex2;
      edges.push_back(e);
    end
  endfunction


  local function void connect_vertices(vertex_t src, vertex_t dest);
    if (connections.exists(src))
      connections[src].push_back(dest);
    else
      connections[src] = '{ dest };
  endfunction
endclass

The connect_vertices(...) function handles updating the array of connections. Even though the edges can't be used in constraints directly, we can still store them. The number of edges we add will be the number of steps we need to draw.

It's also a good idea to store a list of all the vertices we have in our drawing. This list we could easily extract from the connections array by taking all of its keys:

virtual class drawer;
  local vertex_t vertices[$];

  function void pre_randomize();
    vertex_t v;
    void'(connections.first(v));
    do
      vertices.push_back(v);
    while (connections.next(v));
  endfunction
endclass

At this point, it makes sense to try again and write a constraint that can select an edge from the ones we've added to the list. I wanted to try something fancy here:

virtual class drawer;
  constraint choose_existing_edge {
    dummy_edge.v1 inside { vertices } &&
    dummy_edge.v2 inside { connections[dummy_edge.v1] };
  }
endclass

The idea was to choose the first vertex at random. The second vertex we could then choose from the list of vertices connected to the first one. In theory, this is great, but in practice, this constraint doesn't work because the index we are using for connections (dummy_edge.v1) is a random variable itself and this doesn't seem to be allowed. I'm not entirely sure if this is a simulator limitation or if the LRM forbids it.

We shouldn't give up on the idea just yet. With a bit of massaging, we can get it to compile. In the second constraint expression we can just loop over all entries inside connections and stop when we've reached the one corresponding to our chosen "starting" vertex:

virtual class drawer;
  constraint choose_existing_edges {
    dummy_edge.v1 inside { vertices };

    foreach (connections[v])
      if (dummy_edge.v1 == v)
        dummy_edge.v2 inside { connections[v] };
  }
endclass

It's a little more code, but it does the job perfectly. Now we have a solid base to really start building our solver. We'll need to keep track of what edges we've already drawn and when. We'll store them in an array, where index 0 will be the first edge we drawn, index 1 the second and so on:

virtual class drawer;
  local rand edge_t edge_being_drawn[];
endclass

The first constraint we'll write is that each edge we draw actually exists in the drawing. We've already written such a constraint for one edge, so we'll just extend it to cover all of them:

virtual class drawer;
  constraint choose_existing_edges {
    foreach (edge_being_drawn[i])
      edge_being_drawn[i].v1 inside { vertices };

    foreach (edge_being_drawn[i])
      foreach (connections[v])
        if (edge_being_drawn[i].v1 == v)
          edge_being_drawn[i].v2 inside { connections[v] };
  }
endclass

Just choosing edges that exist inside the figure isn't enough. We have to make sure that the edges are unique. Here I tried some more fanciness than the language affords. This constraint, though short and sweet, also doesn't compile:

virtual class drawer;
  constraint choose_unique_edges {
    unique { edge_being_drawn };
  }
endclass

As with the inside operator, the unique operator also only works on integral types. I tried to outsmart the compiler by declaring the struct as packed, but then it can't be declared as rand so that won't get us anywhere. As before, we're just going to have to throw some more code at the problem:

virtual class drawer;
  constraint choose_unique_edges {
    foreach (edge_being_drawn[i])
      foreach (edge_being_drawn[j])
        if (i != j)
          !(edge_being_drawn[i].v1 == edge_being_drawn[j].v1 &&
            edge_being_drawn[i].v2 == edge_being_drawn[j].v2);

    foreach (edge_being_drawn[i])
      foreach (edge_being_drawn[j])
        if (i != j)
          !(edge_being_drawn[i].v1 == edge_being_drawn[j].v2 &&
            edge_being_drawn[i].v2 == edge_being_drawn[j].v1);
  }
endclass

As we already know from the previous post on array constraints we can replace a unique constraint with a double foreach. It's not enough to say that the starting or ending vertices be different. We also need to make sure that we're not backtracking. Going from vertex 1 to vertex 3 is the same edge when going from vertex 3 to vertex 1 (it's just the direction that's different).

One more constraint is missing to make the solution complete. We have to make sure that when going from one edge to another, the end vertex of the previous edge is the start vertex of the current edge. If we don't, then we're lifting our pencil from the paper. This is very easy to express:

virtual class drawer;
  constraint choose_connected_edges {
    foreach (edge_being_drawn[i])
      if (i > 0)
        edge_being_drawn[i].v1 == edge_being_drawn[i - 1].v2;
  }
endclass

Let's test it out by trying to draw a barn. Here's how the vertices are numbered:

The barn_drawer class only needs to define the edges using the add_edge(...) function:

class barn_drawer extends drawer;
  function new();
    add_edge(0, 1);
    add_edge(0, 2);
    add_edge(1, 2);
    add_edge(1, 3);
    add_edge(1, 4);
    add_edge(2, 3);
    add_edge(2, 4);
    add_edge(3, 4);
  endfunction
endclass

We just need to randomize an instance of barn_drawer and we should get the instructions we need to solve our puzzle. Sadly, things are never this easy. Immediately after putting all constraints together I got a constraint violation. After looking at the "choose" constraints over and over and hitting my head on the table, some time later I found what the problem was; it wasn't in my code. As in the first installment of the series, when solving Sudoku, a simulator bug reared its ugly head, but this time it wasn't as easy to pinpoint. I should probably consider moonlighting as a QA for an EDA company since I seem to draw such issues to me. Getting to the point, if we add this slight modification to the choose_unique_edges constraint it's going to make the clouds go away:

virtual class drawer;
  constraint choose_unique_edges {
    // ...

    foreach (edge_being_drawn[i])
      foreach (edge_being_drawn[j])
        // (Very) Possible bug in simulator
        if (i == j - 1)
          edge_being_drawn[i].v1 != edge_being_drawn[j].v2;
        else if (j == i - 1)
          edge_being_drawn[j].v1 != edge_being_drawn[i].v2;
        else

        // This condition should be enough by itself.
        if (i != j)
          !(edge_being_drawn[i].v1 == edge_being_drawn[j].v2 &&
            edge_being_drawn[i].v2 == edge_being_drawn[j].v1);
  }
endclass

And there we have it! Now we can solve any such "draw this without lifting your pencil" puzzle. We've also learned a bit more about the limitations of the SystemVerilog constraint language. I can't help thinking that the whole thing would have been much cleaner in e. I might try it out in the future just to see. If someone else does it, it would be nice to compare. In the meantime, you can find the code on SourceForge if you want to experiment drawing other figures.

Fun and Games with CRV: The N-Queens Problem

It's been quite a while since we've solved the zebra puzzle using SystemVerilog. In this post we'll look at another oldie, but a goldie called the n-queens problem. This problem first appeared in a more specific form as the eight queens puzzle, first published in 1848. In this puzzle, the player is asked to place eight queens on a chessboard in such a way that they don't threaten each other. It has fascinated mathematicians (including the great Carl Friedrich Gauss) ever since to find solutions to it. Edsger Dijkstra used it to illustrate the power of backtracking. More recently, Team Specman also solved this problem using constraint programming and published it in this post. The e code they employed is short and sweet, but it's not so easy to digest, though.

In pure "re-inventing the wheel" fashion that we engineers love, I'm going to do my own solution, but in SystemVerilog.

We'll model the chess board as an n by n array of bit values. A 1 will mean that a queen is present on that square, while a 0 will indicate that the square is empty.

class n_queens_solver #(int unsigned n = 8);
  rand bit board[n][n];
  
  // ...
endclass

Modeling the board like this will (hopefully) make it easier to solve the puzzle in a way closer to how a human might solve it on a real board. We'll want to set constraints on the positions of the queens based on the their ranges of motion. Concretely, we'll want to say that only one queen can occupy a row, column or diagonal.

Before we start, however, we'll want to make sure the language supports a couple of things. First, we want to make sure that we can constrain a vector (a one-dimensional array) to contain only a single 1. We can do this using the classical double-for approach:

class singular_on_line #(int unsigned len = 8);
  rand bit line[len];
  
  constraint double_for {
    // the '1' can only be in one place
    foreach (line[i])
      foreach (line[j])
        (i != j) -> ((line[i] == 1) -> (line[j] == 0));
      
    // the '1' must exist in the array
    1 inside { line };
  }
endclass

The two foreach loops say that if one location of the vector contains the 1, then no other location can hold it. This doesn't ensure, however, that the 1 exists inside the vector, hence the need for the inside constraint. This approach works, but it's pretty long and verbose.

Luckily, starting with the 2012 version of the standard we can use array reduction methods in constraints. A good candidate for this is the sum() method. We want the sum of all elements in the array to be 1:

class singular_on_line #(int unsigned len = 8);
  constraint sum {
    line.sum() == 1;
  }
endclass

When testing this constraint, something strange happens. In most cases we won't get a single 1 inside the array. We will, however, always get an odd number of 1s. What's happening here? Because the elements of line are bits, the result is also interpreted as a one bit value, leading to truncation when adding up all the elements. The proper way to do it is to use an explicit cast to force summation to an integer value:

class singular_on_line #(int unsigned len = 8);
  constraint sum {
    line.sum() with ( int'(item) ) == 1;
  }
endclass

It's a shame we can't use the array locator methods inside constraints, as that would have made everything even more expressive. Maybe in a future release of the standard...

The second thing we should look at before diving into the full problem is how to construct the diagonals. This is going to be a bit more funky, since not all diagonals have the same length. For an array of n x n elements we'll have 2*n - 1 diagonals. Since the diagonals are of different lengths, it makes the most sense to store them as dynamic arrays:

class array_of_diags #(int unsigned n = 8);
  rand bit[2:0] array[n][n];
  
  rand bit[2:0] diags[n*2 - 1][];
endclass

We need to establish a convention on how we'll number the diagonals. Let's look at a 3 x 3 array:

+-------+-------+-------+
|       |       |       |
| (0,0) | (0,1) | (0,2) |
|       |       |       |
+-------+-------+-------+
|       |       |       |
| (1,0) | (1,1) | (1,2) |
|       |       |       |
+-------+-------+-------+
|       |       |       |
| (2,0) | (2,1) | (2,2) |
|       |       |       |
+-------+-------+-------+

We'll number the diagonals going horizontally from left to right and vertically from top to bottom. We'll insert elements going also from left to right, but from bottom to top. This is a bit difficult to explain in words (and I'm not good enough yet with HTML to draw it for you), but it should be easy to understand by example. In our case, the diagonals will contain the following elements:

• diags[0] = { (0,0) }
• diags[1] = { (1,0), (0,1) }
• diags[2] = { (2,0), (1,1), (0,2) }
• diags[3] = { (2,1), (1,2) }
• diags[4] = { (2,2) }

With a little observation and mathematical induction, we can figure out that the constraint to create the diagonals looks like this:

class array_of_diags #(int unsigned n = 8);
  constraint create_diags {
    foreach (diags[i,j])
      if (i < n)
        diags[i][j] == array[i - j][j];
      else
        diags[i][j] == array[(n - 1) - j][i + j - (n - 1)];
  }
endclass

What's very important, though, when working with constraints on dynamic arrays is to make sure that their sizes are set up correctly. We can easily do this inside the pre_randomize() function:

class array_of_diags #(int unsigned n = 8);
  function void pre_randomize();
    foreach (diags[i])
      diags[i] = new[get_len_of_diag(i)];
  endfunction
  
  
  function int unsigned get_len_of_diag(int unsigned idx);
    if (idx < n)
      return idx + 1;
    
    return 2*n - (idx + 1);
  endfunction
endclass

The formula to get the length of a diagonal can be easily worked out by observation. In fact, that's how I figured out most of these array constraints. I just took an example array and tried to relate different things to an element's row/column index and the size of the array.

Just to be on the safe side, I've also made sure that any constraints we apply on the diagonals' elements will also propagate back to the initial array we've constructed them from. We don't want to get any issues with unidirectional constraints. For brevity, I won't show that code here.

With these topics sorted out we can get started. We'll use some helper variables to store our rows, columns and diagonals:

class n_queens_solver #(int unsigned n = 8);
  rand bit rows[n][n];
  rand bit cols[n][n];
  rand bit main_diags[2*n - 1][];
  rand bit anti_diags[2*n - 1][];
endclass

Unfortunately, SystemVerilog doesn't have the concept of pointers, so these extra arrays will use some extra memory, but this shouldn't decrease generation performance. Don't hold me to this last statement, but this is a hunch of mine, since the constraints we use to relate these variables to the board don't increase our randomization state space (they are 1:1 mappings).

It's not really necessary to use a separate variable for the rows (as rows are easily indexable from an array), but it makes the code more expressive (plus, I'm a bit of a sucker for symmetry and it would feel unbalanced to treat the rows differently). Here's the constraint to create the rows:

class n_queens_solver #(int unsigned n = 8);
  constraint create_rows {
    foreach (rows[i, j])
      rows[i][j] == board[i][j];
  }
endclass

And here's how to create the columns:

class n_queens_solver #(int unsigned n = 8);
  constraint create_cols {
    foreach (cols[i, j])
      cols[i][j] == board[j][i];
  }
endclass

The main diagonals are the diagonals that sweep the array from left to right and from top to bottom:

Here's the constraint to create them:

class n_queens_solver #(int unsigned n = 8);
  constraint create_main_diags {
    foreach (main_diags[i,j])
      if (i < n)
        main_diags[i][j] == board[j][(n - 1) - i + j];
      else
        main_diags[i][j] == board[i - (n - 1) + j][j];
  }
endclass

The anti diagonals sweep the array from right to left and from top to bottom:

And here's the constraint to create them too:

class n_queens_solver #(int unsigned n = 8);
  constraint create_anti_diags {
    foreach (anti_diags[i,j])
      if (i < n)
        anti_diags[i][j] == board[i - j][j];
      else
        anti_diags[i][j] == board[(n - 1) - j][i + j - (n - 1)];
  }
endclass

I would love to see a concept where these fields can get created without occupying extra memory, since they're basically just copies of other fields. Until then, we'll have to make the most of what we have.

After creating the lines of our chess board, it's time to finally start writing the constraints to solve the puzzle. Since a queen has an unlimited horizontal range of motion, it must occupy an entire row by itself:

class n_queens_solver #(int unsigned n = 8);
  constraint singular_on_row {
    foreach (rows[i])
      rows[i].sum() with ( int'(item) ) == 1;
  }
endclass

Similarly, a queen must occupy an entire column by itself:

class n_queens_solver #(int unsigned n = 8);
  constraint singular_on_col {
    foreach (cols[i])
      cols[i].sum() with ( int'(item) ) == 1;
  }
endclass

Queens also have unlimited range on any diagonals (both main and anti) they occupy. This means that no two queens can occupy the same diagonal. My first idea was to put a constraint similar to the ones above on each diagonal:

class n_queens_solver #(int unsigned n = 8);
  constraint singular_on_main_diag {
    foreach (main_diags[i])
      main_diags[i].sum() with ( int'(item) ) == 1;
  }
endclass

After adding this constraint the constraint solver started failing. I was scratching my head in wonder and was just about ready to cry foul on the solver, when I realized that I had been wrong all along. It's true that there can only be one queen on a certain diagonal, but the key thing to note is that there doesn't have to be a queen on each diagonal. Of course, this makes sense, since as we saw above there are 2*n - 1 diagonals and we can only place n queens.

What we can do instead is only constrain those diagonals that cross a position where a queen is located:

class n_queens_solver #(int unsigned n = 8);  
  constraint singular_on_main_diag {
    foreach (cols[j,i])
      if (cols[j][i] == 1)
        main_diags[(n - 1) - j + i].sum() with ( int'(item) ) == 1;
  }
endclass

Adding a similar constraint to the anti diagonals will solve the puzzle. The constraint doesn't look very nice, though. It's looks pretty complicated and it won't be easy to understand (even I'm having problems it while writing this post). It seems to me that we're doing too much work for the solver!

As we saw above, we can either have one queen or no queens on a diagonal. Why not write that as a constraint? This leads to much less code:

class n_queens_solver #(int unsigned n = 8);
  constraint singular_on_main_diag {
    foreach (main_diags[i])
      main_diags[i].sum() with ( int'(item) ) inside {0, 1};
  }
  
  constraint singular_on_anti_diag {
    foreach (anti_diags[i])
      anti_diags[i].sum() with ( int'(item) ) inside {0, 1};
  }
endclass

And that's all there is to it! We've written a lot of code just to set up our board's lines, but the constraints we wrote on them are pretty straightforward and easy to understand.

I've tried running the solution on my modest machine and it works pretty fast for an n equal to 8. It's a bit slower for 9 and even slower for 10. It kind of runs out of steam for greater values, as Vitaly predicted in his post. Intelligen might be faster for this particular problem (I haven't tried it out myself), but whether it's faster in all practical situations for usual constraints I can't say. Cadence might be stretching the truth here, or rather put its best foot forward, for marketing purposes. I mean, how often do you write this style of constraints in production code?

You can find the full code on SourceForge. Feel free to download it and see how large an n you can handle.

Also, while I was writing the post I had the idea that instead of using vectors for the rows, columns and diagonals, maybe we could use packed arrays. We might be able to set $onehot constraints on them, though I'm not sure if this is supported. If any of you try it out, please share your experience in the comments section.

Fun and Games with CRV: The Zebra Puzzle

The Zebra Puzzle is a classic logic puzzle, first published by Life International in 1962. Older versions of it exist and it is also sometimes called Einstein's puzzle. According to "Of Camels and Committees" by Tom Fitzpatrick and Dave Rich, it was used in the early days of constrained random verification (CRV) to show off EDA tools at marketing events.

The puzzle consists of a set of fifteen statements:

There are five houses. 
The Englishman lives in the red house. 
The Spaniard owns the dog. 
Coffee is drunk in the green house. 
The Ukrainian drinks tea. 
The green house is immediately to the right of the ivory house. 
The Old Gold smoker owns snails. 
Kools are smoked in the yellow house. 
Milk is drunk in the middle house. 
The Norwegian lives in the first house. 
The man who smokes Chesterfields lives in the house next to the man with the fox. 
Kools are smoked in the house next to the house where the horse is kept. 
The Lucky Strike smoker drinks orange juice. 
The Japanese smokes Parliaments. 
The Norwegian lives next to the blue house.

(Life International, 1962)

Based on these statements, the reader is asked to deduce who drinks water and who owns the zebra.

Deductive reasoning makes my head hurt, so I want to have the computer solve it for me. As with Sudoku, we don't want to build an algorithm that finds the solution. This is exactly the kind of problem constraint programming is perfect for: expressing logical relations between variables. Let's dive right in!

The first step is to formalize the problem. We know that the houses are of different colors, contain people of specific nationalities that drink some things, smoke some cigarette brands and own some pets, again all different. We will model all of these as enumerations.

First let's handle the house colors:

typedef enum { RED, GREEN, IVORY, YELLOW, BLUE } color_e;

Second, nationality is mentioned:

typedef enum { ENGLISH, SPANISH, UKRANIAN, NORWEGIAN, JAPANESE } nationality_e;

Third, here are the pets:

typedef enum { DOG, SNAILS, FOX, HORSE, ZEBRA } pet_e;

Fourth, this is what the inhabitants like to drink:

typedef enum { COFFEE, TEA, MILK, ORANGE_JUICE, WATER } drink_e;

And fifth, this is what they like to smoke:

typedef enum { OLD_GOLD, KOOL, CHESTERFIELD, LUCKY_STRIKE, PARLIAMENT } cigarettes_e;

The easiest way to model the houses is by using a struct:

typedef struct {
  rand color_e       color;
  rand nationality_e nationality;
  rand pet_e         pet;
  rand drink_e       drink;
  rand cigarettes_e  cigarettes;
} house_t;

The second step is to write the starting statements as constraints. We can't know on which instance of the house to apply a specific statement; this is what we want to find out. The statements must apply to all houses (with the exception of a few that apply to a specific house), which means that for the most part we will write foreach constraints.

Statement 1 just says that there are five houses. This isn't a constraint per se, but more of a modeling topic. We model this by declaring our neighborhood as a vector of houses that contains five elements:

class zebra_puzzle_solver;
  rand house_t house[5];
  
  // ...
endclass

Statement 2 says that the Englishman lives in the red house:

constraint statement2_c {
  foreach (house[i])
    house[i].nationality == ENGLISH -> house[i].color == RED;
}

From statement 3 we learn that the Spaniard owns the dog:

constraint statement3_c {
  foreach (house[i])
    house[i].nationality == SPANISH -> house[i].pet == DOG;
}

Statement 4 tells us that the person who drinks coffee lives in the green house:

constraint statement4_c {
  foreach (house[i])
    house[i].drink == COFFEE -> house[i].color == GREEN;
}

We know from statement 5 that the Ukrainian drinks tea:

constraint statement5_c {
  foreach (house[i])
    house[i].nationality == UKRANIAN -> house[i].drink == TEA;
}

Statement 6 is a bit tricky. It tells us that the green house is immediately to the right of the ivory house. This means that we have to take care in our foreach constraint that we don't end up outside the neighborhood (i.e. access a non-existing location in our vector):

constraint statement6_c {
  foreach (house[i])
    if (i < 4)  // make sure we don't go out of bounds
      house[i].color == IVORY -> house[i+1].color == GREEN;
}

Moving on, statement 7 informs us that the Old Gold smoker owns snails:

constraint statement7_c {
  foreach (house[i])
    house[i].cigarettes == OLD_GOLD -> house[i].pet == SNAILS;
}

At the same time, as per statement 8, the Kools smoker lives in the yellow house:

constraint statement8_c {
  foreach (house[i])
    house[i].cigarettes == KOOL -> house[i].color == YELLOW;
}

Statement 9 only applies to the middle house and says that milk is drunk there:

constraint statement9_c {
  house[2].drink == MILK; // no. 2 is the middle house
}

Statement 10 also only applies to only one house, the first one, and tells us that the Norwegian lives there:

constraint statement10_c {
  house[0].nationality == NORWEGIAN;  // no. 0 is the first house
}

Statement 11 becomes tricky again. From it we know that the Chesterfield smoker lives next to the fox owner. "Next to" means either to the left or to the right. As with statement 6, we have to make sure we don't fall off of the neighborhood map. We have three cases to consider. If he lives in the first house (the leftmost) then this means his neighbor to the right owns the fox. Likewise, if he lives in the last house (the rightmost), this means that his neighbor to the left owns the fox. However, if he lives in one of the middle houses, then either one of his neighbors could potentially own the fox. Expressed as constraints, this would look like this:

constraint statement11_c {
  house[0].cigarettes == CHESTERFIELD -> house[1].pet == FOX;
  house[4].cigarettes == CHESTERFIELD -> house[3].pet == FOX;
  
  foreach (house[i])
    if (i > 0 && i < 4)
      house[i].cigarettes == CHESTERFIELD ->
        (house[i-1].pet == FOX) || house[i+1].pet == FOX);
}

Statement 12 is similar to the previous one, but it tells us that the Kools smoker lives next to the horse owner. The constraint looks very much like the one before:

constraint statement12_c {
  house[0].cigarettes == KOOL -> house[1].pet == HORSE;
  house[4].cigarettes == KOOL -> house[3].pet == HORSE;
  
  foreach (house[i])
    if (i > 0 && i < 4)
      house[i].cigarettes == KOOL ->
        (house[i-1].pet == HORSE) || house[i+1].pet == HORSE);
}

Statement 13 is simple again and informs us that the Lucky Strike smoker drinks orange juice:

constraint statement13_c {
  foreach (house[i])
    house[i].cigarettes == LUCKY_STRIKE -> house[i].drink == ORANGE_JUICE;
}

Similarly, from statement 14 we find out that the Japanese smokes Parliament:

constraint statement14_c {
  foreach (house[i])
    house[i].nationality == JAPANESE -> house[i].cigarettes == PARLIAMENT;
}

Statement 15 is again more involved, finally telling us that the Norwegian lives next to the blue house. We could type a bit less here (because we know the Norwegian lives in the first house) and directly say that the second house is blue, but I want the constraint solver to work hard for its money. Let's just write the constraint as we did for statements 11 and 12:

constraint statement15_c {
  house[0].nationality == NORWEGIAN -> house[1].color == BLUE;
  house[4].nationality == NORWEGIAN -> house[3].color == BLUE;
  
  foreach (house[i])
    if (i > 0 && i < 4)
      house[i].nationality == NORWEGIAN ->
        (house[i-1].color == BLUE) || house[i+1].color == BLUE);
}

Ideally, the third step should be to just run our code and find the solution, but as always nothing works right on the first try. I kept getting some very weird results at first, that were completely off. The reason for this is that we used implication constraints. Saying that being English implies you live in the red house is not enough. We don't know the order in which fields are assigned by the solver, so we also need to say that if you live in the red house, then you are English. Luckily, SystemVerilog provides us the equivalence operator <->. Here's how the constraint for statement 2 should really look like:

constraint statement2_c {
  foreach (house[i])
    house[i].nationality == ENGLISH <-> house[i].color == RED;
}

For brevity I won't show all of the fixed constraints here.

Even with the equivalence constraints in place, I got three Japanese and two Norwegians in my neighborhood. I looked at each of the constraints and they all applied (though some vacuously). The last one, however (the one I chose to write long), didn't, but only because the compiler had no problem with me saying that the Norwegian lives next to the house with the color fox (you won't see it in the code I posted as I already fixed that).  Surprisingly, there was no error, no warning, no nothing, even though such a conversion is illegal. Let this be a lesson to us for the future: some simulators are a bit more relaxed with their interpretation of the SystemVerilog standard and we need to make sure to enforce strict LRM compliance, otherwise we're going to have a bad time debugging implicit type conversions.

Even after fixing the foxy house, I still got a neighborhood full of Norwegians with all blue houses. Three of them smoked Chesterfields, while the other two liked Old Gold (and had snails as well, of course). Most drank milk and only one drank water. Also, the middle guy had the zebra. You get the idea, something was still missing. Well, the wording of the puzzle is important. It always said "the Norwegian..." or "the Lucky Strike smoker..." which means there is only one Norwegian and only one Lucky Strike smoker. The original article in Life International adds this fact as a clarification: "[It] must be added that each of the five houses is painted a different color, and their inhabitants are of different national extractions, own different pets, drink different beverages and smoke different brands of American cigarets [sic]."

To reflect this, we just need to add a uniqueness constraint. Unfortunately, because constraint operands have to be of integral types, we can't just say that the houses are unique. We have to declare auxiliary lists for nationalities, pets, etc. and constrain these to be unique. In e we could have accessed these directly, without the need for extra fields, but here is how it looks like in SystemVerilog:

local rand color_e       color[5];
local rand nationality_e nationality[5];
local rand pet_e         pet[5];
local rand drink_e       drink[5];
local rand cigarettes_e  cigarettes[5];

constraint create_sublists_c {
  foreach (house[i]) (
    color[i] == house[i].color &&
    nationality[i] == house[i].nationality &&
    pet[i] == house[i].pet &&
    drink[i] == house[i].drink &&
    cigarettes[i] == house[i].cigarettes
  ); 
}

constraint all_unique_c {
  unique { color };
  unique { nationality };
  unique { pet };
  unique { drink };
  unique { cigarettes };
}

Even with the uniqueness constraint in place, we still get a contradiction error. This one took me a bit to figure out. The problem is with our "complicated" constraints (the ones for statements 11, 12 and 15). Here is how the constraint for statement 11 looks after swapping implication for equivalence, in particular the constraint for the middle houses:

constraint statement11_c {
  foreach (house[i])
    if (i > 0 && i < 4)
      house[i].cigarettes == CHESTERFIELD <->
        (house[i-1].pet == FOX) || house[i+1].pet == FOX);
}

The mistake is with respect to the relation between the equivalence and logical operators. Let's take a step back and let me explain what I mean by that. For the case of implication, the following is true:

a -> (b || c) == (a -> b) || (a -> c)

The same is however not true for equivalence:

a <-> (b || c) != (a <-> b) || (a <-> c)

For all of you math enthusiasts, this means that equivalence is not distributive over disjunction. If you write the truth tables you will see that this is the case. What we're interested in is the right hand side of the expression (the neighbor on the left smokes Chesterfields or the neighbor on the right smokes Chesterfields), but what we have implemented is the expression on the left hand side. Now that we know this, we can fix the constraints (shown for statement 11):

constraint statement11_c {
  foreach (house[i])
    if (i > 0 && i < 4)
      (house[i].cigarettes == CHESTERFIELD <-> house[i-1].pet == FOX) ||
      (house[i].cigarettes == CHESTERFIELD <-> house[i+1].pet == FOX);
}

Technically, more correct would have been to say A <-> B xor A <-> C, because the neighbor can only be either on the left or on the right. This might speed things up a bit and might also make it so that uniqueness constraints are not needed. Unfortunately, we can't try this out as there is no logical exclusive "or" operator in SystemVerilog.

After fixing this last thing, everything now works! We find out that the Norwegian drinks water and that the Japanese owns the zebra. Much easier than deductive reasoning...

I hope you enjoyed this post. It was a lot of fun to make and I learned a bit more about the constraint capabilities of SystemVerilog. If you want to play with the solver, you can download it from SourceForge.

Stay tuned for more fun and games with CRV!