Ah, but you see, there doesn't need to be bijection between his level and SAT problems. There only needs to be a function that when given an arbitrary SAT instance (your "boolean equation") and a blackbox way of solving his puzzle problems can solve that SAT instance.

The proof of NP-hardness is basically

For every instance of a SAT problem, there exists some puzzle whose solution encodes the SAT solution.

You are asking about

For every instance of his puzzle, does there exist a SAT formula solved by this puzzle

Which is a different question.