Publicacions

Mapping many-valued CNF Formulas to Boolean CNF Formulas

Publication Type:

Conference Paper

Authors:

Carlos Ansótegui; Felip Manyà

Source:

Proc. 35th Intern. Symposium on Multiple-Valued logics ISMVL, IEEE, p.290 - 295 (2005)

Abstract:

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 a SAT solver. Our results show that encoding combinatorial problems with the mappings defined here can lead to substantial performance improvements in complete SAT solvers.

»