I see people using SAT solvers and SMT solvers to verify that solidity code is doing what they are doing.
What is the difference between these two?
Or, more simply, it aims to find a scenario where a set of booleans have no contradictions.
An SMT Solver aims to find if any mathematical equation is solvable. It can be thought of as a generalized SAT Solver. Often, these two tools can be used together. You can get a set of boolean expressions solved by a SAT solver like:
x < 5
y < 5
y > x
And input them to an SMT solver to find examples of what x & y can be.
They are often used together because the SAT solver can get expressions and information much faster than SMT solvers.