we define a collection of mappings that transform many-valued clausal forms into satisfiability equivalent Boolean clausal forms, analyze their complexity, and evaluate them on a set of benchmarks with a state-of-the-art SAT solver. Our results provide experimental evidence that encoding combinatorial problems with the mappings defined here can lead to substantial performance improvements in complete SAT solvers.