Mapping problems to Boolean formulas for SAT solvers I came across Marijn Heule and Oliver Kullmann's paper on recent techniques in highly efficient SAT solvers. In particular they describe the Pythagorian Triple Problem, which they solved using that method one year earlier (a problem that was open for several decades, and had a monetary reward by Ronald Graham). Another famous example is the computer-aided special case solution for Erdős's discrepancy problem (before it was generally solved by Terence Tao).
I would like to know whether there is some comprehensive literature on techniques how to map some problems to SAT problems. Otherwise, I would also like to know other special solutions that have been achieved with SAT solvers, using a mapping from a problem in some field to boolean formulars. Are there special methods that are commonly used, or does one has to think about the mapping very specifically from problem to problem? 
 A: I think it's very much specific to particular problems.  The problem statement might be directly translatable into logic clauses, but for nontrivial problems it definitely helps if you formulate the problem in such a way that the SAT solver may handle it efficiently.  
I might mention this paper in which Satisfiability Modulo Theory (SMT) solvers play a role in mapping 
logical constraints to Ising model Hamiltonians for a quantum annealer.
A: In addition to Knuth's book, another useful resource is the Handbook of Satisfiability, especially its 2nd chapter, which discusses some simple best practices for SAT encodings.
A lot of the success solving the Pythagorean Triples Problem has to do not as much with the encoding itself (which in this case is quite straightforward) as with skilled use of efficient parallelization, which is very hard for SAT. The method used is called Cube-and-Conquer, and has its own chapter in the Handbook of Parallel Constraint Reasoning.
I'm afraid that even with all this, making a SAT encoding work well is still a bit of an art, and requires a lot of trial and error (I say this as a person who after writing this answer will go back to fiddling with SAT encodings for work).
