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?
Ethereum Stack Exchange is a question and answer site for users of Ethereum, the decentralized application platform and smart contract enabled blockchain. It only takes a minute to sign up.Sign up to join this community
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.