I'm confused why he brings up the four color theorem, since a 4-coloring of a planar graph can be determined in polynomial time. And he also makes it sound like the theorem hasn't been proven yet.
I think it's fine taking this as a constraint problem. It just means, you know beforehand that there is a solution. Also, if the underlying problem is in P, chances are the SAT instance is not that hard.
Also: have you looked at the poly-algorithm for 4-coloring? I rather write the SAT instance by hand...
