I am working on an application using Quantifier-Free Bit-Vector/Array satisfiability which may or may not require mucking around with the internals of an SMT solver, and would like to understand what's going on behind the scenes of existing methods (beyond merely reading their API's). What papers should anyone interested in working with SMT solvers, particular in QF_ABV, read? I'd be particularly interested in 1) why and how current SAT solvers are able to work so well on an NP-complete problem and 2) the specifics of how bit-vector and array theories are implemented and any tricks that speed them up.
5
-
1$\begingroup$ Regarding your question (1), a short answer is: we have no idea why and a good answer would probably involve solving P/NP. A longer answer would be to consider the videos here, in particular Moshe Vardi's. They are now a couple of years old, but there as been no breakthrough in SAT solving since. $\endgroup$ – Martin Berger May 20 '18 at 14:29
