ToySMT – simple SMT solver under 1500 SLOC of pure C | Hacker News Reader

ToySMT – simple SMT solver under 1500 SLOC of pure C

github.com

91 pointsdennis7147 comments

The author of this (Dennis Yurichev) has also written a 200 page "Quick introduction into SAT/SMT solvers and symbolic execution" that is full of examples of how SAT/SMT solvers can be used.

[1]: https://yurichev.com/writings/SAT_SMT_draft-EN.pdf

This is, in my opinion, not a "real" SMT solver. It translates an SMT instance into a SAT instance. This is easy to do for the theories the author is considering (bitvectors), but not at all straightforward for integers or reals.

Most SMT solvers today use the DPLL(T) technique which transfers information back and forth between a so-called theory solver (e.g., a simplex solver that handles real constraints) and a SAT solver which handles the "Boolean part" of the problem . I feel that an SMT solver that intends to be educational must implement DPLL(T).

I've only seriously examined the source of Z3, but encoding an SMT problem to multiple SAT instances remains a feature there - just convert any qf_bv problem into bit width * SAT instances / 2!

I recall that many popular simplifications required a problem to be expressible as CNF.

(I also seem to recall there is some strategy to simplify logics over Reals/Ints into BV without encoding logical "bignum circuitry" as well?)

> but encoding an SMT problem to multiple SAT instances remains a feature there

Sure. I'm not arguing that bitblasting should never be done, it's probably still the best way of solving bitvector problems. My point is that the pedagogical objective of an toy SMT solver is lost if doesn't teach DPLL(T) and only focuses on bitblasting.

For anybody wondering what SMT stands here for, it's: satisfiability modulo theory.

For anyone wondering how you could write a solver in 1500 lines of C, the answer is here: https://github.com/DennisYurichev/ToySMT/blob/master/ToySMT....

(i.e., use 'system' to shell out to an already existing solver, which is at least documented in the readme).

(To be clear, it shells out to an existing SAT solver. If I understand correctly, the 1500 lines of C implement the "modulo theory" part of "satisfiable modulo theory" — that is, they "compile" things like bitvector addition into pure boolean circuits.)

Reply on news.ycombinator.com