Basée sur Autowrite, Autograph est une bibliothèque d'automates permettant de vérifier des propriétés sur les graphes de largeur de clique bornée. Ces graphes peuvent en effet être représentés par des termes qui peuvent alors être traités par des automates. Le problème d'obtenir un terme à partir d'un graphe est appelé décomposition . Trouver un terme de largeur de clique optimale est un problème NP-complet. Une réduction au problème SAT combinée à l'utilisation d'un SAT-solver permettent d'obtenir un terme de largeur de clique optimale pour de petits graphes (au maximum 24 sommets). Pour de plus gros graphes on utilise des heuristiques et on obtient des termes de largeur de clique non optimale qui peuvent être néanmoins utilisés par Autograph pour vérifier des propriétés sur le graphe. Le buit de ce projet serait d'expérimenter diverses heuristiques de décomposition.
L'utilisation de Common Lisp serait préférable car elle permet de réutiliser le code de différents modules d'Autograph (termes, graphes). L'utilisation d'un autre langage n'est pas exclue.
Articles: