Highlights so far are an implementation of DPLL with conflict-clause learning that lets us solve hard sudoku problems in less than a second (not competitive w/ SAT solvers like MiniSat, but not bad either), and a Herbrand style semi-decision procedure for first-order validity.

There's lots of room for more sophisticated methods and optimization. More to come soon.