I recently completed a course on NP-Complete Problems at edX. The class introduced using SAT solvers, demonstrated using an SAT solver for Sudoku, and gave several exercises. The exercises were very difficult. I am not confident that I could reduce an arbitrary NP-complete problem to SAT.
I have looked for a book, talk, or website teaching you how to encode problems for a SAT solver. I have not found anything beginner-friendly. Can anyone point me to a learning resource? Ideally, I hope to find or purchase a series of guided exercises that start simple and gradually get complicated.