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):

Ressources for the cn2cnf translator

How to use cn2Cnf

cn2cnf invocation
$ cn2cnf Domino-100-100.xml
CNF output file : Domino-100-100.cnf
Encoding output file: Domino-100-100.csv
launching Sat4j process: java -Xmx2g -Xms2g -jar sat4j-csp.jar DimacsOutputPB Domino-100-100.xml
$ cat Domino-100-100.cnf
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
$ cat Domino-100-100.csv

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.

The following options may be considered:

cn2cnf options

The following command translates Domino-100-100.xml using the Java virtual machine located at /usr/lib/jvm/java-8-openjdk-amd64/jre/bin/java ; the Java VM is allowed to use up to 4GB of RAM.

$ cn2cnf --javaloc /usr/lib/jvm/java-8-openjdk-amd64/jre/bin/java --javamem 4 Domino-100-100.xml