CSP2SAT4J: A Simple CSP to SAT translator
Daniel Le Berre, Inês Lynce, Rue Jean, Souvraz Sp · 2005
Abstract. SAT solvers can now handle very large SAT instances. As a consequence, many translations into SAT have been shown successful in recent years: Planning and Bounded Model Checking are two examples of applications in which SAT engines are reported to be as good as or even better than dedicated software. The idea of CSP2SAT4J is to see how a SAT solver could compete against a CSP solver. The translation from CSP to SAT is very basic, and the SAT solver used is not the fastest available, but it has the good property to handle cardinality constraints, which minimises the number of constraints used in the translation. The results obtained by the solver should provide an idea about the efficiency of a “brute force ” translation from CSP into SAT. 1