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 communitySAT solvers are used for Boolean formulas while SMT solvers can handle formulas that involve multiple theories. Both can be used to verify Solidity code, but SMT solvers are more powerful and can reason about more complex properties.
A SAT Solver aims to solve the boolean satisfiability problem for a set of boolean expressions.
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.