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

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.

[1] http://en.wikipedia.org/wiki/Boolean_satisfiability_problem

[2] http://www.cs.berkeley.edu/~russell/code/logic/algorithms/prop.lisp

[3] http://en.wikipedia.org/wiki/DPLL_algorithm

[4] http://en.wikipedia.org/wiki/WalkSAT

[5] http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-Handbook.pdf

Join or login to comment.

  • Peter D.

    Great demos by Ryan, Rex and Prasan; thanks, guys!

    October 1, 2013

7 went

People in this
Meetup are also in:

Create a Meetup Group and meet new people

Get started Learn more

Meetup has allowed me to meet people I wouldn't have met naturally - they're totally different than me.

Allison, started Women's Adventure Travel

Start your Meetup today

Act now and get 50% off.
Until February 1.

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy