SAT has become the backbone of many software systems. In order to make full use of the power of SAT solvers, a SAT compiler must encode domain variables and constraints into an efficient SAT formula. Despite many proposals for SAT encodings, there are few working SAT compilers. This talk focus on Picat-SAT, which demonstrated stunning performance in MiniZinc Challenge 2016, beating long-time top-ranked solvers including or-tools from Google and iZPlus from NTT. In this talk, I will give modeling examples of Picat-SAT, and share some of the encoding algorithms and optimizations used in the Picat-SAT compiler.