undefined | Better HN

0 pointsAnimats4mo ago0 comments

I was doing this in 1980-1983. Here's some code.[1] It's been partly converted to Common LISP, but I was unable to get some of the macros to work.

This is the original Oppen-Nelson simplifier, the first SAT solver. It was modified by them under contract for the Pascal-F Verifier, a very early program verifier.

We kept all the code under SCCS and built with make, because the LISP part was only part of the whole system.

[1] https://github.com/John-Nagle/pasv/tree/master/src/CPC4

0 comments

specialgoodness4mo ago

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.

e404mo ago

Do you remember who you discussed it with? It had to be either Sklower or Foderaro, unless you talked with Fateman.

Were the macros originally from another dialect of Lisp?

AnimatsOP4mo ago

Franz LISP had, I think, MacLISP macros, while Common LISP has a different system.

I talked to Fateman at some point. Too long ago to remember about what.

j / k navigate · click thread line to collapse