Very interesting read. However I’d say that CDCL(T) style SMT solvers are not just the high level language to SAT’s assembly, but they have their own collection of reasoning algorithms on top of the SAT solver. Some SMT solvers even include 2 distinct SAT solvers: one for the main proof search, and one only used for the theory of bitvectors, which is almost entirely “bit-blasted”. So I’m not so sure about this analogy, even though it’s hard to find a better one. I think tools like this would be closer to a high level language on top of SAT.
I’m curious about your bitblasting SMT solver, what does it do and how? :)
Thank you :) I didn’t know SMT solvers were using separate SAT solvers for BV and for the core CDCL(T) loop. Do you have any pointers for that or know why this is done? My intuition says that such a split would make solving instances that mix BV and other theories more difficult, but I can very well imagine my intuition being wrong here.
Like most analogies, it breaks apart if you push it too hard, still I think it’s a useful approximation for someone that has so far considered an SMT solver to be a black box.
The bit-blasting SMT solver I wrote is nothing special, it does straight forward translation of an AST to an AIG (and-inverter graph) and then generates clauses from that. It does no optimization or propagation on the AST and only very little optimization on the AIG. I wrote it as part of a larger project, where I needed a BV SMT solver with more access to the internals than Boolector offers, and the easiest way to get there was to write a very simple bit-blasting one myself. I had already lots of experience in writing problem specific CNF generators. The project didn’t lead anywhere for unrelated reasons.
I might revisit writing a bit-blasting BV SMT solver again at some point. I do have some ideas I want to try :)
If I remember correctly, CVC4 does this, but I don’t have a link on hand right now. The reason why this might be a good idea is that the primary SAT solver in CDCL(T) is tailored for incremental solving interleaved with the theories, may have some specific heuristics for literal weights, might not restart too often, etc. whereas an off the shelf modern SAT solver dedicated to bitblasting will be more efficient on large SAT instances. A lot of CDCL(T) solvers, I think, are originally based on minisat or a minisat-inspired architecture, whereas the best SAT solvers can be significantly better than minisat (look at satcomp!). So it’s a good engineering compromise to separate the two use cases.
Hi everyone, I’m the author of this blog post and happy to answer any questions :)