The boolean satisfiability problem (SAT) was recognized as one of the
first NP-complete problems; Norvig implemented it in AIMA-Lisp by
expanding the truth table for a proposition and figuring out whether
any of the rows were satisfied.
The truth-table method is somewhat inefficient, however; and a few
algorithms have been developed (such as DPLL and WalkSAT) which
are more efficient.
Gomes, et al. wrote a good survey of the relevant algorithms; we
can't avoid implementing something like this if we're ever going to
have logical agents, unfortunately.
We'd like to work through some of the seminal texts in computer science that normally collect dust on the bookshelf (AIMA, PAIP, SICP, TAOCP, &c.). We've finished up Structure and Interpretation of Computer Programs; and are currently working through Russell and Norvig's Artificial Intelligence: A Modern Approach.
We're also a support group for people's side projects of every kind: MOOCs (including Coursera, etc.), learning new languages, pet projects; we provide feedback and accountability.
On Sundays, we get together and work (the Hack Club); and, on Mondays, we get together to present what we've done for the week.