Description

CSP2SAT est une bibliothèque permettant de transcrire un réseau de contraintes en un ensemble de clauses dans le but de résoudre le problème SAT associé à l'aide d'un solveur SAT.

Fonctionnalités

Le seul format de description accepté en entrée pour décrire le réseau de contraintes est le format XML décrit dans ce document. C'est le format utilisé pour la compétition de solveurs CSP First International Constraint Satisfaction Solver Competition.

CSP2SAT peut utiliser plusieurs types de codages :

Codage direct (direct encoding)
Codage multivalué (multivalued encoding)
Codage par supports (support encoding)

Pour chacun de ces codages, CSP2SAT permet de transformer le réseau de contraintes en un réseau de contraintes binaires. Il permet aussi de choisir la façon d'écrire les contraintes d'exclusion. La description des différents codages est disponible dans ce document.

CSP2SAT produit deux fichiers en sortie :

Un fichier au format DIMACS CNF (voir ce document pour une description du format) décrivant les clauses;
Un fichier dans le format XML dont un exemple est disponible ci-dessous, décrivant les variables du problème et leurs valeurs.

<?xml version="1.0" encoding="UTF-8"?>
<variables>
  <variable name="X0" nbValues="10" domain="0 1 2 3 4 5 6 7 8 9" />
  <variable name="X1" nbValues="2" domain="Un Deux" />
  <variable name="X2" nbValues="4" domain="Un Deux Trois Quatre" />
</variables>

Téléchargement

Le source de CSP2SAT (en C++) est téléchargable ici. Pour le décompresser, il est suffisant de posséder gzip et tar

CSP2SAT nécéssite la bibliothèque Xerces (C/C++) du projet Apache pour fonctionner. Vous pouvez la télécharger ici et lire les instructions pour son installation là.

Chacun de ces logiciels est soumis à sa propre licence qui précise ses conditions d'utilisation, de modification et de redistribution. CSP2SAT est soumis à la licence GNU GPL.

Installation

Avant la compilation, assurez vous que vous possédez bien les prérequis, à savoir :

Les sources de CSP2SAT;
Un compilateur C++;
La bibliothèque Xerces-c correctement installée ainsi que tous ses en-têtes;

Ensuite, pour compiler :

Décompressez les sources de CSP2SAT;
Modifiez le Makefile pour l'adapter à votre compilateur et à votre installation de Xerces;
Dans le répertoire contenant les sources de CSP2SAT, tapez make.

Normalement, vous devez obtenir une bibliothèque dynamique libcsp2sat.so, une bibliothèque statique libcsp2sat.a et un executable csp2sat.

Utilisation

Le traducteur csp2sat prend en entrée un fichier décrivant un réseau de contraintes en XML. Il produit en sortie un fichier XML décrivant les variables et leurs domaines ainsi qu'un fichier modélisant de façon booléenne le problème.

L'utilisation de csp2sat se fait selon la syntaxe :

Par exemple pour traduire le fichier souffleuse.xml avec le codage multivalué avec binarisation des contraintes, on executera :

./csp2sat multivalued-bin souffleuse.xml varsSouffleuse.xml clausesSouffleuse.cnf

Pour un exemple d'utilisation de libcsp2sat, on pourra se reporter aux sources de csp2sat (fichier main.cpp).

Contact

Pour rapporter un bug, soumettre un patch (qui corrige un bug, qui ajoute un nouveau type de codage, ou qui améliore les performances), envoyez un courriel à nicolas POINT morbieu AROBASE laposte POINT net ou à helene POINT fargier AROBASE irit POINT fr.

Liens

Logiciels

Le solveur SAT zChaff
La bibliothèque Xerces

Publications

La description du format XML utilisé pour décrire les réseaux de contraintes (lien direct);
La description du format DIMACS CNF utilisé pour décrire les ensembles de clauses;
Les différents types de codages utilisés dans CSP2SAT.