As I was searching for something on google, I saw an ad at the bottom of the page. The ad was about the Davinci code new movie that is coming out. I clicked and found a sudoku like puzzle, related to the movie. The puzzle is explained in the following two pictures (description can also be found on: http://student-rant.blogspot.com/2006/04/googles-da-vinci-code-quest-1.html)

Well… it is clearly a very simple problem for a constraint solver, like Alloy Analyzer! I created the following model (took me half an hour, so no comments or too much thought about it).

module testopen util/ordering[Natural] as ord

abstract sig Natural{}

one sig One extends Natural{}
one sig Two extends Natural{}
one sig Three extends Natural{}
one sig Four extends Natural{}

abstract sig Symbol{}

one sig Cross extends Symbol{}{}
one sig Fi extends Symbol{}{}
one sig Blade extends Symbol{}{}
one sig Star extends Symbol{}{}

sig Cell{
symbol: one Symbol,
rowIndex: Natural,
columnIndex: Natural,
inRange: Natural
}

fact Numbers{
ord/first() = One
ord/next(One) = Two
ord/next(Two) = Three
ord/last() = Four

}

pred defineRange(row:Natural,column:Natural,r:Natural){
all c:Cell |
c.rowIndex = row && c.columnIndex = column => c.inRange = r
}

fact DefineRange{
defineRange(One,One,Two)
defineRange(One,Two,One)
defineRange(One,Three,One)
defineRange(One,Four,One)
defineRange(Two,One,Two)
defineRange(Two,Two,Two)
defineRange(Two,Three,Three)
defineRange(Two,Four,One)
defineRange(Three,One,Four)
defineRange(Three,Two,Two)
defineRange(Three,Three,Three)
defineRange(Three,Four,Three)
defineRange(Four,One,Four)
defineRange(Four,Two,Four)
defineRange(Four,Three,Four)
defineRange(Four,Four,Three)
}

pred staticSymbols(row:Natural, column:Natural, s:Symbol){
all c:Cell |
c.rowIndex = row && c.columnIndex = column =>
c.symbol = s
}

fact{
staticSymbols(One,Four,Fi) &&
staticSymbols(Two,Two,Cross) &&
staticSymbols(Four,Two,Blade) &&
staticSymbols(Four,Three,Star)
}

// No two same symbols in the same Range
fact{
all disj c,c’:Cell |
c.inRange = c’.inRange =>
c.symbol != c’.symbol
}

// All cells have different rowIndex and columnIndex
fact{
no disj c,c’:Cell | (c.rowIndex = c’.rowIndex && c.columnIndex = c’.columnIndex)
}

//No two same symbols in the same row Column
fact{
all disj c,c’:Cell |
c.rowIndex = c’.rowIndex =>
c.symbol != c’.symbol

all disj c,c’:Cell |
c.columnIndex = c’.columnIndex =>
c.symbol != c’.symbol
}

pred solution(){
#Cell = 16
}

run solution for 16 Cell

Alloy Analyzer came up with a solution in 3 seconds, on the dual core 2GB RAM opteron server running linux!

The solution is the following one:

symbol= { (Cell_0 Blade_0) (Cell_1 Blade_0) (Cell_2 Blade_0) (Cell_3 Blade_0) (Cell_4 Fi_0) (Cell_5 Fi_0) (Cell_6 Fi_0) (Cell_7 Fi_0) (Cell_8 Cross_0) (Cell_9 Cross_0) (Cell_10 Cross_0) (Cell_11 Cross_0) (Cell_12 Star_0) (Cell_13 Star_0) (Cell_14 Star_0) (Cell_15 Star_0) }

rowIndex = { (Cell_0 One_0) (Cell_1 Two_0) (Cell_2 Three_0) (Cell_3 Four_0) (Cell_4 One_0) (Cell_5 Two_0) (Cell_6 Three_0) (Cell_7 Four_0) (Cell_8 One_0) (Cell_9 Two_0) (Cell_10 Three_0) (Cell_11 Four_0) (Cell_12 One_0) (Cell_13 Two_0) (Cell_14 Three_0) (Cell_15 Four_0) }

columnIndex = { (Cell_0 One_0) (Cell_1 Four_0) (Cell_2 Three_0) (Cell_3 Two_0) (Cell_4 Four_0) (Cell_5 Three_0) (Cell_6 Two_0) (Cell_7 One_0) (Cell_8 Three_0) (Cell_9 Two_0) (Cell_10 One_0) (Cell_11 Four_0) (Cell_12 Two_0) (Cell_13 One_0) (Cell_14 Four_0) (Cell_15 Three_0) }

It is quite straightforward! The symbol of Cell_0 is Blade, its row is One and column One. The symbol of Cell_1 is Blade again, he row is Two and Column Four etc.

The symbol names are not related to the movie or book symbol names. In my model Blade is the pyramid like shape, Fi is the Greek letter fi, Cross is the symbol that looks like a cross and Star is the symbol that looks like a star. I know that I spent half an hour to solve a problem that would have taken me around 10 minutes to solve manually, but as a proper nerd I prefer to use my (few) grey cells to think how to use a computer to solve a problem for me, instead of solving the problem myself.

Well.. that’s it! I don’t want to spend more than 1 hour on this!

There are a couple of blogs with solutions to the puzzles.
Links to solutions:
http://student-rant.blogspot.com/2006/04/warning-solution-to-google-da-vinci.html
http://googlefact.blogspot.com/

UPDATE: I used the model on my P4 running @ 2.8G with 712 MB ram and took AA 23 seconds to solve the problem. Not bad at all! But for bigger problems the state space will be increased by too much. Looks like an AI technique should be used to find a solution.