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.