Mapping Problems with Finite-Domain Variables into Problems with Boolean Variables

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

Authors

• Carlos Ansótegui
• Felip Manyà

Keywords

No keywords are indexed for this paper.