Past Meetup

Let's implement a SAT-solver (AIMA ch. 7).

This Meetup is past

8 people went


The boolean satisfiability problem (SAT) was recognized as one of the
first NP-complete problems[1]; Norvig implemented it in AIMA-Lisp by
expanding the truth table for a proposition and figuring out whether
any of the rows were satisfied.[2]

The truth-table method is somewhat inefficient, however; and a few
algorithms have been developed (such as DPLL[3] and WalkSAT[4]) which
are more efficient.

Gomes, et al. wrote a good survey of the relevant algorithms[5]; we
can't avoid implementing something like this if we're ever going to
have logical agents, unfortunately.