I see your point -- CNF as a modeling language leaves a lot to be desired. What I like about this article is that it uses CNF anyway and takes you through the

I see your point -- CNF as a modeling language leaves a lot to be desired. What I like about this article is that it uses CNF anyway and takes you through the hard work you'd have to do to express a problem that way. I didn't know about the Tseytin transformation, for instance, so I'd given up on using CNF because of the exponential blowup in my constraints. I probably still won't be using SAT solvers directly, but it's nice to learn how they work. It's like knowing an assembly language for constraint satisfaction.