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 is a companion discussion topic for the original entry at https://verificationgentleman.netlify.app/2015/04/23/draw-this-without-lifting-pencil.html

Getting these to work sometimes feels like an exercise in self-torture. The most elegant constraints are rarely supported by either LRM or the tools. Even so, every time you do one of these, I always try to come up with my own solution. :slight_smile:

I rarely (never? :slight_smile: ) come up with something better, but I think this time I got an elegant one…

  • We can represent required edges in a matrix m_edges[v1][v2], where m_edges[v1][v2] == 1 if there’s an edge between v1 and v2.

  • We can represent the drawing path using r_vertex[EDGES] array, where pencil starts on r_vertex[0], moves to r_vertex[1], etc.

  • Then, the constraint is to say that for each r_vertex[i], r_vertex[i-1] pair, we must have m_edges[r_vertex[i]][r_vertex[i-1]]==1.

  • The only thing missing now is the uniqueness. This is where I use a 3-D matrix r_edges[v1][v2][i] to represent whether step ‘i’ has drawn edge v1-v2 or not. With that available, we can then say that for each m_edges[v1][v2] == 1, we must have a one-hot {r_edges[v1][v2], r_edges[v2][v1]} (accounting for either direction).

Code: (it’s hard to read, blogger doesn’t allow code or pre tags in comments)

class drawer#(VERTICES=5,EDGES=8);

bit[VERTICES-1:0][VERTICES-1:0] m_edges;
rand byte unsigned r_vertex[EDGES:0];
rand bit[VERTICES-1:0][VERTICES-1:0][EDGES:0] r_edges;

constraint c_edges {
foreach(r_edges[v1, v2, i]) {
r_vertex[i] < VERTICES;
(i > 0) && (r_vertex[i] == v2) && (r_vertex[i-1] == v1) →
r_edges[v1][v2][i-1] == 1 &&
m_edges[v1][v2] | m_edges[v2][v1] == 1;

m_edges[v1][v2] → $onehot({r_edges[v1][v2], r_edges[v2][v1]});
}
}
endclass

This works with VCS and Questa. VCS is a bit slow at it… It speeds up quite a bit if we explicitly set r_edges to 0 when they are not drawn on, but I was going for the least amount of constraint code :).

I think Incisive still doesn't support $onehot in a constraint, but one could write a function to replace it.

Self-torture is probably a bit strong for it, but patience for sure. I wanted to dabble with using an adjacency matrix too for the solution, but I didn’t want to go too deep into graph theory. Your solution is anyway pretty cool. It’s interesting to see that one little extra constraint can speed up some solvers.

Regarding $onehot, I had the exact same problem for N-Queens. I’d avoid it since as you say it’s not supported by all sims, but a viable replacement is sum(). A handwritten function would create a unidirectional constraint and that would change the solution space. To use sum(), though we need to work with arrays of bits instead of vectors.

I have originally tried to use a 3-D array with .sum(), but managed to crash 2 of 3 simulators, with third complaining that it didn’t support it yet. (That’s probably where my self-torture comment came from :slight_smile: ). So, that sent me the way of the 3-D vector instead.

Using a onehot() custom function would indeed change the solve order, but since it’s essentially being used to “check” the answer at the end, it would still produce the correct answer here.