[specialgoodness]

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.