This is a faster implementation of WalkSAT and theorem proving by resolution. Compared to original AIMA WalkSAT code, a Python to C++ translation resulted in a 46% average run time reduction. Further optimizations of the C++ WalkSAT in data structure and algorithm resulted in an addition 10 fold increase in speed.