Compile! Project - CRIL-CNRS & Univ. Artois

The cn2cnf preprocessor

Translate constraint networks (CNs) into CNF formulas

cn2cnf is a translator associating with an input constraint network (respecting the format XCSP3) a CNF formula. The whole set of constraints of XCSP3-core is handled by the translator, except the optimization functions. All the constraints are translated into intensional constraints which are encoded using a Tseitin-like algorithm. cn2cnf is mainly a frontend for Sat4j-csp which produces two files for a given instance (an input constraint network):

a CNF formula (respecting the DIMACS format), which represents the network encoded as a propositional formula,
a CSV file, which contains the mapping betwenn the output variables (those of the generated CNF formula) and the input variable assignments of the constraint network.

Ressources for the cn2cnf translator

the runtime code, composed by a Java class and a shell script

How to use cn2Cnf

cn2cnf invocation

	    $ cn2cnf Domino-100-100.xml > Domino-100-100.cnf
         
$ cat Domino-100-100.cnf 

c ... 

[...] 

c ... 

p cnf 10308 1505508  
              
-1 -2 0 

-1 -3 0 

-1 -4 0 

-1 -5 0 

-1 -6 0 

-1 -7 0 

-1 -8 0 

-1 -9 0 

-1 -10 0 

[...] 

x[0]=0;1 

x[0]=1;2 

x[0]=2;3 

x[0]=3;4 

x[0]=4;5 

x[0]=5;6 

x[0]=6;7 

x[0]=7;8 

x[0]=8;9 

x[0]=9;10 

          [...]

The encoding given in Domino-100-100.csv states that variable 1 in the cnf formula is set to true if and only if the CN variable x[0] has value 0, variable 2 in the CNF formula is set to true if and only if the CN variable x[0] has value 1, and so on.