Logic puzzles vs ZDDs

I've been addicted to logical puzzles for a long time. Recently, I've become addicted to writing programs to solve addicting logic puzzles.

Years ago I whipped up a dancing links sudoku solver as popularized by Knuth, which converts sudoku instances into exact cover problems. So of course when I learned ZDDs were good at exact cover problems, again from Knuth, I immediately thought of sudokus.

I dreamt of building a ZDD representing all possible (standard) sudokus. I could then fill in some boxes, and from here, I could count the number of solutions, pick one at random uniformly, or weight the solutions with any given scheme and find the maximum or minimum solution, as well as the mean and standard deviation.

I eagerly wrote enough ZDD routines to encode the sudoku constraints. The preliminary results were encouraging: my ZDD enforcing exactly one per box and exactly one per row for each digit required only 20738 nodes. But the column constraints crushed my aspirations. No matter how I sliced it, the ZDD grew too rapidly as more constraints were added.

As a consolation prize, I hoped to at least convert my program into a solver that would rival my earlier program. Unfortunately, although the end result could solve a sudoku, it did so slowly.

Deflated, I sought reassurance by verifying Knuth's results on chessboard tilings. Thankfully my numbers agreed exactly, so I knew my implementation was sufficiently correct and efficient for basic experiments. On the other hand, it also probably means that sudokus are indeed beyond the reach of ZDDs.

I flailed around looking for another excuse to use ZDDs. It didn't take long: nonogram puzzles turn out to be no match for their power.

By the way, I obviously mean human-friendly nonograms, as the general problem is NP-complete; ZDDs aren't that revolutionary! The same applies to other NP-complete puzzles: rather than prove P = NP, my goal is to write an efficient solver for instances meant for humans, and maybe also instances that are just a bit tougher.

I didn't have much time to stress test the nonogram solver, as I rapidly moved on to a Light Up solver. Shortly after I threw together a dominosa solver, and yet more ZDD solvers for other logic puzzles are in the pipeline. I'll release the code soon.

As dominosa puzzles are easily disguised as exact cover problems, I also wrote a dancing links solver. Unsurprisingly, it is much faster; I'm sure specialized recursive search programs outperform ZDDs for the other puzzles too, but ZDDs have some advantages. Firstly, they are easy to write once the infrastructure is in place. Constraints for many logic puzzles are easily expressed in terms of ZDDs. Secondly, even if ZDDs are only practical for smaller instances, they can often answer more questions.

For example, how many dominosa problems are there if we go up to double-nine? How many are there if we then place a few particular dominoes in certain places? What does puzzle number 12345 look like? And so on.

A really fundamental data structure

There are many things I wish my textbooks had taught me. It's often not the fault of the authors: in any field, even the best ideas suffer a lag between discovery and dissemination. However, even accounting for this, it seems I'm always behind the times. Some glaring omissions I belatedly redressed:

• Calculus can be taught rigorously with infinitesimals, following the path traveled by its original developers, unlike the approach using limits and deltas and epsilons.
• Cuckoo hashing gives hash tables with O(1) worst-case lookups and are also space-efficient.
• Bob Jenkin's hash functions for hash tables are better than those many commonly encountered in textbooks.
• Perfect hashes give optimal performance when the keys come from a small set that can be preprocessed beforehand.
• Crit-bit trees perform similarly to hash tables but have some advantages. My favourites: good worst-case running time and lexicographical operations. Apparently they can be used to sort strings faster than quicksort or radix sort.
• AA trees remove the pain from implementing balanced binary trees.

But most of all, I bemoan my ignorance of binary decision diagrams (BDDs). In his Computer Musings lecture, Don Knuth states "it's one of the only really fundamental data structures that came out in the last 25 years". He felt it was so important that he devoted the following lecture to ZDDs, a close relative of BDDs.

Take a map of the USA, and consider the following problems:

1. Suppose you want to visit every state capitol exactly once, traveling on highways. Which route is shortest? Which route is longest? What is the mean and standard deviation of all the routes?
2. Weight the states by any means, for example, by reading their two-letter code as a number in base 36. Then find a set of states such that no two members of the set are adjacent, and the total weight is maximized.
3. There are several ways to colour the map with four colours such that no two adjacent states have the same colour. How do we pick one of these colourings at random (uniformly)?

Or consider these:

4. How many ways can you tile a chessboard using 1x1, 2x1 and 3x1 rectangles? What if we also have pieces that look like 2x2 boxes with one tile missing?
5. List all 5-letter words that remain words after replacing a 'b' with 'o'.

Do you know how to solve these efficiently? If not, you might want to read up on BDDs, particularly Knuth's treatment, which has just hit the presses, and watch his lectures. Using these sources, I took some notes on ZDDs.

Learning about BDDs reminded me of learning about Pólya theory, another simple yet powerful technique which transforms the seemingly impossible into child's play.

Assorted sorts

Let void x(int *p, int *q) be function that swaps its arguments, namely, after execution, *p is equal to the original value of *q and vice versa.

What do the following functions do?

void f(int *m, int *n) {
int *p;
for(p = m; p < n; p -= *p > p[1] ? x(p, p + 1), p != m : -1);
}

void f(int *m, int *n) {
int *p, *q;
for(p = m; p <= n; p++) for(q = p; q <= n; *p > *q ? x(p, q) : 0, q++);
}

void f(int *m, int *n) {
  int i, j, k;
  for(i = 1; (k = i) <= n - m; i++)
    while(k && m[j = k - 1 >> 1] < m[k]) x(m + j, m + k), k = j;
  for(k--; x(m, m + k--), k;) for(i = 0;
      j = 2 * i + 1, k >= (j += k > j && m[j] <= m[j + 1]) && m[j] > m[i];
      x(m + j, m + i), i = j);
}

void f(int *m, int *n) {
int *p, *q, i;
do
for (i = 0, p = q = m, ++q; q <= n; p = q++) *p > *q ? x(p, q), i = 1 : 0;
while(i);
}

void f(int *m, int *n) {
int *p, *q;
for(p = m + 1, q = n; p < q; *p > *m ? x(p, q--) : *p++);
m != n ? *m > *p ? x(m, p) : 0, f(m, --p), f(q, n) : 0;
}

void f(int *m, int *n) {
int *p, *q, i, j;
for(p = m + 1; p <= n; p++, *q = i)
for(i = *p, q = p; q > m && i < (j = *(q - 1)); *q-- = j);
}

void f(int *m, int *n) {
static short s[] = { 1, 4, 10, 23, 57, 132, 301, 701, 1750 };
int *p, *q, i, j, a, b;
for(a = sizeof(s)/sizeof(short) - 1; a && s[a] > n - m; a--);
while(a >= 0) for(p = m + (b = s[a--]); p <= n; p++, *q = i)
for(i = *p, q = p; q > m && i < (j = *(q - b)); *q = j, q -= b);
}

The title is a big hint, but if you're still not sure, experiment with a function by compiling it with the following code, and supply some integers on standard input.

#include <stdio.h>

void f(int *m, int *n);

void x(int *p, int *q) {
  int i = *p;
  *p = *q, *q = i;
}

int main() {
  enum { limit = 8192 };
  int a[limit], *n, *k;
  for(n = a; 1 == scanf("%d", n) && n - a < limit; n++);
  puts("in:");
  for (k = a; k < n; k++) printf(" %d", *k);
  puts("");
  f(a, n - 1);
  puts("out:");
  for (k = a; k < n; k++) printf(" %d", *k);
  puts("");
  return 0;
}

Can you identify each algorithm? The answers are, in some order, bubble sort, gnome sort, insertion sort, selection sort, shell sort, heapsort and quicksort.

The real puzzle is why I bothered. All I can say is you don't have to be a chef to enjoy making spaghetti: see the International Obfuscated C Code Contest.

Notable Notation

Pursuing a graduate degree in computer science at Stanford offered many perks. I benefited from at least one more than some of my colleagues, as I was assigned an office only a few doors away from Don Knuth's.

I'd occasionally catch a glimpse of the legendary computer scientist, for some reason usually donning a bicycle helmet. However, the proximity of his office alone seems to have had an effect: I switched to LaTeX for typesetting. As an undergraduate I loyally used Lout, whose author, Jeff Kingston, had an office near where I worked. In seriousness, it was probably more for practical reasons than out of respect: all my co-authors used LaTeX.

I still have a soft spot for Lout with its clean and comprehensible internals. Compare with the inscrutable black-magic LaTeX style sheets built on top of TeX, which itself is tricky to grasp. However, the TeX equation syntax certainly deserves its status as the lingua franca of mathematicians communicating via email and other plain text mediums.

My workplace is no longer near Knuth or Kingston. Perhaps not entirely coincidentally, I no longer use TeX or Lout. Wanting documentation sources to be as readable as much as possible, I devised a markup language inspired by venerable ASCII typesetting tricks of heavy email users and README authors, such as *asterisks*, _underscores_, and ==Headings==, and wrote a script to translate it to HTML. Luckily I didn't get far before discovering AsciiDoc.

Equation-heavy notes, books, HTML, PDF: AsciiDoc handles them all despite using source files that look like ordinary text documents. Easy to learn, easy to type, and easy on the eyes. Fine-tuning the final layout is difficult, a blessing in disguise as users have solid excuses for ignoring those typesetting nitpicks TeXperts are expected to correct.

But I digress: back to name-dropping Donald E. Knuth. Although he was warm and friendly, I only spoke to him a few times as he was also busy. However, I had many chances to listen to him. Sometimes he'd give a talk in the meeting area outside my door, where I always had a guaranteed seat: I could simply wheel my office chair a few meters.

Regrettably I recall almost nothing. There was a story about how noticing a pattern in table of numbers yielded a PhD thesis; he made it sound so easy. I also vaguely remember a fascinating introduction to coroutines along with an obscure but accessible application: generating certain Gray code sequences. This would describe all I have left from Knuth's talks, but happily, some of his Computer Musings were recorded and are freely available online.

The Notation episode is surprisingly interesting, especially the historical tidbits. The notation for floor and ceiling functions only became standard relatively recently, a brilliant idea that usurped many inferior schemes and rapidly took over the world. Another young fad is to use "lg" for the base 2 logarithm, though now it seems we should use "lb" instead.

The highlight was Iverson's bracket convention: one places an expression within square brackets, and the whole thing evaluates to 1 if the expression is true, and 0 otherwise. For example, [k is even] means 1 when k is even, and 0 otherwise. Other examples:

• sign(x) = [x > 0] - [x < 0]
• [A and B] + [A or B] = [A] + [B]

"Two notes on notation" describes how to harness the power of the square bracket.

This should all sound familiar to C programmers, because many C operators evaluate to 1 when the result is true and 0 otherwise. It's simultaneously disheartening and amusing that while mathematicians and computer scientists are discovering the utility of this convention, some programming language designers actively oppose it by introducing a boolean data type that cannot be interchanged with integers.

The lecture was crammed with other ideas that deserve to be widespread. I discuss them somewhere I can use AsciiDoc and LaTeX equation notation.