Mostly Lint cleanup

Also, interface changes to the boolfunc.satisfy_one and
Expression.equivalent methods. The ability to change the SAT algorithm
seems a little silly, so just choose a good default. More advanced
methodologies should approach the solution from algorithm rather than
data.