  The boolean satisfiability problem, SAT, was the first problem proved NP complete [Cook, 1971], i.e., it is a hardest NP problem.  The fact that SAT is NP complete means that all problems in NP are reducible to SAT.  Over the years, researchers have built very efficient SAT solvers which can quickly solve many SAT instances – i.e., find a satisfying assignment or prove that there is none -- even for instances with millions of variables.  Thus, SAT solvers are being used as general purpose problem solvers.  On the other hand, there are known classes of small instances for which current SAT solvers fail.  Thus part of the P versus NP question concerns the practical and theoretical complexity of SAT [Nordström, 2015].