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.
Also: have you looked at the poly-algorithm for 4-coloring? I rather write the SAT instance by hand...