2

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?

Improve this question

2 Answers 2

Reset to default
1

SAT 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.

Improve this answer
0

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.

Improve this answer
6
  • Is it possible to convert a smr problem to a sat problem for sat solvers?
    – user2284570
    Aug 15 at 12:24
  • what's an smr problem?
    – Patrick Collins
    Aug 15 at 14:47
  • Sorry, I was meaning smt.
    – user2284570
    Aug 15 at 18:20
  • 1
    ah. Yes. An SMT solver is actually a "generalized SAT solver". You could think of a SAT solver as a specific implementation of an SMT solver.
    – Patrick Collins
    Aug 19 at 21:07
  • I was looking actual programs for converting to dimacs.
    – user2284570
    Aug 20 at 16:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.