Topics of research

One of the major research in Computer Science and specifically in Artificial Intelligence concerns the knowledge representation and the reasoning from such knowledge. A classical approach is based on the concepts of mathematical logic. The problem is that in computer science practical results are expected: the deduction must be programmed and produce these results in a reasonable time. It is in this very general context that my research is done.

In fact, many practical problems can be represented simply in propositional logic. But the fact remains that the problem SAT (decision problem of the satisfiability a set of constraints built on a finite set of propositional symbols and expressed in the form clausale) is NP-complete. At present, the deduction in propositional calculus can not exhibited a general and efficient algorithm in all cases. Until the P = NP conjecture has not been proved or disproved, we can not know if a algorithm is able to solve efficiently (ie such that the time complexity at the worst case is polynomial) this problem as well as those problems which are naturally related it (automatic proof, logic programming, deductive databases, VLSI, etc).

The main goal of my research is focused on the expansion of the class of treatable problems in practice by the way of new technics, new heuristics or new algorithms increasing the practical efficiency of treatments, or by the discovery of new restrictions for wich it is possible to ensure a resolution in a polynomial time.

My research topics are:

  • Knowledge representation and reasoning
  • Practical resolution of NP-Hard problems
  • Propositional logic: models and algorithms
  • Satifiability problem (SAT)
  • Quantified Boolean Formulas (QBF)
  • Constraint Satifaction Problems (CSP)
  • Compilation of knowledge bases
  • Localization and treatment of inconsistencies
  • Non-monotonic logic
  • Cooperative work and fusion of knowledge bases
  • Validation of knowledge bases systems

My research is done as part of the axis "Algorithms for inference and decision process" of the computer science research center of LENS (CRIL).

back to top

Supervision of students

I have a PES (« Prime d'Excellence Scientifique») since 2009. Previously, I had a PEDR (« Prime d'Encadrement Doctoral et de Recherche ») (obtained in october 2001 and october 2005).

Ph.D thesis

  • Atef Hasni (2010-...), « Squaro vs SAT »
  • Jean-Marie Lagniez (2008-2011), « Satisfiabilité propositionnelle et raisonnement par contraintes : modèles et algorithmes »
  • Cédric Piette (2005-2007), « Techniques algorithmiques pour l'extraction de formules minimales inconsistantes »
  • Olivier Fourdrinoy (2003-2007), « Utilisation de techniques polynomiales pour la résolution pratique d'instances de SAT »
  • Richard Ostrowski (2001-2004), « Reconnaissance et exploitation de propriétés structurelles pour la résolution du problème SAT »
  • David Ansart (2000-2005), « Utilisation et extensions de l'algorithmique pour SAT pour la résolution de différents problèmes d'intelligence artificielle »

Master thesis

  • Ludovic Cornet (2012), « Imposer des contraintes moins restrictives dans un CSP, comparaison d'approches»
  • Atef Hasni (2010), « Imposer des contraintes moins restrictives dans un CSP»
  • Soufien Ghini (2008), « SAT : nouvelles formes de représentation et de résolution »
  • Jean-Marie Lagniez (2008), « Recherche locale pour SAT et UNSAT »
  • Cédric Piette (2005), « Méta-heuristiques pour la détection de noyaux minimalement inconsistants »
  • Jérome Degave (2004), « Symétries et QBF »
  • Olivier Fourdrinoy (2003), « Hybridation des méthodes de résolution pour SAT»
  • Richard Ostrowski (2001), « Résolution de formules booléennes générales »
back to top

Ph.D and HdR Committees

Member of the following Ph.D thesis committees

  • Jean-Marie Lagniez, Thèse de Doctorat de l'Université d'Artois, « Satisfiabilité propositionnelle et raisonnement par contraintes : modèles et algorithmes », december 6th, 2011
  • Olivier Fourdrinoy, Thèse de Doctorat de l'Université d'Artois, « Utilisation de techniques polynomiales pour la résolution pratique d'instances de SAT », november 27th, 2007
  • Cédric Piette, Thèse de Doctorat de l'Université d'Artois, « Techniques algorithmiques pour l'extraction de formules minimales inconsistantes », november 21th, 2007
  • David Ansard, Thèse de Doctorat l'Université d'Artois, « Utilisation et extensions de l'algorithmique pour SAT pour la résolution de différents problèmes d'intelligence artificielle », february 4th 2005
  • Richard Ostrowski, Thèse de Doctorat l'Université d'Artois, « Reconnaissance et exploitation de propriétés structurelles pour la résolution du problème SAT », december 15th 2004
  • Bernard Jurkowiak, Thèse de Doctorat l'Université de Picardie Jules Verne, « Programmation haute performance pour la résolution des problèmes SAT et CSP », october 4th, 2004

Referee of the following Ph.D thesis

  • Benoit Da Mota, Thèse de Doctorat de l'Université d'Angers, « Formules booléennes quantifiées: transformations formelles et calculs parallèles. », december 3rd, 2010

Member of the following HdR committees

  • Laurent Simon, Habilitation à Diriger des Recherches de l'Université de Paris-Sud, « Logique Propositionnelle : un langage simple, des problèmes complexes », december 13th, 2010
back to top

Softwares

  • SUn platform: for "Sat or UNsat platform" is a software developped in C which countains several algorithms for SAT (DPLL, GSAT, WSAT, ...), several heuristics for these algorithms (jeroslow-wang, ffis, random walk strategy, tabu, ...) and several generators of instances (pigeons-hole, dubois, random, ...).
    More details here. The source code of this platform is available by submitting a email.
  • TSAT: for Tabu for SAT. TSAT is a local search algorithm based on GSAT using a tabu strategy to escape of local minima.
    TSAT is presented here and is a part of the SUn platform. [TSAT is also known as TWSAT for Tabu Walk strategy for SAT]
  • DP+LS: is the first efficient hybridization between the DPLL (Davis-Putnam-Logemann-Loveland) algorithm and a local search method like GSAT or TSAT. The local search method is used at each decision node of DPLL for find a model from the partial interpretation constructed by DPLL and/or for choose the next variable to fix in DPLL. This variable is the most falsified ones during the local search.
    This algorithm is detailed here and is a part of the SUn platform.
  • LSAT: is a SAT solver based on a classical DPLL procedure with a pre-processing step which ables to recover and exploit some structural knowledge that is hidden in the conjonctive normal form.
    LSAT has participated at the SAT competitions in 2002 and 2003. In 2002, this solver was in demonstration. In 2003, LSAT has won the first step of the competition on the "handmade" benchmarks and has finished second during the final step.
    More details on LSAT in the dedicated page and here. The source code of LSAT is available here.
  • OMUS: (for One Minimally Unsastifiable Set of clauses) is a core inconsistency extractor of SAT instances. First, the AOMUS (A for approximate) algorithm based on a local search method is used to extract an approximation of a MUS. Then, a exact MUS is obtained by the OMUS algorithm by removing all clauses which does not partipate at the inconsistency.
    This software was mainly developed by Cédric Piette. More derails on (A)OMUS can be found here. The source code is available here.
  • HYCAM: is a tool to extract all MUS of a CNF formula. It is major improvement of an algorithm proposed by M. Liffiton and K. Sakallah. This last algorithm was been hybrided with a local search method for designing HYCAM.
    This software was mainly developed by Cédric Piette. More derails on HYCAM can be found here. The source code is available here.
  • MUSTER: is a tool to extract a fine-grained explanation of the inconsistency of a CSP instance. This is the first software which provides a MUST (Minimally Unsatisfiable Set of Tuples).
    This software was mainly developed by Cédric Piette. More derails on MUSTER can be found here. The source code of MUSTER is available by submitting a email.
  • CDLS: is a local search solver for SAT which exploits the conflict analysis used in CDCL approach (like minisat) to escaping from local minima and proving unsatisfiability.
    This software was mainly developed by Jean-Marie Langniez. The source code of CDLS is available by submitting a email.
  • SatHyS: is a SAT solver based on the hybridization of a local search and an CDCL solver. It's the first hybrid solver which is able to solve more instances than classical local search and CDCL solvers. This software was mainly developed by Jean-Marie Langniez. The source code of SatHyS is available here.
  • FAC-Solver: is an adaptation of SatHyS algorithm to CSP. This software was mainly developed by Jean-Marie Langniez. The source code of CDLS is available by submitting a email.
back to top

Awards

back to top

Research projects

Current Research projects

Past Research projects

  • BQR (Bonus Qualité Recherche) « Utilisation de la programmation par contraintes multi-cœurs pour représenter et manipuler des préférences », 2009-2011.
  • ANR Blanc UNLOC « Local Search and Unsatisfiability »,2009-2011.
  • Franco-Portuguese action, project « MUSICA: Algorithmes pour l'identification et le calcul de sous formules minimales inconsistantes », 2006-2008.
  • AS STIC : « Algorithmique et problématique expérimentale pour l'évaluation de formules booléeens quantifiées » (AS CNRS STIC 83 of RTP 11 « Information et Intelligence : Raisonner et Décider »).
  • Franco-Portuguese action, project « OpenSAT: a platform open source for SAT », 2002-2004.
  • Project « TIC : Traitement Intelligent des Connaissances ». Project of the axis TACT (now TAC) of the CPER Nord/Pas-de-Calais until 2004-2008.
  • Project « Composants intelligents de connaissances » of the IRCICA scientific consortium, until 2009.
  • Project « RESSAC : Aspects algorithmiques de la résolution de problèmes exprimés à l'aide de contraintes » of the PRC-IA, 1995-1996.
  • Projects Ganymède and Ganymède II of the CPER Nord/Pas-de-Calais on « Communication Avancée et Activités Coopératives », 1995-2000.
  • Project « Algorithmes pour l'inférence et la satisfaction de contraintes », GT 1.2 of the PRC-GDR I3 until 2007.
back to top

Committees

Program committees

  • International conference CPAIOR (International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems) in 2012.
  • International conference IJCAI (International Joint Conference on Artificial Intelligence) as senior PC
  • International conference ICTAI (International Conference on Tools with Artificial Intelligence) in 2008, 2009, 2010, 2011.
  • International conference IEEE-IRI (The IEEE International Conference on Information Reuse and Integration) in 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011.
  • National conference RJCIA'00 (« Cinquièmes Rencontres de Jeunes Chercheurs en Intelligence Artificielle »)
  • International conference SCI/ICISAS in 1998, 1999 and 2000.
  • National conference JNPC'97 (« Troisièmes journées sur la Résolution Pratique des Problèmes NP-complets »)
  • International workshop on "Advances in Propositional Deduction" at ECAI'96

Organization committees

Other committees (CoS, CoNRS, ...)

  • External member of the CSE of the University of Picardie Jules Verne (section CNU 27), until 2008.
  • Member of the CSE of the University of Artois (section CNU 25-26-27), 2001-2007.
  • Member of the CoS (Committee of Selection) of the University of Artois (section CNU 27), 2009.
  • Member of the CoS of the University Blaise Pascal of Clermond-Ferrand, 2010.
  • Member of the CoS of the University Joseph Fourrier of Grenoble, 2012.
  • Member of the section 07 of the CoNRS: National Committee of Scientific Research (2008-2012)
back to top

Others Scientific Activities

Referees

Reviewing of papers

  • International Journal on Artificial Intelligence Tools (IJAIT), 2011, 2012.
  • Journal of Automated Reasoning (JAR), 2010, 2011.
  • Journal of Multiple-Valued Logic and Soft Computing (JMVLSC), 2010.
  • Journal of Information Sciences (IS), 2008.
  • Journal of Artificial Intelligence Research (JAIR), 2002.
  • Symposium on Theoretical Aspects of Computer Science (STACS), 2011.
  • International Conference on Software Engineering and Knowledge Engineering (SEKE), 2008.
  • International Joint Conference in Artificial Intelligence (IJCAI), 2003 and 2007.
  • International Conference on Theory and Applications of Satisfiability Testing (SAT), 2005, 2006, 2007, 2010, 2012.
  • European Conference on Artificial Intelligence (ECAI), 2006.
  • Mexican International Conference on Artificial Intelligence (MICAI), 2006.
  • IEEE International Conference on Tools with Artificial Intelligence (ICTAI), 2003, 2004.
  • Colloque sur l'Optimisation et les Systèmes d'Information (COSI), 2007 and 2008.
  • Congrès francophone AFRIF-AFIAl Reconnaissance des Formes et Intelligence Artificielle (RFIA), 2004.
  • Journées Nationales sur la résolution Pratique de Problèmes NP-Complets (JNPC), 2003.

Research Associations

  • Member of SPECIF: French Society for Education and Research in Computer Science.
  • Member of AFIA: French Association for the Artificial Intelligence
  • Member of the administration council (2006-2010) and secretary (2007-2009) of AFPC: French Association for Constraint Programming
  • Member of ACP: International Association for Constraint Programming
back to top

Publications

Go to the dedicated page.

back to top