I agree with the recommendation to start with a modelling language in a sibling comment. On the MiniZinc homepage, there are Coursera courses linked that are qu

I agree with the recommendation to start with a modelling language in a sibling comment. On the MiniZinc homepage, there are Coursera courses linked that are quite nice as an introduction into combinatorial modelling. Apart from that, it is worth noting that the solver used in the article, OR-Tools, is not strictly a SAT solver. I would rather describe it as a hybrid portfolio solver, since it combines constraint programming, SAT, MIP, and local search in a single solver. It is also possible to use that solver as a back-end when solving a model written in MiniZinc.