This is an experimental toolbox to reduce various problems to boolean satisfiability, such as

• Linear and non-linear integer arithmetic

• Graph coloring

Part of the experiment is to see how SAT solvers perform on a redundant ternary encoding of integer arithmetic.