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.

• Type: Conference
• Year: 2004
• Where: SAT
• Authors: Carlos Ansótegui, Felip Manyà
• Keywords: Complete Sat Solvers, SAT 2004, SAT Solvers, State-of-the-art Sat Solvers