Projet de programmation

Mini Solver SMT

Le projet est à rendre pour le 8 juin 2018. Il peut être réalisé en binôme.

Programmer votre solver SMT

Le but du projet est de programmer un démonstrateur SMT combinant un solver SAT avec une procédure de décision pour la théorie de l'égalité (uniquement entre variables). Essentiellement, cela revient à s'inspirer des règles de DPLL(T) vues en cours, et à utiliser une structure union-find comme procédure de décision pour la théorie de l'égalité (cette structure devra être étendue pour raisonner sur les différences).

Langage d'entrée

Le langage d'entrée de votre solver SMT est une simple extension du format Dimacs des solvers SAT. Voici sa syntaxe sur un petit exemple:
c Exemple d'un fichier .cnfuf 
p cnf 4 2
1=2 2<>4 1=3
1=3 4<>1
La première ligne qui commence par le caractère c est un commentaire. La deuxième ligne p cnf 4 2 indique que la formule est une CNF avec 4 variables et 2 clauses. Les variables sont représentées par des entiers (dans l'exemple, 1, 2, 3 et 4). Chaque clause tient sur une seule ligne et est constituée d'atomes de la forme i=j ou i<>j, où i et j représentent deux variables, c'est-à-dire deux entiers entre 1 et 4.

Les transparents du cours

TP sur Cubicle

Quelques articles ou chapitre de livre

À rendre pour le 8 juin 2018

Envoyez votre solution sous la forme d'un fichier compressé portant votre nom (nom.tgz), ou les deux noms de votre binôme (nom1-nom2.tgz), à sylvain.conchon@lri.fr

Votre archive devra contenir les sources de votre programme, un makefile pour le compiler, un petit texte d'une page décrivant ce que vous avez implémenté et les fichiers de tests que vous avez utilisés.