Title :
Mapping many-valued CNF formulas to Boolean CNF formulas
Author :
Ansótegui, C. ; Manyà, F.
Author_Institution :
Dept. of Comput. Sci., Cornell Univ., Ithaca, NY, USA
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.
Keywords :
Boolean functions; computability; computational complexity; equivalence classes; multivalued logic; SAT solver; computational complexity; equivalent Boolean clausal forms; many-valued clausal forms; satisfiability; Artificial intelligence; Computer science; Encoding; Logic; Machinery; Polynomials; Problem-solving; Random number generation;
Conference_Titel :
Multiple-Valued Logic, 2005. Proceedings. 35th International Symposium on
Print_ISBN :
0-7695-2336-6
DOI :
10.1109/ISMVL.2005.23
