I came across Marijn Heule and Oliver Kullmann's paper on recent techniques in highly efficient [SAT solvers](https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext). In particular they describe the [Pythagorian Triple Problem](https://en.wikipedia.org/wiki/Boolean_Pythagorean_triples_problem), which they solved using that method [one year earlier](https://link.springer.com/chapter/10.1007%2F978-3-319-40970-2_15) (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](https://arxiv.org/abs/1405.3097) for [Erdős's discrepancy problem](https://en.wikipedia.org/wiki/Sign_sequence#Erd.C5.91s_discrepancy_problem) (before it was generally [solved by Terence Tao](https://discreteanalysisjournal.com/article/609-the-erdos-discrepancy-problep)).


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? 



Mapping problems to Boolean formulas for SAT solvers
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](https://doi.org/10.3389/fphy.2014.00056) in which Satisfiability Modulo Theory (SMT) solvers play a role in mapping 
logical constraints to Ising model Hamiltonians for a quantum annealer.


