Using Alloy Analyzer to solve the first Google Davinci Code Quest puzzle!

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 test

open 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.

Weird files (advertismen.com and pushowXX.dll)

Last night I found on a P2P network an exe file that was supposed to be a screensaver. Well...yes I did double click! It gave me a usual "do you want to proceed with the installation?" window and I said yes! Well... that was it! It finished the installation, but I could not find any new screen saver on the control panel or anywhere else. Weird isn't it?

Now, I downloaded a trial version of Ashampoo Uninstaller platinum to see the changes the installation made to my system. I installed Ashampoo and run the "screensaver" installer again. This time I noticed that somewhere in the text of the terms and conditions a company named "ADVERTISMEN.COM" appeared. Tried to google it but wasn't lucky. I also did a DSN lookup of the url and found out that the domain name was registered on the 5th of April of 2006. Is it a new spyware?

Well, after the installation was finished, Ashampoo generated a log file, which showed that the install.exe had installed two files in the windows/system32 folder. The files were called pushow67.dll and pushow55.dll. I used DLL Export Viewer to find out that they exposed one interface called "Uninstall". It also created a registry key under: HKEY_LOCAL_MACHINE\SOFTWARE\Microsoft\Windows\CurrentVersion\Uninstall\ called "UninstallString" with value: rundll32.exe C:\WINNT\system32\pushow55.dll Uninstall

It also created another key under: HKEY_LOCAL_MACHINE\SOFTWARE\Microsoft\Windows NT\CurrentVersion\Windows called AppInit_DLLs. The value was pushow55.dll.

All this is weird! I deleted the files and the registry entries, run ad-aware and spybot and they didn't find anything. Finally I logged to my online banking system (didn't enter my real credentials though) running Etheral. After inspecting the packets I didn't find anything alarming.

Well... I am not sure if it is a new spyware, Trojan or something, but I know I should have thought twice before running that bloody exe file. Now I just hope I have cleaned my system from whatever it was!