I am certain not a SAT specialist and it is a very frustrating technology. There is little literature and it is very hard to figure out what it means in concret

I am certain not a SAT specialist and it is a very frustrating technology. There is little literature and it is very hard to figure out what it means in concrete cases. But this article is way above all that I read on this subject. Many thanks! Just an example: "Modeling has lots of interesting constraints, one of which I often hear and I am confused by: that it should minimize the number of variables. Given the above, that SAT solvers can be seen at as partial evaluation engines that thrive on the fact that they can partially evaluate and partially backtrack"