5
$\begingroup$

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.

|cite|improve this question
$\endgroup$
  • 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

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.