I came across Majin 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?

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?