Constraint Satisfaction in F#

After reading an interesting article by Harald Bögeholz on solving the logical puzzle Slitherlink in Haskell, I thought it would be fun to write a similar solver in F#.However, being a mathematician, I like to approach problems in as general a way as possible, so I decided to write a general CSP solver instead and then use this solver to tackle Slitherlink. As a bonus, the resulting solver can also easily solve problems like the Eight Queens Puzzle and Sudoku – you can find my code here.

A CSP, Constraint Satisfaction Problem, is the problem of assigning values to variables that satisfy some given constraints:

  • There are some variables which need to be assigned values.
  • Each variable has a (finite) domain of possible values. (This will often be a set of numbers, but it could just as well be a set of names, colors, letters and so on.)
  • There are constraints that must be fulfilled by assignments of values to variables.

If each constraint in a CSP is only concerned about two variables, I call the CSP a binary CSP.

Sudoku

Sudoku (Photo credit: The Consortium)

Sudoku can be seen as a binary CSP:

  • There are 9 x 9 = 81 variables, one for each field in the grid.
  • The domain of each variable is the set {1,2,3,4,5,6,7,8,9}. Exceptions are the variables that correspond to fields which have numbers written into them as hints – the domains of such variables only contain one number.
  • The constraints state that no two variables in the same row, column or block can have the same value. This gives (9 + 9 + 9) x (9 x 8 / 2) = 972 constraints.

How do we solve such a (binary) CSP?

There are many different algorithms, some general, some for special kinds of domains and constraints. One of the simplest and most popular algorithms is the so-called AC-3 algorithm.

The idea of this algorithm is to eliminate impossible values from all domains, until each domain only contains values that are consistent with all constraints involving that domain. After this elimination step, there are three possible outcomes:

  1. Each domain only contains one element. In this case, assigning each variable to the one remaining element in its domain is the unique solution to the problem.
  2. At least one domain is empty. Then the CSP does not have a solution.
  3. All domains contain at least one element, and at least one domain contains more than one element. In that case, we “divide and conquer”: We create two new, smaller CSP’s by splitting one domain into two domains. Then we recursively apply the algorithm to the two smaller problems.

Implementing this algorithm in F# in a functional way was easy, and once I had it, I could easily solve Sudokus and the Eight Queens Puzzle with it.

A 3 adjacent to an 0.

A 3 adjacent to an 0. (Photo credit: Wikipedia)

But what about Slitherlink?

Unfortunately, Slitherlink is not a binary CSP. How is Slitherlink a CSP anyway?

  • There’s one variable for each edge in the grid.
  • Each variables domain is {0,1}, where an edge is part of the solution-loop if its value is 1.
  • For each intersection in the grid, either zero or two adjacent edges must have value 1 (otherwise, the solution-loop would cross itself or have “lose ends”).
  • For each number in a field in the grid, the sum of values of the four surrounding edges must be that number.

So each hint number gives a constraint for the four surrounding edges, and each intersection implies a constraint for the adjacent edges (2-4, depending on whether the intersection is in a corner, on the border or in the interior).

Luckily, there is a simple way to convert general CSP’s, which are not binary, into binary CSP’s. Let’s look at an example! Say we have three variables, x, y, and z, each of which has domain {1,2,3}, and let’s say we have the constraint x + y + z = 6, which is clearly not binary, because it involves not only two variables, but all three.

The trick is to introduce a new variable, say xy, with domain {(1,1), (1,2), (1,3), (2,1), (2,2), (2,3), (3,1), (3,2), (3,3)}, i.e. the Cartesian product of the domains of x and y. We also introduce two new constraints, one stating that the first component of the value of xy must equal x, the other stating that the second component must equal y. Note that those two constraints are binary, involving xy and x and xy and y respectively!

We can then rewrite the original non-binary constraint x + y + z = 6 as a binary constraint between xy and z, stating that the sum of the components of xy and z must be 6.

So by introducing the “compound” variable xy and two new binary constraints and by rewriting the non-binary original constraint as a binary constraint involving the new variable, we have “gotten rid of” the non-binary constraint!

It is easy to see that the same idea works not only for constraints involving three variables, but also for constraints that involve even more variables – like four variables in the case of Slitherlink.

So I extended my solver by implementing this idea:

  • If the given CSP is binary, it is solved with the AC-3 algorithm.
  • If it is not binary, it is first converted into a binary CSP (by introducing compound variables and new constraints as explained above). This binary CSP is then solved with AC-3, and the solution is translated into a solution for the original problem.

Sadly, even with this extension, we’re not quite there yet, as far as Slitherlink is concerned: I explained how Slitherlink gives rise to a CSP, but I the careful reader will have noticed that the constraints I mentioned are not enough to guarantee that there will be only one solution-loop. The constraints do guarantee that there will be proper loops (non intersecting, no “lose ends”), but they say nothing about how many loops there will be.

My first idea was to simply first look for all solutions of the CSP and then filter out the illegal ones. This worked surprisingly well for normal 5×5 Slitherlink puzzles, but it took too long for bigger puzzles. So I introduced an extra check into the AC-3 algorithm itself: Whenever AC-3 narrows a domain down to a single element, an optional “global” check is run to see whether this domain can be part of a valid solution. In the case of Slitherlink, this “global check” checks whether there is at most one “loop component”. If there are two, the solution is rejected.

This catches illegal solutions much earlier in the algorithm and leads to a satisfying speed-up.

Finally, I did some profiling, and I saw that some purely functional data structures I had used for my implementation of AC-3 were performing poorly. So I replaced them with their mutable cousins and gained another significant speed-up (sadly for the price of sacrificing some “purity”). On my machine, I can now solve big 10×10 Slitherlink puzzles in less than ten seconds.

Big 10x10 Slitherlink

Big 10×10 Slitherlink

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: