Boolean satisfaction and optimization engines to solve SAT, Pseudo-Boolean and MAXSAT problems.