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.