Olivier ROUSSEL

Ma thématique de recherche gravite pour l'essentiel autour du problème SAT. En deux mots, ce problème consiste à déterminer si une formule booléenne admet ou non un choix de valeurs qui la rende vraie.

runsolver Runsolver est le programme qui contrôle les resources utilisées par un solveur dans les compétitions. Il est maintenant disponible sous licence GPL.

PB12 : la septième compétition de solveurs pseudo-booléens Avec Vasco Manquinho, j'organise la septième compétition de solveurs pseudo-booléens. Tous les détails sur cette compétition sont disponibles à cette adresse : http://www.cril.univ-artois.fr/PB12

ppfolio ppfolio est un outil qui permet de simuler le Virtual Best Solver (VBS) sur un système multicoeurs. Bien qu'il se contente de lancer plusieurs solveurs en parallèle, il a obtenu des résultats exceptionnels à la compétition 2011. Voir la page consacrée à ppfolio.

SAT 2011 Competition Avec D. Le Berre et L. Simon, j'organise l'édition 2011 de la compétition SAT (voir le site web des compétitions SAT et les résultats détaillés de la compétition)

PB11 : la sixième compétition de solveurs pseudo-booléens Avec Vasco Manquinho, j'organise la sixième compétition de solveurs pseudo-booléens. Tous les détails sur cette compétition sont disponibles à cette adresse : http://www.cril.univ-artois.fr/PB11

PB10 : la cinquième compétition de solveurs pseudo-booléens Avec Vasco Manquinho, j'organise la cinquième compétition de solveurs pseudo-booléens. Tous les détails sur cette compétition sont disponibles à cette adresse : http://www.cril.univ-artois.fr/PB10

SAT 2009 Competition Avec D. Le Berre et L. Simon, j'organise l'édition 2009 de la compétition SAT (voir le site web des compétitions SAT et les résultats détaillés de la compétition)

Quatrième compétition de prouveurs CSP : CSC09 Avec C. Lecoutre et M. Van Dongen, j'organise la quatrième édition de la compétition de prouveurs CSP, Max-CSP et WCSP

PB09 : la quatrième compétition de solveurs pseudo-booléens Avec Vasco Manquinho, j'organise la quatrième compétition de solveurs pseudo-booléens. Tous les détails sur cette compétition sont disponibles à cette adresse : http://www.cril.univ-artois.fr/PB09

Troisième compétition de prouveurs CSP : CPAI08 Je participe à l'organisation de la troisième compétition de prouveurs CSP (voir aussi ce miroir).

SAT 2007 Competition J'ai intégré l'équipe des organisateurs de la compétition SAT quand ils ont choisi d'utiliser l'environnement que j'ai mis en place pour les évaluations et compétition PB06, CPAI06 et PB07 (cet environnement est lui même dérivé de celui de la compétition SAT 2005 développé par Laurent Simon et Daniel Le Berre). Voir le site web des compétitions SAT et les tous les détails sur la compétition SAT 2007

The SAT Game Le SAT Game est une présentation amusante du problème SAT. Essayez de résoudre à la main des instances SAT simples !

PB07 : la troisième évaluation de solveurs pseudo-booléens Avec Vasco Manquinho, j'organise la troisième évaluation de solveurs pseudo-booléens. Tous les détails sur cette évaluation sont disponibles à cette adresse : http://www.cril.univ-artois.fr/PB07

Deuxième compétition de prouveurs CSP : CPAI06 J'ai participé à l'organisation de la deuxième compétition de prouveurs CSP. Les résultats de cette compétition sont disponibles sur cette page.

Un analyseur syntaxique en C/C++ pour le format XML 2.0 des instances CSP Je suis en train d'écrire un analyseur syntaxique pour le format XML 2.0 des instances CSP. Suivre ce lien pour des informations complémentaires.

PB06 : la deuxième évaluation de solveurs pseudo-booléens Avec Vasco Manquinho, j'organise la deuxième évaluation de solveurs pseudo-booléens. Tous les détails sur cette évaluation sont disponibles à cette adresse : http://www.cril.univ-artois.fr/PB06

csp2sat+zchaff Dans le papier d'ICTAI'04, j'ai introduit une compilation logique qui permet à la propagation unitaire sur des clauses d'obtenir les mêmes résultats que le maintien de l'arc-consistance sur un problème CSP (une alternative au support encoding). Cette compilation logique a été expérimentée dans un solveur basé sur zChaff et qui a été soumis à la First International Constraint Satisfaction Solver Competition. Bien que ce solveur ait été écrit à la hâte en moins de trois jours, il a obtenu des résultats tout à fait satisfaisants sur les CSP binaires (et des résultats assez mauvais sur les CSP non binaires ce qui est finalement assez logique puisque la gestion des contraintes n-aires était minimaliste). Voir les actes de la compétition pour connaître les résultats de ce solveur. Téléchargez la version de csp2sat+zchaff qui a participé à la compétition (exécutable Linux statique, compressé avec bzip2)

PB05 : la première évaluation de solveurs pseudo-booleéens Avec Vasco Manquinho, j'ai organisé une évaluation de solveurs pseudo-booléens (évaluation intégrée à la competition SAT 2005). Tous les détails sur cette évaluation sont disponibles à cette adresse : http://www.cril.univ-artois.fr/PB05

pb2sat+zchaff Olivier Bailleux, Yacine Boufkhad et moi-même avons proposé un codage d'une contrainte pseudo-booléenne sous la forme d'un ensemble de clauses tel que la propagation unitaire sur cet ensemble de clauses permet de restaurer la consistance d'arc généralisée sur la contrainte pseudo-booléenne. Ce codage a été expérimenté dans un solver construit sur le prouveur zChaff et qui a participé à l'évaluation PB05. Voir la page de l'évaluation pour connaître les résultats de ce solveur. Télécharger la version de pb2sat+zchaff qui a participé à l'évaluation. (exécutable statique Linux, compressé avec bzip2)

orsat La librairie orsat a pour but de fournir un ensemble de structures de données, d'algorithmes et d'outils pour faciliter le développement d'algorithmes novateurs reliés de près ou de loin au problème de satisfiabilité (SAT). Ce projet s'inscrit dans une démarche similaire à OpenSAT avec toutefois un accent mis sur la généricité du code. Il s'appuie sur les templates et C++ pour concilier généricité et efficacité. Plus d'informations sur la page du projet.

OpenSAT Avec Gilles Audemard, j'ai participé au projet OpenSAT initié par Daniel Le Berre. Le projet OpenSAT avait pour but de mettre en place une plate-forme de développement pour les problèmes basés sur le test de satisfiabilité. Cette plate-forme se voulait utilisable à deux niveaux différents : du point de vue de l'utilisateur : Cette plate-forme devait permettre de fournir à l'utilisateur des composants logiciels réutilisables qui fournissent une solution aux problèmes autour de SAT. du point de vue du chercheur : La plate-forme OpenSAT devait permettre de fournir au chercheur des implantations standardisées des structures de données et des algorithmes les plus avancés dans le domaine du test de satisfiabilité Une première version de l'implantation de référence de OpenSAT a été développée en quelques mois et a participé à la compétition SAT 2003. Malgré sa jeunesse, cette version a obtenu des résultats tout à fait honorables tout comme le prouveur JQUEST2 également développé dans le cadre du projet OpenSAT. Afin de maximiser l'utilisation de la plate-forme par la communauté, OpenSAT a été développé selon le modèle open-source en utilisant le langage Java afin de faciliter la réutilisation (voir le site du projet). Le développement de cette plate-forme a été abandonné en 2004. Daniel Le Berre poursuit le développement d'une plate-forme Java pour SAT dans le projet SAT4J.

OpenQBF Le projet OpenQBF qui s'inscrit dans le cadre de l'action spécifique QBF se fonde sur la plate-forme OpenSAT pour construire un prouveur pour les formules booléennes quantifiées. Ce projet est développé par D. Le Berre, G. Audemard et O. Roussel. La toute première version du prouveur développé a été soumise à l'évaluation des prouveurs QBF qui a été organisée durant la conférence SAT 2003.

Action Spécifique QBF J'ai participé à l'action spécifique QBF. Pour plus de détails, voir le site de l'action.

Redondances Yacine Boufkhad, Olivier Bailleux et moi-même avons étudié le phénomène de redondance dans les formules booléennes et leur repercussion sur la complexité de la résolution du problème SAT.

Achèvement Mes premiers travaux de recherche sous la direction de Philippe Mathieu portaient sur l'achèvement des bases de connaissances. L'achèvement est une forme de compilation des formules booléennes.