I'm trying to figure out how an SMT solver works as simple as possible. Let's assume we have a simple input program with symbolic values x and y. E.g.

if (x+y < 20) {
   if (x > 10) {
      if (y > 10) {

Here we have different paths, depending on the conditions. To reach assume(false) each condition has to be true, so our outcoming formula is:

$x+y < 20 \,\,\,\,\,\wedge \,\,\,\,\, x > 10 \,\,\,\,\, \wedge \,\,\,\,\, y > 10$

So far, so good. What happens next, step by step?

I would like to implement, as simple as possible, a solver which gets as input something like the formula above and delivers specific output to reach the end of the path - here assume(false), i.e. x = 2147483647, y = 2147483647 (jfi: x+y would be -2) - for overflow detection or similar.

I know there are a lot of SMT solvers on the internet, but I couldn't find a really simple self-explaining one. Looking forward to a suggestion.


What happens next is that we invoke a SMT solver to try to check whether the formula

$$x+y < 20 \quad \land \quad x > 10 \quad \land \quad y > 10$$

is satisfiable. The solver tries to find values for $x,y$ that make this formula true. If it finds such a value, then it knows the assume(false) statement is reachable. (I am guessing you meant to write assert(false), not assume(false).) If the formula is not satisfiable, then that statement is not reachable.

So basically you are asking: how do SMT solvers work? That is too broad for this site, but there are lots of places that explain how SAT solvers and SMT solvers work. I would suggest doing some research; you will find many explanations. You could start with the DPLL algorithm for SAT.

There is little point in implementing your own solver. Your solver will probably perform far worse than existing tools. There has been a lot of research into building effective solvers, and the techniques required are non-trivial. Instead, I'd recommend you simply use an existing solver, such as Z3.

If you just want to implement one for fun, the most straightforward approach is probably to bit-blast to SAT: treat each bit of (the binary representation of) $x,y$ as a boolean variable, then write down a boolean formula (on those boolean variables) that expresses the requirement that $x+y<20$. How can you do that? Write a boolean circuit that computes $x+y$ and compares the sum to 20, then convert that circuit from CircuitSAT to SAT. Finally, invoke an off-the-shelf SAT solver to check satisfiability of this boolean formula. You'll need to do some research to understand each of these steps, but there's a lot written on how to do that.

  • $\begingroup$ I already implemented a really simple SAT solver, which takes the DIMACS format as input and checks for satisfiability. Sure, this will be really ineffective, however, I want to implement it as simple as possible, no optimization, only for understanding how such things really work. I also read something about bit-blasting, but how can I treat each bit of $x,y$ as a boolean variable since they have no value, because they are symbolic, no? $\endgroup$ – racc44 Sep 29 '17 at 5:31
  • 1
    $\begingroup$ @racc44, As I wrote in my answer, in my opinion "write me a tutorial on how to build a SMT solver" is too broad to be a good fit for this site's format, because answers would need to be too long. However, there are many resources that describe algorithms for SMT. I suggest doing some research to read about them, and after that, if you run into a specific question about something you read, ask a new question about that. $x,y$ are just variables. You can create a new (boolean) variable $t_0$ to represent "the least significant bit of $x$", and so on. $\endgroup$ – D.W. Sep 29 '17 at 5:37
  • 1
    $\begingroup$ @racc44, an example paper: ece.uwaterloo.ca/~vganesh/Publications_files/vg2007-STP-CAV.pdf That's a fairly advanced paper that assumes you know how bit-blasting and other standard techniques work, so perhaps read more basic material first, but it might help you find an entry point into the research literature (by reading the papers it cites). $\endgroup$ – D.W. Sep 29 '17 at 5:44
  • $\begingroup$ @racc44 the whole point of a variable is that you don't know it. If you knew it, it would be a constant. $\endgroup$ – harold Sep 29 '17 at 8:15

You may not need a general SMT solver. In this case, you have a bunch of inequalities conjoined together, which you can solve as a linear program.

A simpler alternative to an SMT solver is to implement the theory as an add-on to a logic program. Most decent Prolog implementations, for example, have a CLP(R) or CLP(Q) library which can solve equality and inequality constraints over reals or rationals.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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