SAT solvers are getting more and more efficient in solving large instances and are being used as back-ends in various contexts. Every time one wants to use them to solve a problem in a specific domain, he/she has to come up with an ad-hoc encoding that not only has the right set of solutions but also puts the constraints (even redundant) in a form that helps the heuristics of solvers in finding a solution faster.
Many such encodings seem to me would be very common, for example: asserting that a finite set of nodes is linked as a tree, or as a DAG, or a list is sorted...
Is there a repository/recipe book of common encodings for common problems with optimised solutions?