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.