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, cha

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