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.

Any category    Compiler   

Go to the software webpage