But in the article is said: The proof is surprisingly simple and he did it by showing how the boolean satisfiability problem (SAT) can be mapped onto a level in the game.
And only an example level was given, one that looks like it was designed for that purpose. What I can't understand is how a "real" level of the game (like this one: http://bit.ly/bOWbgi ) can be mapped in a boolean equation.