Translate constraint networks (CNs) into CNF formulas

cn2cnf est un traducteur associant à un réseau de contraintes d’entrée (respectant le format XCSP3) une formule CNF. L’ensemble des contraintes de XCSP3-core est traité par le traducteur, à l’exception des fonctions d’optimisation. Toutes les contraintes sont traduites en contraintes intensionnelles qui sont encodées en utilisant un algorithme de type Tseitin. cn2cnf est principalement un frontal pour Sat4j-csp qui produit deux fichiers pour une instance donnée (un réseau de contraintes d’entrée) :

• une formule CNF (respectant le format DIMACS), qui représente le réseau encodé comme une formule propositionnelle,
• un fichier CSV, qui contient la correspondance entre les variables de sortie (celles de la formule CNF générée) et les affectations des variables d’entrée du réseau de contraintes.