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