The Nelson-Oppen simplifier is a great piece of work, but it is not the first SAT solver. Boyer and Moore published their formally verified SAT solver in their 1979 A Computational Logic, the first book on the Boyer-Moore Theorem Prover, though it was first implemented I believe in 1973. This algorithm, based on IF-normalization and lifting, was also a core part of the original Boyer-Moore prover. One interesting note is that it actually was almost an earlier discovery of BDDs - they have the core BDD data structure and normalization algorithm but were just missing memoization and the fact that orderings on variables induce canonicity for checking boolean equivalence! But in any case, Boyer-Moore had a (formally verified, even!) implemented and used SAT solver long before Nelson and Oppen.
Beautiful! Imandra is a modern Boyer-Moore style theorem prover for higher-order functional programming (its logic is based on a typed higher-order subset of OCaml rather than Boyer-Moore's basis on an untyped first-order subset of Pure Lisp (and later Common Lisp with ACL2)), but there are a lot of similarities! It also integrates computable counterexamples in a really cool way (they're first-class values reflected in the runtime and you can directly compute with them, including counterexamples to higher-order goals which involves function synthesis!). Imandra is used a lot for formal verification in finance, for example.
This is interesting work but it totally misses the boat when it talks about the current state of the art. They cite a 2014 version of the Goel-Hunt-et al formal x86 model in ACL2, but they fail to talk about its modern version. The modern version (developed at Centaur and then Intel!) is an ACL2 x86 model that is so precise that it can boot Linux and run user-land programs. Let me say that again: it is a formal mathematical model of a processor that is so precise that it can boot Linux and run user-land programs! This is a monumental accomplishment and is not even mentioned in their paper.
