Olivier ROUSSEL

I am mainly interested by the SAT problem (and by a number of variants). In a few words, the SAT problem consists in determining if an assignation of boolean variables exists such that a given boolean formula evaluates to true.

runsolver The runsolver tool which is used in the competitions to control the resources used by solvers is now freely available under the GPL license.

PB12: the Seventh Competition of Pseudo-Boolean Solvers With Vasco Manquinho, I organize the seventh competition of pseudo-Boolean solvers. All details about this evaluation are available on http://www.cril.univ-artois.fr/PB12

ppfolio ppfolio is a simple tool for emulating the Virtual Best Solver (VBS) on a multicore host. It only runs several solvers in parallel, but nevertheless obtained unexpected results in the 2011 competition. See the details on the ppfolio page.

SAT 2011 Competition With D. Le Berre and L. Simon, I organize the 2011 edition of the SAT competition (see the SAT Competition web site and the detailed results of the competition)

PB11: the Sixth Competition of Pseudo-Boolean Solvers With Vasco Manquinho, I organize the sixth competition of pseudo-Boolean solvers. All details about this evaluation are available on http://www.cril.univ-artois.fr/PB11

PB10: the Fifth Competition of Pseudo-Boolean Solvers With Vasco Manquinho, I organize the fifth competition of pseudo-Boolean solvers. All details about this evaluation are available on http://www.cril.univ-artois.fr/PB10

SAT 2009 Competition With D. Le Berre and L. Simon, I organize the 2009 edition of the SAT competition (see the SAT Competition web site and the detailed results of the competition)

CSC09: fourth competition of CSP solvers With C. Lecoutre and M. Van Dongen, I organize the fourth edition of the competition of CSP solvers (CSP, Max-CSP and WCSP).

PB09: the Fourth Competition of Pseudo-Boolean Solvers With Vasco Manquinho, I organize the fourth competition of pseudo-Boolean solvers. All details about this evaluation are available on http://www.cril.univ-artois.fr/PB09

CPAI08: third competition of CSP solvers I am involved in the organisation of the third competition of CSP solvers (see also this mirror).

SAT 2007 Competition I joined the organizers of the SAT Competition when they decided to run the competition on the framework which I had setup for the PB06, CPAI06 and PB07 evaluations and competition (which is itself derived from the SAT 2005 framework developped by Laurent Simon and Daniel Le Berre). See the SAT Competition web site and the detailed results of the different phases of the SAT 2007 competition

The SAT Game The SAT Game is a funny representation of the SAT problem. Try to solve some easy SAT instances by hand!

PB07: the third Evaluation of Pseudo-Boolean Solvers With Vasco Manquinho, I organize the third evaluation of pseudo-Boolean solvers. All details about this evaluation are available on http://www.cril.univ-artois.fr/PB07

CPAI06: second competition of CSP solvers I got involved in the organisation of the second competition of CSP solvers. You can consult the results of the competition.

A C/C++ parser for the XML 2.0 format of CSP instances I'm currently writing a parser for the XML 2.0 format of CSP instances. See here for information on this parser.

PB06: the second Evaluation of Pseudo-Boolean Solvers With Vasco Manquinho, I organize the second evaluation of pseudo-Boolean solvers. All details about this evaluation are available on http://www.cril.univ-artois.fr/PB06

csp2sat+zchaff My ICTAI'04 paper introduced a knowledge compilation which could be used so that unit propagation on clauses give the same result as maintaining arc-consistency on a CSP problem (an alternative to support encoding). This knowledge compilation has been experimented in a solver based on the zChaff SAT solver and which was submitted to the First International Constraint Satisfaction Solver Competition. Although this solver was a quick hack (it was written in a rush in about three days), it obtained quite good results on binary CSP (and pretty bad result on non binary CSP which is quite normal since the support for n-ary constraints was minimalist). See the competition proceedings to learn about the results of this solver. Download the version of csp2sat+zchaff which was submitted to the evaluation (static Linux executable, bzip2 compressed)

PB05: the first Evaluation of Pseudo Boolean Solvers With Vasco Manquinho, I have organized an evaluation of pseudo-boolean solvers (as a special subtrack of the SAT 2005 competition). All details about this evaluation are available on http://www.cril.univ-artois.fr/PB05

pb2sat+zchaff Olivier Bailleux, Yacine Boufkhad and I have proposed an encoding of a pseudo-boolean constraint as a set of clauses such that using unit propagation on this set of clauses is equivalent to restoring the generalized arc consistency on the initial pseudo boolean constraint. This encoding has been implemented in a solver based on the zChaff SAT solver and which was submitted to the PB05 evaluation. See the evaluation home page to learn about the results of this solver. Download the version of pb2sat+zchaff which was submitted to the evaluation (static Linux executable, bzip2 compressed)

orsat The goal of the orsat library is to provide a set of data structures, algorithms and tools to facilitate the implementation of novative algorithms more or less directly linked to the satisfiability problem (SAT). This project is similar to the OpenSAT project but here the stress is put on the genericity of the code. It is written in C++ and makes intensive use of templates to obtain both genericity and efficiency. More information on the project page.

OpenSAT Sorry, no translation available so far ! 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 Sorry, no translation available so far ! 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.

QBF Specific Action I was involved in the QBF specific action. For more details, see the action web site.

Redundancy Yacine Boufkhad, Olivier Bailleux and I have studied redundancy in boolean formulae and its impact on the difficulty to solve the SAT problem.

Achèvement Sorry, no translation available so far ! 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.