Contraintes & Apprentissage

Les formalismes de contraintes riches et expressifs permettent de décrire des problèmes complexes de manière naturelle et succincte. Les solveurs de contraintes permettent alors d'en trouver des solutions de manière efficace.

Contraintes du premier ordre

on s'intéresse ici à la décidabilité et la complétude de théories étendues, et à leurs algorithmes de résolution de contraintes

Contraintes quantifiées

on s'intéresse ici aux problèmes de contraintes faisant intervenir les quantificateurs existentiels et universels.

Parallélisation fractale de SAT

on s'intéresse ici à l'accélération des algorithmes combinatoires au travers des schémas de parallélisation fractale qui deviennent possibles dans le modèle de calcul des machines à signaux.

Projets

digecode

parallélisation sur grille de solveurs CSP