# Des Données aux Connaissances : Modèles et Algorithmes

Saïd Jabbour

► To cite this version:

Saïd Jabbour. Des Données aux Connaissances : Modèles et Algorithmes. Informatique [cs]. Université d'Artois, 2018. tel-04284476

HAL Id: tel-04284476

https://theses.hal.science/tel-04284476

Submitted on 14 Nov 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
UNIVERSITÉ D'ARTOIS

ECOLE DOCTORALE SPI 072
SCIENCES POUR L'INGÉNIEUR

# Mémoire

pour l'obtention du titre de

## Habilitation à Diriger les Recherches

de l'Université d'Artois

Mention : INFORMATIQUE

Présentée par

Said JABBOUR

# Des Données aux Connaissances : Modèles et Algorithmes

Soutenue publiquement le
6 décembre 2018

## Composition du jury :

* Rapporteurs :
  Sihem AMER-YAHYA (Directrice de Recherche)
  Philippe-Viger FOURINER (Professeur)
  Felip MANYA (Professeur)

LIG - CNRS, Université Grenoble Alpes
Harbin Institute of Technology (Chine)
IIIA-CSIC (Espagne)

* Examinateurs :
  Anthony HUNTER (Professeur)
  Jean-Charles RÉGIN (Professeur des Universités)
  Philippe BESNARD (Directeur de Recherche)

University College London (UK)
Université de Nice-Sophia Antipolis
IRIT - CNRS, Université Paul Sabatier
# Table des matières

<table><tr><td>1</td><td>Introduction générale</td><td>1</td></tr><tr><td>2</td><td>Satisfiabilité propositionnelle</td><td>5</td></tr><tr><td>2.1</td><td>Introduction</td><td>5</td></tr><tr><td>2.2</td><td>Définitions et notations</td><td>5</td></tr><tr><td>2.3</td><td>Approches de résolution du problème SAT</td><td>6</td></tr><tr><td>2.4</td><td>Élimination de symétries</td><td>7</td></tr><tr><td>2.5</td><td>Résolution séquentielle</td><td>8</td></tr><tr><td>2.5.1</td><td>Amélioration du schéma d'apprentissage de clauses</td><td>8</td></tr><tr><td>2.5.2</td><td>Simplification des bases des clauses apprises</td><td>8</td></tr><tr><td>2.6</td><td>Résolution parallèle du problème SAT</td><td>9</td></tr><tr><td>2.6.1</td><td>Approche portfolio</td><td>9</td></tr><tr><td>2.6.2</td><td>Échange de clauses</td><td>10</td></tr><tr><td>2.6.3</td><td>Intensification et diversification</td><td>11</td></tr><tr><td>2.6.4</td><td>Parallèle & déterminisme</td><td>11</td></tr><tr><td>2.6.5</td><td>Approche distribuée</td><td>12</td></tr><tr><td>2.7</td><td>Énumération de modèles</td><td>12</td></tr><tr><td>2.7.1</td><td>Énumération de tous les modèles</td><td>12</td></tr><tr><td>2.7.2</td><td>Enumeration des impliquants premiers</td><td>13</td></tr><tr><td>2.7.3</td><td>Enumeration des modèles Top-k</td><td>14</td></tr><tr><td>2.8</td><td>Contraintes de cardinalité & problème des pigeons</td><td>15</td></tr><tr><td>2.9</td><td>Contrainte de cardinalité conditionnelle</td><td>17</td></tr><tr><td>2.10</td><td>Représentation compacte</td><td>17</td></tr><tr><td>2.10.1</td><td>Forme normale conjonctive</td><td>18</td></tr><tr><td>2.10.2</td><td>Contraintes tables</td><td>19</td></tr><tr><td>3</td><td>Fouille de données & Clustering</td><td>21</td></tr><tr><td>3.1</td><td>Introduction</td><td>21</td></tr><tr><td>3.2</td><td>Définitions et cadre formel</td><td>21</td></tr><tr><td>3.3</td><td>Fouille des itemsets</td><td>23</td></tr><tr><td>3.3.1</td><td>Approche symbolique</td><td>24</td></tr><tr><td>3.3.2</td><td>Solveur adaptatif</td><td>25</td></tr><tr><td>3.3.3</td><td>Motifs maximaux</td><td>25</td></tr><tr><td>3.3.4</td><td>Décomposition & approche parallèle</td><td>26</td></tr><tr><td>3.3.5</td><td>Symétries et motifs ensemblistes</td><td>27</td></tr><tr><td>3.3.6</td><td>Modèles Top-k et motifs Top-k</td><td>28</td></tr><tr><td>3.3.7</td><td>Motifs skyPatterns</td><td>29</td></tr><tr><td>3.3.8</td><td>Motifs ensemblistes sous incertitude</td><td>29</td></tr><tr><td>3.4</td><td>Fouille de règles d'association</td><td>30</td></tr><tr><td>3.4.1</td><td>Approche symbolique</td><td>30</td></tr></table>
<table><tbody><tr><td>3.4.2</td><td>Règles non-redondantes</td><td>31</td></tr><tr><td>3.5</td><td>Fouille de motifs séquentiels</td><td>32</td></tr><tr><td>3.5.1</td><td>Définitions et cadre formel</td><td>32</td></tr><tr><td>3.5.2</td><td>Approche symbolique</td><td>33</td></tr><tr><td>3.6</td><td>Clustering de formules booléennes</td><td>35</td></tr><tr><td><b>4</b></td><td><b>Graphes</b></td><td><b>39</b></td></tr><tr><td>4.1</td><td>Introduction</td><td>39</td></tr><tr><td>4.1.1</td><td>Définitions et notations</td><td>39</td></tr><tr><td>4.2</td><td>Détection de communautés</td><td>40</td></tr><tr><td>4.2.1</td><td>Communauté k-liée centrée</td><td>41</td></tr><tr><td>4.2.2</td><td>Communauté k-clique-star</td><td>42</td></tr><tr><td>4.2.3</td><td>Compression de graphes à base contraintes pseudo-booléennes</td><td>43</td></tr><tr><td><b>5</b></td><td><b>Représentation de connaissances & Raisonnement</b></td><td><b>45</b></td></tr><tr><td>5.1</td><td>Introduction</td><td>45</td></tr><tr><td>5.2</td><td>Gestion et mesure de l'incohérence</td><td>45</td></tr><tr><td>5.2.1</td><td>Définitions et notations</td><td>46</td></tr><tr><td>5.2.2</td><td>Mesure de degré d'incohérence via les preuves minimales</td><td>46</td></tr><tr><td>5.2.3</td><td>Additivité restreinte</td><td>47</td></tr><tr><td>5.2.4</td><td>Sous-additivité</td><td>48</td></tr><tr><td>5.2.5</td><td>Dominance faible</td><td>49</td></tr><tr><td>5.2.6</td><td>Restauration de la cohérence</td><td>50</td></tr><tr><td>5.3</td><td>Théorie de l'argumentation</td><td>51</td></tr><tr><td>5.3.1</td><td>Enumeration des extensions Top-k</td><td>51</td></tr><tr><td>5.3.2</td><td>Raisonnement sur des ontologies conflictuelles</td><td>52</td></tr><tr><td><b>6</b></td><td><b>Composition de services web</b></td><td><b>53</b></td></tr><tr><td>6.1</td><td>Introduction</td><td>53</td></tr><tr><td>6.2</td><td>Définitions et cadre formel</td><td>54</td></tr><tr><td>6.3</td><td>Composition de services web à base d'ensembles minimaux incohérents</td><td>55</td></tr><tr><td>6.4</td><td>Composition de services web à base d'impliquants premiers</td><td>55</td></tr><tr><td><b>7</b></td><td><b>Bilan et perspectives</b></td><td><b>57</b></td></tr><tr><td><b>8</b></td><td><b>Activités de recherche</b></td><td><b>61</b></td></tr><tr><td>8.1</td><td>Valorisation scientifique</td><td>61</td></tr><tr><td>8.1.1</td><td>Distinctions</td><td>61</td></tr><tr><td>8.1.2</td><td>Logiciels</td><td>61</td></tr><tr><td>8.1.3</td><td>Distinctions : compétitions de solveurs</td><td>62</td></tr><tr><td>8.1.4</td><td>Brevets</td><td>62</td></tr><tr><td>8.1.5</td><td>Collaboration industriels (passées et en cours)</td><td>63</td></tr><tr><td>8.1.6</td><td>Projets de recherche nationaux</td><td>63</td></tr><tr><td>8.2</td><td>Encadrement de la recherche et animation scientifique</td><td>64</td></tr><tr><td>8.2.1</td><td>Activités d'encadrement</td><td>64</td></tr></tbody></table>
<table><tr><td>8.2.2</td><td>Membre de comités de programme</td><td>65</td></tr><tr><td>8.2.3</td><td>Relecture d'articles</td><td>65</td></tr><tr><td>8.2.4</td><td>Expertise de projets</td><td>66</td></tr><tr><td>8.2.5</td><td>Collaborations internationales et bourses de thèse</td><td>66</td></tr><tr><td>8.2.6</td><td>Collaborations nationales</td><td>66</td></tr><tr><td>8.2.7</td><td>Responsabilités collectives</td><td>66</td></tr><tr><td colspan="2"><strong>Bibliographie</strong></td><td><strong>69</strong></td></tr><tr><td>9</td><td><strong>Publications jointes</strong></td><td><strong>87</strong></td></tr></table>
Table des figures

<table><tr><td>2.1</td><td>Représentation compacte de contraintes</td><td>17</td></tr><tr><td>3.1</td><td>Visualisation de l'espace des itemsets possibles</td><td>23</td></tr><tr><td>3.2</td><td>Arbre des chemins de guidage</td><td>27</td></tr><tr><td>4.1</td><td>Exemples de graphes</td><td>43</td></tr><tr><td>4.2</td><td>Quelques classes de graphe</td><td>44</td></tr><tr><td>5.1</td><td>De l'hypergraphe au graphe des MUSes de K</td><td>49</td></tr></table>
# Liste des tableaux

<table><tr><td>3.1 Deux représentations d'une table des transactions</td><td>22</td></tr></table>
## CHAPITRE 1

# Introduction générale

Mes thématiques de recherche s'inscrivent à la frontière de plusieurs domaines différents mais de premier plan incluant l'Intelligence Artificielle (IA), la fouille de données et les systèmes d'information. Elles peuvent être caractérisées par les mots clés suivants : programmation par contraintes, représentation des connaissances, la problématique de raisonnement sur des ontologies conflictuelles (incohérentes et/ou inconsistantes) via l'argumentation déductive, fouille de motifs sous contraintes, clustering, détection de communautés, compression de données et composition de services web. Cette multidisciplinarité a plusieurs motivations et sources d'explications. Tout d'abord ma volonté à explorer de nouvelles thématiques afin de mettre en lumière leurs connexions, leurs complémentarités et leurs spécificités en vue d'une réelle fertilisation croisée. De plus, bien que les formalismes ou les modèles de représentation utilisés ne sont pas les mêmes, certaines interrogations et problématiques étudiées dans ces domaines sont similaires et récurrentes. On peut citer par exemple la problématique de la qualité des données, l'algorithmique d'énumération de structures combinatoire, les paradigmes utilisés pour l'intégration ou la fusion de données/connaissances et la détection d'incohérences. Une autre motivation vient de la place de plus en plus grande qu'occupent les recherches autour de l'analyse et de la valorisation des données via des techniques issues de la fouille de données et de l'apprentissage automatique. Ces dernières ont contribué à élargir considérablement l'éventail des applications qui touche à de nouveaux secteurs dans le monde industriels et des services. Au-delà de ces motivations indéniables, mon ouverture à d'autres thématiques de recherche s'est concrétisée au gré des rencontres et des projets de recherche multidisciplinaires auxquels j'ai participé.

Dans un ordre chronologique, mes premiers travaux ont porté sur les problèmes de décision ou d'optimisation associés à l'inférence et à la prise de décision en intelligence artificielle (axe II du CRIL). Ces problèmes sont typiquement intraitables, i.e. il n'existe usuellement pas d'algorithme déterministe en temps polynomial dans le pire des cas pour ceux-ci (et la théorie de la complexité pousse à conjecturer fortement qu'il n'en existera jamais). Cette difficulté calculatoire impose le développement de solutions palliatives ayant pour objectif d'élargir la classe des problèmes traitables en pratique, en permettant la résolution d'instances de tailles de plus en plus grande, dans un laps de temps raisonnable. Dans ce contexte, je me suis particulièrement intéressé à deux problèmes représentatifs de cette difficulté calculatoire, il s'agit du problème de la satisfiabilité d'une formule propositionnelle (SAT) et de son extension les formules booléennes quantifiées (QBF), deux exemples de références de la classe des problèmes NP et PSPACE complet respectivement. Mes travaux de recherche autour de ces deux problèmes ont portés principalement sur les aspects algorithmiques incluant l'apprentissage de clauses, les techniques de simplifications, les stratégies de résolution et la détection et l'exploitation de propriétés structurelles des problèmes traités (e.g. symétries, dépendances fonctionnelles). Nos contributions ont donné lieu à divers solveurs parmi les plus performants, attesté par les diverses médailles que nous avions obtenue lors des compéti-
tions internationales. Nous avons donc eu la chance de participer à cette effervescence particulière qu'a connu la résolution du problème SAT ces dernières décennies, dont les résultats ont permis un réel passage à l'échelle. Les solveurs SAT modernes sont aujourd'hui capables de résoudre efficacement des instances de SAT issues de problèmes réels avec plusieurs millions de variables et de clauses. Ce saut qualitatif a contribué à élargir les domaines d'applications traditionnels de SAT (vérification formelle de logiciels et de matériels) à d'autres champs d'applications comme la planification, la bio-informatique et la cryptographie. La modélisation d'applications du monde réel en logique propositionnelle et l'extension des résultats de SAT à des problématiques autour de SAT est devenue aujourd'hui une pratique courante. Cette nouvelle situation suscite un réel débat sur le fait que la complexité au pire cas généralement privilégié par la théorie de la complexité est loin de refléter la réalité de la résolution de problèmes en pratique (voir article de Moshe Y. Vardi "On P, NP, and computational complexity" ACM 2010).

Depuis ma thèse, plusieurs rencontres et faits marquants ont contribué à concrétiser mon projet d'ouverture à d'autres thématiques de recherche. Notre expertise reconnue sur la résolution du problème de la satisfiability propositionnelle a fortement intéressé l'équipe "Constraint Reasoning" de Microsfot Research Cambridge (UK) dirigée par Youssef Hamadi. Dans le cadre d'un stage à Cambridge et d'un postdoctorat au laboratoire commun Inria-Microsoft à Paris, je me suis intéressé au développement d'approches parallèles pour SAT exploitant les architectures multicœurs. Dans ce cadre, nous avons proposé la première approche parallèle de type portfolio avec de nombreuses améliorations ayant permis de dominer la compétition SAT (parallel track) de 2008 à 2011. Cette approche a ensuite été intégré dans le solveur SMT (Sat Modulo Theory) Z3 développé par Leonardo de Moura à Microsoft, un solveur état-de-l'art, très utilisé dans la vérification de logiciels. Ce succès a contribué grandement au regain d'intérêt pour le développement d'approches parallèles pour SAT et CP.

Le CRIL est un laboratoire structuré autour de deux axes complémentaires, la représentation des connaissances et raisonnements (Axe 1), et Algorithmes pour l'inférence et contraintes (Axe 2). Cette proximité entre les deux axes a été propice à mon intérêt pour la thématique de la représentation des connaissances. Nous avons proposé plusieurs contributions à deux des problématiques de cet axe : la théorie de l'argumentation et les mesures d'incohérentes. Pour l'argumentation, nous avons entre autres introduit des relations de préférences, exprimés en fonction des relations d'attaque et de défense entre arguments, pour le calcul des Top-k extensions non conflictuelles. Pour quantifier l'incohérence des bases de connaissances, nous avons proposés de nouvelles mesures et de nouvelles propriétés que toute mesure d'incohérence est censée vérifier. Nos mesures prennent mieux en compte la structure de l'hypergraphe induit par les sous-formules minimalement incohérences. Elles nous ont permis d'exhiber de nouveaux problèmes comme celui du set packing fermé ou l'extension du problème "Symmetric Intersecting Monotone UNSAT".

Un autre fait marquant ayant influencé mes travaux récents est sans aucun doute le projet ANR Défi DAG<fnref n="1" /> "Approches déclaratives pour l'énumération de motifs intéressants à partir de données" 2009-2013. Ce projet auquel j'ai eu la chance de participer a un double objectif, celui de (1) définir des langages déclaratifs de haut niveau (logiques ou algébriques) pour exprimer et représenter les problèmes de fouille de données et (2) exhiber des sous-classes de problèmes pour lesquelles il existe des algorithmes génériques et efficaces. Les nombreux résultats que nous

<footnote n="1">1. https://projet.liris.cnrs.fr/dag/</footnote>
avions obtenus dans le cadre de ce projet multidisciplinaire regroupant le CRIL (Programmation par contraintes/logique), le LIRIS (Bases de données/Fouille de données) et le LIMOS (Algorithmique d'énumération/théorie des graphes), ont été à l'origine de la création d'un groupe de recherche au CRIL autour de la fouille de données et contraintes. Dans ce cadre et par fertilisation croisée entre la fouille de données et l'intelligence artificielle et plus particulièrement CP/SAT, nous avons proposé diverses formulations des problèmes de fouille de données en SAT, incluant la fouille d'itemsets fréquents, maximaux ou fermés, l'énumération de règles d'association et de ses nombreuses variantes et la fouille de séquences. Les apports de cette fertilisation croisée sont particulièrement illustrés par deux de nos contributions, à savoir (1) l'extension des symétries (largement étudiées en SAT/CP) en fouille de données, (2) l'exploitation de la fouille de données pour compressor des formules booléennes ou des contraintes relationnelles (ou en extension) et (3) la mise en œuvre de nouvelles techniques de clustering d'objets complexes représentés par des formules booléennes. Les effets de bord de cette ouverture thématique sont nombreux et enrichissants. Le premier exemple vient du fait que la modélisation de problèmes de fouilles de données en logique propositionnelle fait souvent intervenir des contraintes linéaires 0/1 (contraintes de cardinalité et contraintes pseudo booléennes) dont le codage SAT a fait l'objet de nombreux travaux. Dans ce cadre, nous avons proposé une formulation de ce type de contraintes en utilisant le fameux principe des tiroirs (ou Pigeon-Hole Problem). Le second vient de notre étude sur la compression de formules booléennes en particulier de clauses binaires. Ces dernières admettent une représentation sous forme de graphes. Nous avons observé que les cliques ou bi-cliques de clauses binaires représentent des inéquations linéaires 0/1 particulières. Cette observation est à l'origine de la proposition de nouvelles classes de graphes à l'origine de notre approche de compression de graphes par une représentation sous forme d'une disjonction d'inéquations linéaires 0/1 dont les solutions donnent les arêtes du graphe originale. Notre approche de compression par l'exploitation de certaines classes de graphes admet des connexions avec une autre thématique de recherche importante : la détection de communautés. Nous avons proposé diverses approches déclaratives et spécialisés en exploitant diverses classes de graphes.

La description (non exhaustive) chronologique ci-dessus est donnée pour illustrer mes ouvertures thématiques qui vont de SAT aux graphes et à la détection de communautés en passant par la représentation des connaissances et la fouille de données. Cette ouverture thématique se poursuivra avec le projet QDoSSI « Qualité des données multi-sources : un double défi pour les sciences sociales et les sciences de l'informatique » financé par la mission pour l'interdisciplinarité du CNRS depuis 2016. L'objet étant d'analyser les données (structurés et non structurés) traitant des migrations internationales afin de comprendre les processus à l'œuvre dans la construction des parcours migratoires. Ce projet offre donc une excellente opportunité pour contribuer à d'autres thématiques comme la qualité des données, la fouille de texte, la fouille de graphes attribués et la visualisation de données.

Une synthèse détaillée de mes travaux et des perspectives sera donnée dans la suite de ce mémoire d'habilitation à diriger les recherches qui est organisé en 10 chapitres.

Le second chapitre est consacré à nos travaux en lien avec la résolution effective du problème SAT comprenant notre approche parallèle portfolio, les travaux sur l'énumération de modèles, l'amélioration des encodages et la compression de formules. Dans le troisième chapitre nous reviendrons sur nos contributions en fouille de données. Nous parlerons de ceux effectués pour la fouille des motifs ensemblistes et séquentiels et les différentes améliorations proposées. Nous
présentons également le problème de clustering d'objets représentés sous forme de formules pro-
positionnelle et les solutions proposées. Le quatrième chapitre est dédié à nos travaux dans les
graphes. Nous abordons deux problématiques différentes à savoir la détection de communau-
tés et la question de trouver des représentations compactes. Nous parlerons notamment de notre
nouvelle technique de compression de graphes à base de contraintes pseudo-booléennes. Le cin-
quième chapitre adresse nos contributions dans le cadre de la représentation de connaissances.
Nous présentons les travaux dans le cadre de la gestion de l'incohérence mais également ceux en
lien avec l'argumentation. Le septième chapitre décrit les approches proposées dans le cadre de la
composition des services web. Nous présentons les deux approches visant à trouver une composi-
tion optimale en prenant en compte la qualité de service. Nous concluons, dans le chapitre neuf, la
description des travaux par un chapitre sur le bilan et les perspectives de nos travaux de recherche.
Le dernière chapitre est consacré à la description de mes activités de recherche annexes.
# Satisfiabilité propositionnelle

## 2.1 Introduction

Ce premier chapitre est consacré à une description synthétique de mes contributions dédiées à la résolution du problème de satisfiabilité propositionnelle (SAT). Nous commençons par introduire un ensemble de notations et de définitions élémentaires, suivi par un bref aperçu de solveurs SAT modernes. La suite du chapitre est consacrée à la description de nos travaux dans ce domaine. Ces contributions peuvent être scindées naturellement en cinq catégories : (i) les approches dédiées à l'amélioration de la résolution du problème SAT, (ii) l'utilisation du parallélisme en satisfiabilité propositionnelle, (iii) l'énumération des modèles d'une formule CNF, (iv) l'encodage de la contrainte de cardinalité (conditionnelle) et finalement (v) la compression de formules booléennes et contraintes tables.

## 2.2 Définitions et notations

Dans cette section, nous allons présenter les principaux éléments de la logique propositionnelle nécessaire pour la suite du manuscrit.

Soit $\mathcal{L}$ un langage propositionnel défini à partir d'un ensemble fini $\mathcal{PS}$ de symboles propositionnels $(p, q, r, \text{etc.})$. L'ensemble des formules est défini de manière inductive à partir de $\mathcal{PS}$, la constante $\perp$ (*Faux*), la constante $\top$ (*Vrai*), et utilisant les connecteurs logiques usuels $\neg$, $\wedge$, $\vee$, $\to$ ainsi que le connecteur d'équivalence $\leftrightarrow$. Pour chaque deux formules propositionnelles $\Phi$ et $\Psi$ de $\mathcal{L}$, le connecteur $\leftrightarrow$ est défini par $\Phi \leftrightarrow \Psi \equiv (\Phi \to \Psi) \wedge (\Psi \to \Phi)$. Dans la suite, nous nous référons à l'ensemble des symboles de $\mathcal{PS}$ qui apparaissent dans la formule $\Phi$ comme $S(\Phi)$.

Étant donnée une formule $\Phi \in \mathcal{L}$, une interprétation booléenne $\mathcal{B}$ de $\Phi$ est une fonction de $S(\Phi)$ dans $\{0, 1\}$. Soient deux formules $\Phi, \Psi \in \mathcal{L}$, nous avons les équivalences suivantes : $\mathcal{B}(\perp) = 0, \mathcal{B}(\top) = 1, \mathcal{B}(\neg\Phi) = 1 - \mathcal{B}(\Phi), \mathcal{B}(\Phi \wedge \Psi) = \min(\mathcal{B}(\Phi), \mathcal{B}(\Psi)), \mathcal{B}(\Phi \vee \Psi) = \max(\mathcal{B}(\Phi), \mathcal{B}(\Psi)), \text{et } \mathcal{B}(\Phi \to \Psi) = \max(1 - \mathcal{B}(\Phi), \mathcal{B}(\Psi)).$

Un modèle d'une formule $\Phi \in \mathcal{L}$ est une interprétation booléenne $\mathcal{B}$ qui satisfait $\Phi$, i.e., $\mathcal{B}(\Phi) = 1$. $M(\Phi)$ représente l'ensemble des modèles de la formule $\Phi$, i.e., $M(\Phi) = \{M \mid M \models \Phi\}$. Une formule $\Phi$ est satisfiable ssi $M(\Phi) \neq \emptyset$. Soient $X \subseteq S(\Phi)$ et $\mathcal{B} \in M(\Phi)$, nous définissons $\mathcal{B}^X = \{x \in X \mid \mathcal{B}(x) = 1\}$ et $M^X(\Phi) = \{\mathcal{B}^X \mid \mathcal{B} \in M(\Phi)\}$. Une interprétation $\mathcal{B}$ de $\Phi$ est dite impliquant premier (PI en court) si et seulement si pour tout littéral $a \in \mathcal{B}$, $\mathcal{B} \setminus \{a\} \not\models \Phi$. Nous notons par $\mathrm{PI}(\Phi)$ la disjonction de tous les impliquants premiers de $\Phi$. Évidemment, $\mathrm{PI}(\Phi)$ est logiquement équivalent à $\Phi$. Nous utilisons le symbole $\vdash$ pour désigner la relation de déduction ou d'inférence. Notons que le symbole $\vdash$ n'est pas un nouveau symbole du langage mais appartient au métalangage. $\vdash_*$ désigne la relation de déduction modulo la propagation unitaire.
Une formule sous *forme normale conjonctive* (CNF) est une conjonction (finie) de clauses. Une *clause* est une disjonction (finie) de littéraux. Un *littéral* est soit une variable propositionnelle $x \in \mathcal{PS}$ ou sa négation $\neg x$. Notons également que toute formule propositionnelle peut être transformée en une formule CNF équivalente pour la satisfiabilité, en utilisant l'encodage linéaire de Tseitin [Tseitin 1968]. Une clause *c* est dite *impliqué premier* d'une formule satisfiable $\Phi$ si $\Phi \vdash c$, *c* n'est pas tautologique, et pour toute clause $c' \subset c$, $\Phi \nvDash c'$.

Le problème de la satisfiabilité propositionnelle, appelé SAT, est le problème de décision qui consiste à déterminer si une formule CNF est satisfiable ou non. Ce problème a été montré NP-complet [Cook 1971]. Depuis les années soixante et les fameux travaux de Davis et Puttnam [Davis et al. 1962], le problème SAT a fait l'objet de nombreux travaux sur le plan théorique et pratique. Plusieurs algorithmes ont été proposés et raffinés tout le long des décennies passées. Ces recherches ont aboutis à des procédures (solveurs SAT modernes) efficaces en pratique conduisant à une vraie révolution dans la résolution des instances SAT et un succès indéniable sur le plan industriel. Au delà de l'application phare qui est la vérification formelle (Bounded Model Checking) [Clarke et al. 2001], le champ d'application de SAT n'a cessé de s'accroître au cours des années allant de la bio-informatique à la correction de circuits électroniques vis-à-vis de leur spécification en passant par l'ordonnancement [Crawford & Baker 1994], et la fouille de données [Boudane et al. 2016]. Cette expansion du champ d'application s'accompagne par une difficulté croissante dûe à la structure intrinsèque de certains problèmes mais parfois à la simplicité du langage propositionnel menant à des formules de plus en plus volumineuses.

## 2.3 Approches de résolution du problème SAT

Les algorithmes dédiés à la résolution du problème SAT peuvent être scindés en deux principales catégories : complet et incomplet. Dans la catégorie des solveurs complets, le solveur dit solveur SAT moderne (Conflict Driven Clause Learning) [Marques-Silva & Sakallah 1996, Moskewicz et al. 2001] est l'archetype des solveurs de cette catégorie et le symbole de leurs succès. C'est une amélioration notable de l'algorithme DPLL [Davis et al. 1962].

Un algorithme SAT de type CDCL est une procédure de recherche arborescente de type retour-arrière (backtrack) qui développe un arbre binaire. En chaque nœud, une variable de la formule est choisie et affectée à l'une de ces valeurs de vérités suivi de la propagation unitaire. Si tous les littéraux sont affectés ou propagés sans contradiction, alors la formule est déclarée satisfiable et l'interprétation courante est un modèle de la formule. Dans le cas contraire, un conflit a lieu, i.e., une clause est rendue fausse par l'interprétation courante (tous ces littéraux sont affectés à *faux*).

CDCL [Zhang et al. 2001] se distingue par la manière de capturer la propagation unitaire en utilisant des structures intelligentes ("Watched Literals"), de traiter les conflits (application de la résolution en utilisant les graphes d'implications), et par l'utilisation des heuristiques de choix de variables (VSIDS) pour circonscrire la partie conflictuelle de l'espace de recherche. Cette procédure a été également enrichie par des méthodes visant à améliorer la résolution en recommençant régulièrement la recherche (redémarrage) pour diversifier la recherche et en maintenant une base de clauses apprises de qualité (supprimer régulièrement des clauses jugées non pertinentes).
## 2.4 Élimination de symétries

Dans cette section, nous parlons de symétries, un concept largement étudié en littérature et qui a fait l'objet de certains de nos travaux. La symétrie est un concept fondamental en informa- tique, mathématiques, physiques et plein d'autres domaines. Elle existe dans divers problèmes réels. Les symétries sont communément exploitées dans la résolution de problèmes combina- toires, tels que les problèmes d'ordonnancement. Par exemple, dans un problème d'ordonnance- ment où certaines machines peuvent être interchangeables, partant d'un ordonnancement valide, on peut en obtenir un autre valide en permutant ces machines. Exploiter les symétries permet de réduire le coût de la recherche de solutions, en évitant d'explorer des branches symétriques de l'espace de recherche. Beaucoup de travaux ont ainsi porté sur les symétries dans les pro- blèmes de satisfaction de contraintes (CSP) [Gent & Smith 2000, Cohen et al. 2006], satisfaisa- bilité propositionnelle [Benhamou & Sais 1994, Crawford 1992], en formules booléennes quan- tifiées [Audemard et al. 2007], et en recherche opérationnelle [Margot 2003, Liberti 2012].

Tout d'abord, introduisons quelques concepts de la théorie des groupes. Un groupe $(G, \circ)$ est un ensemble fini $G$ avec un opérateur binaire associatif $\circ : G \times G \to G$ admettant un élément neutre et un élément inverse. L'ensemble de toutes les permutations $P$ sur un ensemble fini $E$ associé à l'opérateur de composition $\circ$, noté $(P, \circ)$, forme un groupe. En outre, chaque permutation $\sigma \in P$ peut être représentée par un ensemble de cycles $\{c_1...c_n\}$ tel que chaque cycle $c_i$ est un ensemble d'éléments de $E$ $(l_{i_1}...l_{i_n})$ avec $\forall 1 \le k < n_i, \sigma(l_{i_k}) = l_{i_{k+1}}$ et $\sigma(l_{i_n}) = l_{i_1}$.

Soient $\Phi$ une formule CNF et $\sigma$ une permutation sur $\text{Lit}(\Phi)$. On peut étendre le concept de permutation $\sigma$ à $\Phi$ comme suit : $\sigma(\Phi) = \{\sigma(c) \mid c \in \Phi\}$ et $\sigma(c) = \{\sigma(l) \mid l \in c\}$.

**Définition 1.** Soient $\Phi$ une formule CNF et $\sigma$ une permutation sur les littéraux de $\Phi$. $\sigma$ est une symétrie de $\Phi$ si elle satisfait les conditions suivantes :

$$ \neg \sigma(\neg x) = \neg \sigma(x), \forall x \in \mathcal{L}(\Phi), $$

$$ \neg \sigma(\Phi) = \Phi. $$

Par conséquent, une symétrie $\sigma$ définit une relation d'équivalence sur l'ensemble des affecta- tions possibles. L'élimination des symétries consiste à supprimer toutes les interprétations symé- triques sauf une dans chaque classe d'équivalence. Usuellement, l'élimination d'une symétrie $\sigma = (x_1, y_1)(x_2, y_2)...(x_n, y_n)$ s'effectue par ajout de contraintes appelées SBP (Symmetry Breaking Predicates) [Crawford 1992, Crawford et al. 1996, Aloul et al. 2003a, Aloul et al. 2003b, Walsh 2006] définit formellement comme suit :

$$ (x_1 \le y_1) $$

$$ (x_1 = y_1) \rightarrow (x_2 \le y_2) $$

$$ (x_1 = y_1) \land (x_2 = y_2) \land \dots \land (x_{n-1} = y_{n-1}) \rightarrow (x_n \le y_n) $$

L'ajout de ces contraintes permet de préserver l'équivalence pour la satisfiabilité entre la for- mule originale et celle augmentée par le SBP. De plus, la suppression d'un ensemble de symétries s'effectue en ajoutant le SBP associé à chacune d'entre elles.
## 2.5 Résolution séquentielle

Durant les années qui ont suivi ma thèse, nous nous sommes intéressés à améliorer la résolution effective du problème SAT. Les limites observées dans sa résolution nous ont encouragés à chercher d'autres alternatives capables de rendre la résolution plus efficace. Nous avons explorés plusieurs directions de recherche allant de l'amélioration du schéma d'apprentissage des clauses à l'introduction d'une approche parallèle. Nous nous somme également intéressés aux techniques de pré-traitement en amont de la résolution en explorant des encodages de certaines contraintes usuellement utilisées lors des encodages ou en proposant des représentations plus compactes.

Dans la suite nous présentons les travaux réalisés en lien étroit avec la résolution du problème SAT.

### 2.5.1 Amélioration du schéma d'apprentissage de clauses

L'ajout des clauses obtenues par résolution à chaque conflit (apprentissage de clauses) permet d'éviter de revisiter des sous-espaces de recherche déjà exploré. Toutefois, le nombre de ces clauses est connu pour être exponentiel dans le pire cas. Dans [Jabbour 2009, Hamadi et al. 2009, Jabbour et al. 2013b, Hamadi et al. 2012, Hamadi et al. 2016], nous nous sommes intéressés à améliorer le schéma d'apprentissage de clauses en proposant plusieurs modèles. En effet, lors de l'encodage de certains problèmes d'application vers SAT, et afin de réduire la taille de ce dernier, souvent des variables supplémentaires sont ajoutées. Ces variables sont généralement exprimées en fonction de celles du problème initial par le biais de fonctions booléennes. Ces fonctions booléennes de la forme $y \leftrightarrow f(x_1, ..., x_n)$, $f \in \{\wedge, \vee\}$ peuvent êtres découvertes soit syntaxiquement ou sémantiquement en utilisant la propagation unitaire [Grégoire et al. 2004]. Dans [Jabbour et al. 2013b], nous avons proposé d'améliorer la qualité des clauses apprises en substituant certaines de leurs variables par leurs définitions. Le but est de faire en sorte que les contraintes portent plus sur les variables originales du problème.

Améliorer le schéma d'apprentissage de clauses a fait également l'objet d'un autre travail [Hamadi et al. 2009]. Dans ce dernier, nous avons exploré dans quelle mesure utiliser le graphe d'implications pour déduire de nouvelles clauses utiles pour la recherche i.e., ayant du pouvoir de propagation. Dans [Pipatsrisawat & Darwiche 2008], les auteurs ont exploré cette notion en considérant les clauses assertives (au moment de leur génération) en se basant sur une forme de résolution particulière appelée *merge résolution* [Andrews 1968], i.e., $\Phi \vdash x \vee y \vee \alpha$ et $\Phi \wedge \neg x \wedge \neg \alpha \nu_*$ y. Dans [Jabbour et al. 2013b], nous avons proposé de générer par résolution des clauses particulières dites *bi-assertives* dans l'esprit de celles proposées dans [Pipatsrisawat & Darwiche 2008] en partant de chacun des deux littéraux en contradiction lors d'un conflit et en effectuant des résolutions jusqu'au littéral assertif.

### 2.5.2 Simplification des bases des clauses apprises

Le nombre de clauses pouvant être générées par résolution est connu pour être exponentiel dans le pire des cas. Bien que la résolution est appliquée uniquement en cas de conflit, ce nombre reste également exponentiel. Garder toutes les clauses apprises présente l'inconvénient de ralentir la propagation unitaire et par conséquent la résolution. Afin de maintenir un équilibre entre l'apprentissage de clauses et l'efficacité de la propagation unitaire, il est commode
dans les solveurs SAT de supprimer régulièrement certaines clauses jugées non pertinentes pour
le reste de la recherche. Plusieurs travaux [Audemard & Simon 2009] ont essayé de mettre en
exergue des stratégies capable de juger de la pertinence des clauses apprises et par conséquent
de décider de celles à maintenir et celles à supprimer. Dans [Jabbour et al. 2014b], nous avons
exploré ce champ en partant de l'observation que les clauses de taille réduite ont plus de pro-
babilité d'être utilisées dans le processus de propagation ou dans la construction des preuves
d'insatisfiabilité. Nous avons proposé plusieurs stratégies privilégiant les clauses de taille réduite
et faisant un choix arbitraire sur le reste des clauses. Choisir de manière arbitraire les clauses à
garder consiste à opérer une forme de diversification de la recherche. Nous avons proposé éga-
lement d'autres variantes comme celle basée sur la taille relative de chaque clause, i.e., la taille
modulo la propagation unitaire. Certaines stratégies se sont montrées particulièrement efficaces
sur plusieurs classes de problèmes, principalement sur des problèmes issues de la cryptographie
[Soos et al. 2009, Massacci & Marraro 2000]. Ces stratégies ont été implantées dans *Minisat* don-
nant lieu à un nouveau solveur appelé *X-Minisat*<fnref n="1" />.

## 2.6 Résolution parallèle du problème SAT

Dans cette section, nous donnons un aperçu de nos travaux effectués dans le cadre de la
résolution parallèle du problème SAT.

### 2.6.1 Approche portfolio

L'avénement récent des nouvelles architectures multicœurs a permis de raviver l'intérêt pour
le parallélisme et l'emergence d'une génération de solveurs SAT parallèles [Heule et al. 2018,
Audemard et al. 2012, Chu et al. 2008] visant à pousser les limites des problèmes pouvant être
résolus en pratique. Certaines approches ont remis au goût du jour le paradigme *diviser pour
régner* usuellement utilisant les chemins de guidage dans les premières générations de solveurs
SAT [Chrabakh & Wolski 2003, Böhm & Speckenmeyer 1996, Jurkowiak et al. 2001]. Ce prin-
cipe consiste à diviser l'espace de recherche entre différents cœurs de calcul de façon disjointe
en attribuant à chacun un sous-espace à explorer (sous-formule). Toutefois, cette approche est
confrontée à certaines problèmes, principalement l'équilibrage de charge. De plus, le nombre
de variables des instances SAT actuelles est élevé rendant l'approche moins efficace lorsque le
nombre de cœurs de calcul est limité. Partant du constat que les solveurs SAT sont sensibles aux
valeurs de leur paramètres, i.e., un changement minimal dans la valeur d'un paramètre peut avoir
une grande influence sur le temps de calcul, nous avons proposé ManySAT [Hamadi et al. 2009],
le premier solveur parallèle dont l'architecture est basée sur un portfolio de solveurs de type
CDCL changés en leur principal composants. ManySAT permet de lancer plusieurs solveurs de
type CDCL (cœur de calcul) incarnant chacun une stratégie différente. Le but est de permettre une
exploration différente de l'espace de recherche. D'autres part, afin d'éviter de revisiter des sous
espaces de recherche redondants, les différents cœurs de calcul échangent régulièrement certaines
clauses entre eux. Intuitivement les clauses de taille réduite sont échangées permettant d'amélior-
rer considérablement la résolution. Empiriquement, dans la première version de ManySAT, nous

<footnote n="1">1. http://www.cril.univ-artois.fr/ sais/X-SAT/</footnote>
avons constaté qu’échanger des clauses de taille inférieure à 10 permet d’obtenir les meilleures performances.

Le solveur ManySAT s’est distingué en remportant la première compétition dédiée aux solveurs SAT parallèles organisée en 2009².

## 2.6.2 Échange de clauses

La stratégie de partage de clauses proposée dans [Hamadi et al. 2009] a certaines limitations. En effet, pour certains problèmes, la résolution passe par des phases où les clauses générées ont une taille plus élevée que la limite fixée. Pour certains autres, le nombre de clauses ayant une taille inférieure au seuil fixée peut s’avérer très élevé forçant les cœurs de calcul à passer plus de temps à échanger des clauses qu’à explorer l’espace de recherche. Dans [Hamadi et al. 2011], nous avons proposé une politique dynamique de partage de clauses qui utilise des limites de taille par paires pour contrôler l’échange entre chaque deux cœurs de calcul. L’évolution des limites par paires suit une loi AIMD (Additive-Increase-MultiplicativeDecrease), un algorithme de contrôle par rétroaction [Chiu & Jain 1989]. L’algorithme Additive Increase/Multiplicative Decrease (AIMD) est un algorithme de contrôle de débit utilisé pour éviter la congestion dans les réseaux de communication. Le problème résolu par AIMD est de deviner la bande passante de communication disponible entre deux nœuds communicants. L’algorithme effectue des sondes successives, augmentant le taux de communication w linéairement tant qu’aucune perte de paquets n’est observée, et la diminuer exponentiellement quand une perte est rencontrée. Plus précisément, l’évolution de w est définie par la formule AIMD(a, b) suivante :

$$w = \begin{cases} w - a \times w & \text{si une perte est détectée} \\ w + b & \text{sinon.} \end{cases}$$

Pour remédier au problème de la pertinence des clauses partagées, nous étendons notre politique pour intégrer la qualité des échanges. Chaque cœur de calcul évalue la qualité des clauses reçues, et le contrôle est capable d’augmenter/diminuer les limites par paires basées sur la qualité sous-jacente des clauses récemment reçues. La justification étant que les informations récemment reçues d’une source particulière est qualitativement liée à l’information qui pourrait être reçu de lui dans un avenir très proche.

Dans [Audemard et al. 2012], nous avons continué l’exploration de l’échange de clauses en parallèle. Une nouvelle alternative issue des travaux dans le cadre de la résolution séquentiel de SAT a été développée. Il s’agit d’adapter l’heuristique basée sur la stratégie psm définie dans [Audemard et al. 2011] au cadre parallèle basé sur un portfolio de solveurs. Plus précisément, les clauses sont échangées entre les cœurs de calcul si elles n’excèdent pas une taille fixe. Ces clauses ne sont pas réellement intégrées à la recherche que si elles sont potentiellement utiles à la recherche, i.e., très proche de l’interprétation en cours d’exploration. Dans le cas contraire elles sont gelées et vérifiées périodiquement.

Dans [Lazaar et al. 2012], nous nous sommes intéressés à l’échange de clauses à grande échelle d’une architecture parallèle. Nous avons montré que la topologie de communication complète (e.g., ManySAT2.0) arrive très souvent à son limite lorsque le nombre de cœurs est important. Pour pallier ce problème, nous avons introduit une nouvelle technique décentralisée qui

<footnote n="2">2. http://www.satcompetition.org/</footnote>
permet de contrôler l'échange et le partage de clauses entre les différents cœurs. Notre approche consiste à sélectionner pour chaque cœur de calcul, les potentiels cœurs pouvant communiqués avec lui, i.e, autorisés à partager des clauses apprises avec ce dernier de manière décentralisée et dynamique. Notons que la longueur maximale des clauses partagées est fixe préalablement. Pour ce faire, nous nous sommes basés sur une approche bandit multi-armée baptisée Bandit Ensemble for Parallel SAT Solving (BESS) afin de gérer de manière dynamique l'échange entre les différents cœurs de calcul.

### 2.6.3 Intensification et diversification

Dans les solveurs SAT modernes, les redémarrages constitue une forme de diversification de la recherche alors que la pondération des variables des conflits vise à intensifier la recherche en focalisant la recherche sur des sous-espaces conflictuels. Dans les approches parallèles de type portfolio, la diversification est facilement mise en œuvre par le biais des paramètres des solveurs. Par contre l'intensification de la recherche n'a pas été suffisamment explorée. Afin de trouver un compromis entre ces deux principes d'intensification et de diversification, nous avons proposé dans [Guo et al. 2010] une nouvelle approche parallèle basée sur le principe *maître/esclave*. Plus précisément, certains cœurs de calcul sont choisis pour être des maîtres et ont pour objectif de diversifier la recherche. Les cœurs de calcul restants, appelés esclaves, ont pour but d'intensifier la recherche de leurs maîtres. L'intensification consiste à forcer les esclaves à explorer différem- ment des sous-espaces proche de ceux en cours d'exploration par les maîtres. Formellement, dans [Guo et al. 2010], les maîtres partagent régulièrement avec les esclaves les affectations partielles à considérer. Ces dernières sont composées de littéraux des derniers conflits. Cette stratégie a montré son efficacité principalement sur les instances connues pour être insatisfiables.

Dans [Guo et al. 2014], nous avons considéré une autre alternative pour la diversification de la recherche. Dans ce travail, nous nous sommes intéressés à l'impact des stratégies de réduc- tion de la base des clauses apprises sur la parallélisation des approches SAT de type portfolio. Nous avons proposé de diversifier la recherche en forçant chacun des cœurs à réduire sa base de clauses apprises en choisissant une stratégie différente parmi celles proposées dans la littérature [Audemard & Simon 2009] tout en proposant de nouvelles.

### 2.6.4 Parallèle & déterminisme

L'approche parallèle permet de diminuer le temps nécessaire à la résolution de certains problèmes SAT et d'en résoudre d'autres jusqu'au là inaccessible par les solveurs séquentiels. Tou- tefois, cela s'accompagne par une problématique liée au déterminisme de ces solveurs. En effet, à cause de l'échange de clauses, lorsque l'instance est satisfiable le modèle trouvé peut être dif- férent d'une exécution à une autre. Même constat peut être fait pour la preuve par résolution pour la réfutation. Pour remédier à ce problème, nous avons proposé un solveur SAT parallèle déterministe [Hamadi et al. 2011]. Ses résultats sont entièrement reproductibles, c'est-à-dire, une exploration parallèle reproductible de l'espace de recherche, qui comprend le même modèle rap- porté ou preuve de l'insatisfiabilité. Nous avons proposé un solveur qui définit un environnement contrôlé basé sur un ordre total des interactions des solveurs à l'aide de barrières de synchronisa- tion. Pour maximiser l'efficacité, l'échange d'informations (clauses de conflit) et la vérification de
la terminaison sont effectués régulièrement. La fréquence de ces échanges influence grandement
sur la performance de notre solveur. Nous avons proposé dans ce cadre une stratégie dynamique
pour décider de la fréquence de synchronisation.

2.6.5 Approche distribuée

Dans [Audemard et al. 2014], nous avons proposé un autre cadre pour résoudre le problème
SAT en parallèle en se basant sur le principe de diviser pour régner dans un environnement dis-
tribué afin de pouvoir profiter des architectures distribuées offrant un large nombre de cœurs de
calcul. En se basant sur une architecture maître/esclave utilisant le principe de diviser pour régner,
nous avons conçu un solveur où le maître se charge d'attribuer les sous-espaces de recherche à
explorer lorsqu'un esclave a fini d'exécuter sa tâche et qui utilise l'équilibrage de charge pour
gérer l'inactivité des cœurs de calcul [Chrabakh & Wolski 2003, Chu et al. 2008]. Cependant, ce
cadre est exposé à certains cas pathologiques dans le contexte SAT, comme l'effet ping pong ou
encore la division inutile pouvant considérablement ralentir les performances de l'approche. Nous
avons proposé plusieurs améliorations visant à éviter ces cas problématiques en munissant les es-
claves de capacités à refuser de diviser l'espace de recherche sous certaines conditions. Ce travail
a donné lieu à un solveur appelé Dolius<fnref n="3" />.

2.7 Énumération de modèles

Comme ça été mentionné auparavant, avec l'expansion des domaines d'application de SAT, le problème d'énumération de tous ou une partie des modèles de formules sous forme CNF connait un vrai regain d'intérêt. Nous allons à présent détailler nos travaux portant sur l'énumération des modèles d'une formule propositionnelle.

2.7.1 Énumération de tous les modèles

Généralement, les approches d'énumération de modèles sont basés sur les solveurs SAT mo-
dernes. Ces implantations sont basées sur l'ajout de clauses, appelées *clauses bloquantes*, per-
mettant d'éviter la génération des modèles redondants [McMillan 2002, Chauhan *et al.* 2003,
Jin *et al.* 2005]. Ces clauses peuvent correspondre à la négation du modèle trouvé. D'autres ap-
proches ont essayé d'améliorer cette procédure [Jin *et al.* 2005]. Dans [Morgado & Marques-Silva 2005],
les auteurs proposent plusieurs optimisations obtenues par apprentissage et simplification des
clauses bloquantes. Le but est de trouver la plus petite interprétation partielle satisfaisant la for-
mule et couvrant le modèle trouvé par le solveur. Une interprétation partielle de taille *k* sur une
formule contenant *n* variables représente les $2^{n-k}$ modèles et ajouter la clause bloquante associée
permet d'éviter l'énumération d'un tel ensemble de modèles. Cependant, cette approche naïve
présente certaines limites. Tout d'abord, de point de vue complexité, le nombre de modèles à
énumérer peut être exponentiel. Cumuler à la fois des clauses apprises issues des conflits et celles
dites bloquantes peut altérer l'efficacité de la résolution. Le deuxième problème est lié à l'uti-
lisation de l'heuristique de branchement VSIDS connue pour être plus appropriée pour trouver
un seul modèle ou prouver qu'aucun modèle n'existe. De plus, il est bien connu que l'ordre

<footnote n="3">3. http://www.cril.univ-artois.fr/hoessen/dolius.html</footnote>
utilisé pour l'énumération de tous les modèles peut changer radicalement la complexité de calcul [Creignou et al. 2011]. Dans [Dechter & Itai 1992], les auteurs ont montré qu'énumérer tous les modèles d'une théorie donnée peut être effectuée dans le temps proportionnel au produit du nombre de modèles à l'effort nécessaire pour générer chaque modèle séparément. Par conséquent, un moyen efficace pour améliorer le processus d'énumération consisterait à chercher tous les modèles à proximité du modèle trouvé à une itération donnée.

Motivé par les observations ci-dessus, nous avons introduit dans [Jabbour et al. 2014a] une extension des solveurs CDCL pour énumérer tous les modèles d'une formule CNF. Notre approche procède de la manière suivante : la première étape consiste à chercher le premier modèle en utilisant un solveur CDCL classique. Lorsque ce dernier est trouvé, le solveur continue la recherche des autres modèles en inhibant les redémarrages.

### 2.7.2 Enumération des impliquants premiers

Les implicants premiers (PI) des fonctions booléennes est un sous-ensemble de générateurs de tous les modèles. Ils ont été utilisé dans le contexte de la minimisation des fonctions booléennes par Quine [Quine 1952, Quine 1959] et McCluskey [McCluskey 1956]. Cette première application de la forme canonique des impliquants premiers est importante car cela permet de réduire la taille et le coût du circuit numérique tout en améliorant la vitesse (par exemple, [Tison 1967]). En plus de l'analyse et de l'optimisation des circuits numériques, les impliquants premiers ont trouvé plusieurs autres domaines d'application, y compris l'analyse de l'arbre de défaillance [Coudert & Madre 1993, Dutuit & Rauzy 1997], la bio-informatique [Acuña et al. 2012], les bases de données [del Val 1994], le diagnostique [de Kleer et al. 1990], et la représentation des connaissances et du raisonnement [Cadoli & Donini 1997]. Il est également importante dans de nombreux domaines de l'intelligence artificielle tels que le raisonnement automatique et non monotone [Ginsberg 1989], la compilation de connaissances [Darwiche & Marquis 2002], les systèmes multi-agents [Slavkovik & Agotnes 2014]. Cependant, le problème de génération de tous les impliquants premiers d'une théorie propositionnelle est une tâche très complexe.

Dans [Jabbour et al. 2014f], nous avons proposé une approche originale qui réécrit une formule CNF $\Phi$ comme une nouvelle formule CNF $\Phi'$ telle que les impliquants premiers de $\Phi$ correspondent aux modèles de $\Phi'$. Notre encodage emprunte l'idée de renommage des littéraux utilisée dans les formulations en programmation linéaire (ILP) proposées dans [Pizzuti 1996, Manquinho et al. 1997, Manquinho et al. 1998]. Formellement, soit $\Phi$ une formule CNF. Nous associons à chaque littéral $a$ de $\text{Lit}(\Phi)$ une variable propositionnelle $x_a$. Nous définissons la formule CNF $\Phi^R$ comme la formule obtenue à partir de $\Phi$ en renommant chaque littéral $a \in \text{Lit}(\Phi)$ par sa variable propositionnelle correspondante $x_a$, et en ajoutant les clauses binaires suivantes :

$$ \bigwedge_{a \in \text{Var}(\Phi)} (\neg x_a \lor \neg x_{\neg a}) \qquad (2.1) $$

La contrainte $\mathcal{M}(\Phi^R)$ définie dans (2.2) permet d'établir une bijection entre les impliquants premiers de la formule $\Phi$ et les modèles de la formule résultante.

$$ \mathcal{M}(\Phi^R) = \bigwedge_{a \in \text{Lit}(\Phi)} (x_a \rightarrow \bigwedge_{c \in \Phi^R, x_a \in c} c \setminus \{x_a\}) \qquad (2.2) $$
L'énumération des impliquants premiers est alors réduite au problème de l'énumération de
tous les modèles d'une formule CNF. Une telle correspondance permet de bénéficier des per-
formances des solveurs SAT modernes. Cependant, mettre (2.2) sous forme CNF peut augmen-
ter considérablement le nombre de variables et de clauses additionnelles. Dans notre deuxième
contribution, nous avons étendu notre approche en proposant un encodage plus compacte en ex-
ploitant la structure des formules. Plus précisément, grâce aux fonctions booléennes généralement
présentes dans les problèmes réels, des réductions significatives peuvent être opérées.

2.7.3 Enumération des modèles Top-k

Souvent dans le monde réel, l'énumération de tous les modèles n'est pas requise et est rem-
placée par l'énumération de certains modèles dit préférés. La notion de préférence joue un rôle
primordial dans plusieurs disciplines telles que l'économie, la recherche opérationnelle, et la
théorie de la décision en général. Les préférences sont pertinentes pour la conception de sys-
tèmes intelligents qui prennent en charge les décisions. La modélisation et le raisonnement avec
les préférences jouent un rôle croissant en intelligence artificielle et ses domaines connexes tels
que le raisonnement non monotone, la planification, le diagnostique, la configuration, la pro-
grammation par contraintes (CP), etc. Par exemple, dans le raisonnement non monotonique,
l'introduction de la sémantique préférentielle par Shoham [Shoham 1988] donne un cadre uni-
ficateur où la logique non monotone est réduite à une logique standard avec une relation de
préférence (ordre) sur les modèles de cette logique. Plusieurs modèles de représentation et de
raisonnement à propos des préférences ont été proposés. Par exemple, les contraintes souples
[Meseguer et al. 2006] sont l'un des moyens les plus généraux pour traiter les préférences quan-
titatives, tandis que les CP-net (réseaux de préférences conditionnelles) [Boutilier et al. 2004]
sont plus pratique pour les préférences qualitatives. Il existe une littérature abondante sur les
préférences (voir [Walsh 2007, Brafman & Domshlak 2009, Domshlak et al. 2011] pour plus de
détails). Dans l'exploration de données, les préférences ont également été étudiées par plusieurs
auteurs [Bistarelli & Bonchi 2007, de Amo et al. 2012, Ugarte Rojas et al. 2014]. Par exemple,
dans [Bistarelli & Bonchi 2007], les auteurs ont présenté un nouveau paradigme de découverte de
modèle basé sur des contraintes souples, où les contraintes ne sont plus des fonctions booléennes
rigides. Plus récemment, Ugarte et al. [Ugarte Rojas et al. 2014] ont introduit une méthode gé-
nérique et efficace basée sur la programmation par contraintes pour l'extraction de skypatterns
(soft-) qui permettent d'exprimer la préférence de l'utilisateur en fonction des relations de domi-
nance. Partant de l'observation que les relations de dominance sont présentes dans de nombreux
problèmes, dans [Négrevergne et al. 2013], les auteurs proposent une algèbre qui combine les
contraintes et les relations de dominance qui peuvent être utilisées pour décrire un large éventail
de paramètres d'exploration de modèles.

Dans [Jabbour et al. 2013d, Jabbour et al. 2017d], nous nous sommes intéressés aux préfé-
rences qualitatives définies par une relation de préférence sur les modèles d'une formule propo-
sitionnelle qui n'ont pas reçu beaucoup d'attention [Rosa et al. 2010, Castell et al. 1996]. Nous
avons introduit un cadre générique pour traiter les préférences qualitatives des formules proposi-
tionnelle. Nos préférences qualitatives sont définies à l'aide d'une relation réflexive et transitive
≥ (pré-ordre) sur les modèles d'une formule propositionnelle. Cette relation de préférence sur
les modèles est d'abord utilisée pour introduire un nouveau problème, appelé Top-k SAT, défini
comme le problème de l'énumération des modèles Top-k d'une formule propositionnelle. Ici, un modèle Top-k est défini comme un modèle n'ayant pas plus que (k - 1) modèles préférés à lui par rapport à la relation de préférence considérée. Nous avons également montré que Top-k SAT généralise les deux problèmes bien connus à savoir le problème MaxSAT partiel et le problème de génération de modèles minimaux. Un algorithme général pour calculer les modèles Top-k est également proposé pour des relations de préférences particulières.

## 2.8 Contraintes de cardinalité & problème des pigeons

Parmi les contraintes les plus récurrentes lors de l'encodage de certains problèmes d'applications vers SAT, les contraintes de cardinalité sont sans doute les plus fréquentes. Plusieurs applications impliquent le comptage d'arguments exprimés sous forme de contraintes de cardinalité ou contraintes pseudo-booléennes. Ce type de contraintes est souvent dû à l'encodage de problèmes du monde réel, tels que l'assignation de fréquences radio, la programmation temporelle et les problèmes de configuration de produits pour n'en citer que quelques-uns. Ces contraintes sont exprimées sous la forme suivante :

$$ \sum_{i=1}^{n} x_i \# k \quad x_i \in \{0, 1\}, \quad k \in \mathbb{Z}, \quad \# \in \{\le, \ge, =\} \qquad (2.3) $$

La transformation de la contrainte (2.3) en CNF a fait l'objet de nombreux travaux visant à proposer des encodages efficaces en utilisant plusieurs modèles incluant les BDD, les réseaux de tri, etc. [Warners 1996, Sinz 2005, Silva & Lynce 2007, Asín et al. 2009, Eén & Sörensson 2006, Bailleux et al. 2009]. L'efficacité fait référence à la fois à la compacité de la représentation (taille de la formule CNF) et à la capacité d'atteindre le même niveau de propagation de contraintes (cohérence d'arc généralisée) sur la formule CNF. Souvent ces transformations se basent sur l'ajout de nouvelles variables et clauses pour réduire la taille de l'encodage. Nous avons proposé dans [Jabbour et al. 2013d, Jabbour et al. 2014g] une approche originale basée sur le principe des tiroirs (pigeon-hole problem). Ce dernier affirme qu'il n'y a pas de correspondance injective de k pigeons à n cases telle que $n < k$. Le problème des pigeons peut être transformé en un problème SAT obtenu par l'introduction de variables additionnelles $p_{ij}$ exprimant que le pigeon i est mis dans la case j. La formulation standard du principe des tiroirs est le résultat de la conjonction des contraintes (2.4) et (2.5) suivantes :

$$ \bigwedge_{i=1}^{k} \bigvee_{j=1}^{n} p_{ij} \qquad (2.4) $$

$$ \bigwedge_{l=1}^{k} \bigwedge_{1 \le i < j < n} (\neg p_{il} \lor \neg p_{jl}) \qquad (2.5) $$

Pour transformer la contrainte de cardinalité $\sum_{i=1}^{n} x_i \ge k$ en CNF, nous nous sommes basés sur l'encodage erronée de Hooker, dans une note non publiée [Warners 1996], pour donner la bonne formulation en utilisant le principe des tiroirs ci-dessous.
$$ \bigwedge_{i=1}^{n} \bigwedge_{j=1}^{k} (x_i \lor \neg p_{ji}) \qquad (2.6) $$

$$ \bigwedge_{i=1}^{k} (\bigvee_{j=1}^{n} p_{ij}) \qquad (2.7) $$

$$ \bigwedge_{l=1}^{k} \bigwedge_{1 \le i < j < n} (\neg p_{il} \lor \neg p_{jl}) \qquad (2.8) $$

La transformation est polynômiale et nécessite l'ajout de $n(k + 1)$ variables et $k + n(k + \frac{k(k-1)}{2})$ clauses. Par conséquent, la complexité globale est en $O(kn)$ variables et $O(nk^2)$ clauses. Toute fois, cet encodage ne permet pas de satisfaire la contrainte de la cohérence d'arc généralisée. Le problème des tiroirs est connu pour être difficile à résoudre. Pour pallier ce problème, dans [Jabbour et al. 2013d, Jabbour et al. 2014g] nous nous sommes basés sur les symétries très présentes dans cette formulation. Nous avons proposé de combiner les contraintes d'élimination de symétries (voir section 2.4) et les contraintes (2.6), (2.7), et (2.8). Formellement, au lieu d'ajouter conjonctivement les contraintes de suppression de symétries à l'encodage initial, nous avons montré qu'une application intelligente de la résolution entre ces deux ensembles permet d'obtenir le nouveau encodage constitué de 2.9), (2.10) et (2.11) qui satisfait la cohérence d'arc généralisée.

$$ \bigwedge_{1 \le i \le k} (\bigvee_{1 \le j \le n-k+1} p_{ij}) \qquad (2.9) $$

$$ \bigwedge_{1 \le i \le k} \bigwedge_{1 \le j \le n-k+1} (x_{i+j-1} \lor \neg p_{ij}) \qquad (2.10) $$

$$ \bigwedge_{1 \le i < k} \bigwedge_{1 \le j < n-k+1} (\neg p_{(i+1)j} \lor \bigvee_{1 \le l \le j} p_{il}) \qquad (2.11) $$

Cet encodage présente l'inconvénient d'être en $O(k(n-k)^2)$ en le nombre d'occurrences des littéraux. Dans [Hattad et al. 2017], nous avons montré qu'il est possible de compacter cet encodage afin de maintenir la même complexité en nombres de clauses et de variables mais en réduisant la taille en le nombre de littéraux de $O(k(n-k)^2)$ à $O(k(n-k))$. En effet, comme illustré dans la figure 2.1 représentant un sous-ensemble de clauses issues de (2.11), la sous clause $(p_{11} \lor p_{12} \lor p_{13} \lor p_{23} \lor \dots \lor p_{2\frac{n-k}{2}})$ est fréquente dans $\frac{k}{2}$ clauses. Par conséquent, le principe d'extension de Tseitin par ajout de variables peut être utilisé permettant de substituer $\frac{n-k}{2} \times \frac{k}{2}$ littéraux par seulement $\frac{kn}{2} + \frac{k}{2}$ autres.

Par ailleurs, nous avons montré que notre approche peut facilement être rendue incrémentale i.e., le changement de la borne de la contrainte de cardinalité ne nécessite pas un encodage depuis le début. Cette approche a été intégrée au solveur QMaxSAT [Koshimura et al. 2012] pour résoudre des problèmes d'optimisation de type MaxSAT ou MaxSAT partiel.
<figure><img src="image_2.png" /><figcaption>FIGURE 2.1 – Représentation compacte de contraintes</figcaption></figure>

## 2.9 Contrainte de cardinalité conditionnelle

Dans [Jabbour et al. 2017a], nous nous sommes intéressés à une variante de la contrainte de cardinalité appelée *contraintes de cardinalité conditionnelle* exprimée sous la forme $y \to \sum_{i=1}^{n} x_i \le k$. Une manière naturelle de coder cette contrainte en CNF consiste à encoder $\sum_{i=1}^{n} x_i \le k$ sous forme clausale et d'ajouter $\neg y$ à chacune des clauses. Toutefois, cette manière de procéder ne permet pas de préserver l'arc cohérence généralisée. En effet, considérons le cas où $k = 1$. En utilisant la transformation de $\sum_{i=1}^{n} x_i \le 1$ décrite dans [Sinz 2005] (équivalence à celle obtenue avec le principe des tiroirs), $y \to \sum_{i=1}^{n} x_i \le k$ est exprimée comme suit :

$$ (\neg y \lor \neg x_1 \lor p_1) \land (\neg y \lor \neg x_n \lor \neg p_{n-1})\land \\ \bigwedge_{1<i<n} (\neg y \lor \neg x_i \lor p_i) \land (\neg y \lor \neg p_{i-1} \lor p_i) \land (\neg y \lor \neg x_i \lor \neg p_{i-1}) \quad (2.12) $$

En utilisant (2.12), on peut déduire que l'affectation de plusieurs littéraux $x_i$ à vrai ne permet pas de déduire $\neg y$ par propagation unitaire. En effet, la formule restante est binaire et sans clause unitaire. Afin de pallier ce problème, nous avons montré que si $\Phi$ est une formule de horn insatisfiable sous une interprétation partielle de littéraux positifs, alors il est possible de déduire par propagation sur ses clauses mixtes d'autres littéraux positifs rendant l'une de ses clauses négatives totalement fausse. Ce résultat permet de décider des clauses à augmenter par $\neg y$ afin de préserver l'arc cohérence généralisée à savoir les clauses totalement négatives. Notons que la majorité des encodages de la contrainte de cardinalité $\sum_{i=1}^{n} x_i \le k$ sont des formules de horn. Dans le cas particulier de la contrainte $y \to \sum_{i=1}^{n} x_i \le 1$, cela donne lieu à la formulation suivante :

$$ (\neg x_1 \lor p_1) \land (\neg y \lor \neg x_n \lor \neg p_{n-1})\land \\ \bigwedge_{1<i<n} (\neg x_i \lor p_i) \land (\neg p_{i-1} \lor p_i) \land (\neg y \lor \neg x_i \lor \neg p_{i-1}) \quad (2.13) $$

## 2.10 Représentation compacte

Dans cette section, nous présentons deux approches visant à compacter la représentation des formules CNF et contraintes tables afin d'améliorer l'efficacité de la résolution.
### 2.10.1 Forme normale conjonctive

Réduire la taille des représentations CNF est une question cruciale dans l'efficacité de la ré-solution à l'heure des données volumineuses (Big Data). Les travaux visant à encoder de manière concise certaines contraintes spécifiques comme les contraintes de cardinalité, etc. ont contribué à réduire considérablement la taille des formules issues de transformations vers CNF et constituent une étape dans ce but. Les méthodes de simplification par application de la règle de résolution en constituent une autre [Eén & Biere 2005].

Dans [Jabbour et al. 2013f], nous avons montré comment la fouille de données peut être exploitée de manière originale et élégante pour compacter la représentation CNF des formules. Nous avons montré que les techniques d'extraction d'itemsets sont très appropriées pour découvrir des sous-clauses fréquentes dans les formules CNF. Plus précisément, une formule CNF $\Phi$ est codée sous la forme d'une table de transactions $D$ contenant chacune les littéraux d'une clause. Les itemsets fréquents (fermés) de $D$ correspondants dans ce cas aux sous-clauses qui se répètent dans $\Phi$. Ces motifs sont ensuite utilisés pour réécrire la formule CNF de manière plus compacte grâce au principe d'extension de Tseitin [Tseitin 1968] par ajout de variables additionnelles comme illustré dans l'exemple 1.

**Exemple 1.** La sous-clause $x_4 \lor x_5 \lor x_6$ est fréquente dans la formule $\Phi$ suivante. L'application du principe d'extension de Tseitin permet d'obtenir la nouvelle CNF $\Phi'$ par ajout d'une variable supplémentaire $y$.

$$ \Phi = \begin{array}{l} \neg x_0 \lor x_2 \\ \neg x_1 \lor x_4 \\ \neg x_3 \lor x_4 \\ \neg x_5 \lor x_6 \\ \neg x_0 \lor x_1 \lor \mathbf{x}_4 \lor \mathbf{x}_5 \lor \mathbf{x}_6 \\ x_3 \lor \mathbf{x}_4 \lor \mathbf{x}_5 \lor \mathbf{x}_6 \\ \neg x_1 \lor x_2 \lor \mathbf{x}_4 \lor \mathbf{x}_5 \lor \mathbf{x}_6 \\ \neg x_2 \lor x_3 \lor \mathbf{x}_4 \lor \mathbf{x}_5 \lor \mathbf{x}_6 \end{array} \quad \Phi' = \begin{array}{l} \neg x_0 \lor x_2 \\ \neg x_1 \lor x_4 \\ \neg x_3 \lor x_4 \\ \neg x_5 \lor x_6 \\ \neg x_0 \lor x_1 \lor \mathbf{y} \\ x_3 \lor \mathbf{y} \\ \neg x_1 \lor x_2 \lor \mathbf{y} \\ \neg x_2 \lor x_3 \lor \mathbf{y} \\ \neg \mathbf{y} \lor x_4 \lor x_5 \lor x_6 \end{array} $$

La recherche de l'ordre de remplacement optimale peut être encodée en problème d'optimisation. Nous avons montré également que l'ensemble des clauses binaires, très présentes dans les transformations de problèmes d'application vers SAT, peut considérablement être réduit. Cette réduction est possible en considérant une représentation intermédiaire, sous forme d'implications, $((x_1 \lor x_2) \land (x_1 \lor x_3) \land (x_1 \lor x_4) \land (x_1 \lor x_5))$ est équivalente à $x_1 \rightarrow x_2 \land x_3 \land x_4 \land x_5)$. Cette formulation permet de représenter les conséquences des implications sous forme de table de transactions et par conséquent de calquer le processus de la fouille des itemsets préalablement décrit pour compacter l'ensemble des clauses binaires. Nous avons également prouvé que notre approche peut réaliser des réductions similaires à celle de [Rintanen 2006]. C'est le cas pour un ensemble de clauses binaires formant un graphe biparti ou une clique. Cela offre une réelle alternative pour trouver des encodages réduits de certaines contraintes standards qui sont récurrentes lors des transformations vers SAT.
## 2.10.2 Contraintes tables

La programmation par contraintes (CP) est un paradigme puissant pour résoudre des problèmes combinatoires, basée sur un large éventail de méthodes de l'intelligence artificielle. Bien que ce paradigme appartient à la même classe de complexité que SAT (NP-Complet) et a motivé beaucoup de fertilisations allant de la traduction de problèmes de satisfaction de contraintes en SAT à l'hybridation d'approches, CP se distingue par un langage plus expressif. Un problème de satisfaction de contraintes (CSP) est un triple $\langle X, Dom, C \rangle$ où :

- $X = \langle X_1, X_2, \dots, X_n \rangle$ est un n-tuple de variables,

- $Dom = \langle Dom(X_1), Dom(X_2), \dots, Dom(X_n) \rangle$ est un n-tuple de domaines tel que $X_i \in Dom(X_i)$,

- $C = \{C_1, C_2, \dots, C_k\}$ est un ensemble de contraintes où chaque contrainte $C_i$ porte sur un sous-ensemble de X.

Les contraintes entre variables peuvent être exprimées soit en intension (contraintes globales e.g., contrainte de cardinalité, alldiff, etc.) ou en extension (contraintes tables).

Les contraintes tables sont considérées depuis longtemps comme particulièrement importantes dans les problèmes de satisfaction de contraintes. L'une des formulations de CSP les plus utilisées consiste à exprimer chaque contrainte en extension ou en tant que relation entre les variables avec domaines finis associés. Cependant, la taille de ce type de contraintes en extension pourrait être exponentiel dans le pire des cas. La complexité de l'espace de ce type de contraintes est un obstacle. Des tentatives de compression ont été proposées [Katsirelos & Walsh 2007] où une représentation alternative de l'ensemble des tuples d'une relation est représentée par un ensemble de tuples compressés. Cependant, les tuples compressés peuvent être plus grands que l'arité de la contrainte d'origine.

Dans [Jabbour et al. 2015a], nous avons proposé une approche de compression de contraintes tables qui combine les deux techniques d'extraction d'éléments fréquents et le principe d'extension de Tseitin pour dériver une nouvelle représentation compacte des contraintes tables. Nous avons montré que notre approche de compression de formules propositionnelles peut être parfaitement étendue et appliquée au cas des CSP en considérant le graphe de contraintes comme base de données, où les transactions correspondent aux contraintes et les items aux variables du CSP. Un itemset fréquent fermé correspond à un sous-ensemble de variables partagées le plus souvent par les différentes contraintes du CSP. Puis, en utilisant l'extension (variables auxiliaires), nous avons montré comment de telles contraintes peuvent être réécrites tout en préservant l'équivalence pour satisfiabilité. Dans [Jabbour et al. 2015a], nous avons également considéré chaque contrainte table individuellement donnant lieu à une nouvelle base de transactions formée d'une séquence de tuples, c'est-à-dire un ensemble de tuples indexés. Plus précisément, chaque valeur d'un tuple est indexé avec sa position dans la contrainte. En énumérant les itemsets fréquents fermés de cette base de transactions, nous sommes en mesure d'identifier le plus grand rectangle de la contrainte de la table. De même, avec le principe d'extension, nous avons montré comment une telle contrainte peut être représentée de manière plus succinte.
<figure><img src="image_3.png" /></figure>
# Fouille de données & Clustering

## 3.1 Introduction

L'analyse de données incluant l'extraction des connaissances à partir de données et la classification est à l'heure actuelle de domaine de recherche majeure accentué par la libéralisation de l'accès aux données qui rend ce domaine au centre de beaucoup de travaux de recherche.

L'extraction des motifs ensemblistes est l'une des tâches fondamentales de la fouille de données. Elle vise à découvrir des nouvelles relations intéressantes cachées dans de grandes bases de données. Depuis la première application, largement connue sous la dénomination de panier de la ménagère [Agrawal & Srikant 1994], plusieurs nouveaux domaines d'application ont été identifiés comme la bio-informatique, le diagnostic médical, la détection d'intrusion, la fouille du web et l'analyse des données scientifiques. Ce large spectre d'applications a permis à la fouille d'itemsets ou règles d'association d'être appliquée à une variété de bases de données, y compris les données séquentielles, spatiales, et les données des graphes.

D'autres part, l'extraction des motifs séquentiels est largement utilisée en bio-informatique comme un moyen d'extraire des connaissances significatives à partir d'un grand volume de données telles que la découverte de motifs dans les protéines, la prédiction de gènes et l'alignement de séquences. Ce problème est au cœur de nombreux autres domaines d'applications tels que les bases de données et l'exploration de texte. Elle constitue une tâche centrale dans la biologie calculatoire, l'analyse de séquence temporelle et l'exploration de texte.

Comme souligné dans [Raedt et al. 2008, Raedt et al. 2011], les contraintes font souvent partie de la spécification de plusieurs problèmes de fouille de données. Cette observation a conduit à un nouveau domaine de recherche actif et multidisciplinaire permettant une fertilisation croisée entre la fouille de données et l'intelligence artificielle [Raedt et al. 2008, Davidson et al. 2010, Dao et al. 2013, Kemmar et al. 2014, Gebser et al. 2016]. Plusieurs modèles de représentation et de résolution en intelligence artificielle ont été utilisés pour modéliser et résoudre plusieurs problèmes de fouille de données.

Dans la suite, nous présentons nos différentes approches pour la fouille des motifs ensemblistes et séquentiels.

## 3.2 Définitions et cadre formel

Soit $\Omega$ un ensemble fini non vide de symboles appelés *items*. À partir de maintenant, nous supposons que cet ensemble est fixe. Nous utilisons les lettres *a*, *b*, *c*, etc. pour désigner les éléments de $\Omega$.
— Un *itemset* *I* sur Ω est défini comme un sous-ensemble de Ω, c'est-à-dire, *I* ⊆ Ω. Nous
utilisons 2^Ω pour désigner l'ensemble des itemsets sur Ω et les lettres majuscules *I*, *J*, *K*,
etc. pour représenter les éléments de 2^Ω.

— Une *transaction* est une paire ordonnée (*i*, *I*) tel que *i* est une entier naturel, appelé *identifiant de transaction*, et *I* un itemset, i.e., (*i*, *I*) ∈ N × 2^Ω.

— Une *base transactionnelle D* (ou table de transactions) est définie comme un ensemble fini de transactions non vides ($D \subseteq N \times 2^\Omega$) où chaque identifiant de transaction fait référence à un ensemble d'éléments unique.

La figure 3.2 montre deux représentations de base d'une table de transactions. Dans celle de droite, les valeurs sont des booléens indiquant que l'item est présent (1) ou pas (0).

<table>
  <thead>
    <tr>
      <th>id</th>
      <th>transactions</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>1</td>
      <td>C D E F G</td>
    </tr>
    <tr>
      <td>2</td>
      <td>C D E F G</td>
    </tr>
    <tr>
      <td>3</td>
      <td>A B C D</td>
    </tr>
    <tr>
      <td>4</td>
      <td>A B C D F</td>
    </tr>
    <tr>
      <td>5</td>
      <td>A B C D</td>
    </tr>
    <tr>
      <td>6</td>
      <td>C E</td>
    </tr>
  </tbody>
</table>

<table><caption>TABLE 3.1 – Deux représentations d’une table des transactions</caption>
  <thead>
    <tr>
      <th>id</th>
      <th colspan="7">transactions</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>1</td>
      <td>0</td>
      <td>0</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
    </tr>
    <tr>
      <td>2</td>
      <td>0</td>
      <td>0</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
    </tr>
    <tr>
      <td>3</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>0</td>
      <td>0</td>
      <td>0</td>
    </tr>
    <tr>
      <td>4</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>0</td>
      <td>1</td>
      <td>0</td>
    </tr>
    <tr>
      <td>5</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>1</td>
      <td>0</td>
      <td>0</td>
      <td>0</td>
    </tr>
    <tr>
      <td>6</td>
      <td>0</td>
      <td>0</td>
      <td>1</td>
      <td>0</td>
      <td>1</td>
      <td>0</td>
      <td>0</td>
    </tr>
  </tbody>
</table>

Étant donnés une table de transactions *D* et un itemset *I*, la *couverture* de *I* dans *D*, notée *C(I, D)*, est définie par *C(I, D) = {i ∈ N | (i, J) ∈ D et I ⊆ J}*. Le *support* de *I* dans *D*, noté *Supp(I, D)*, correspond à la cardinalité de *C(I, D)*, i.e., *Supp(I, D) = |C(I, D)|*.

Les itemsets fréquents peuvent être obtenus à partir de ceux dits fermés en énumérant tous les sous-ensembles.

**Définition 2 (Itemset Fermé).** Soit *D* une table de transactions. Un itemset *I* ⊆ Ω tel que *Supp(I, D) ≥ 1* est fermé si pour tout itemset *J* tel que *I ⊂ J*, *Supp(J, D) < Supp(I, D)*.

La propriété la plus importante pour élaguer la recherche l'espace dans les algorithmes traditionnels est l'anti-monotonicité i.e., si *I* n'est pas un itemset fréquent alors tout itemset *I* ⊂ *J* n'est pas fréquent également.

Le problème de fouille des itemsets fréquents consiste à énumérer, étant donné un seuil de support minimum *minupp*, l'ensemble {*I* ∈ Ω | *supp(I)* ≥ *minsupp*}. La figure 3.3.5 représente l'espace des 2^Ω itemsets possible connu pour former un treillis.

**Définition 3 (Règle d'Association).** Une Règle d'Association est un motif de la forme $X \rightarrow Y$ tel que $X$ (appelé antécédent) et $Y$ (appelé conséquence) sont deux itemsets disjoints.

En fouille de règles d'association, le prédicat d'intérêt est défini en utilisant les notions de sup-
port et de confiance. Le *support d'une règle d'association* $X \to Y$ dans une table de transactions
*D*, est définit comme suit :

$$
\mathrm{Supp}(X \to Y, D) = \frac{\mathrm{Supp}(X \cup Y, D)}{|D|}
$$
<figure><img src="image_4.png" /><figcaption>FIGURE 3.1 – Visualisation de l'espace des itemsets possibles</figcaption></figure>

Clairement, le support d'une règle d'association détermine la fréquence d'occurrence de la règle.

On peut alors définir la *confidence* de $X \to Y$ dans $D$ comme suit :

$$ Conf(X \to Y, D) = \frac{Supp(X \cup Y, D)}{Supp(X, D)} $$

Intuitivement, la *confidence* fournit une estimation de la probabilité conditionnelle de $Y$ étant donné $X$. Lorsqu'il n'y a pas d'ambiguïté, nous omettons de mentionner la table de transactions $D$, et nous notons simplement $Supp(X \to Y)$ et $Conf(X \to Y)$.

Une règle d'association *valide* est une règle d'association avec un support et une *confiance* supérieure ou égale au seuil de support minimum (*minsupp*) et au seuil de *confiance* minimum (*minconf*), respectivement.

Le problème de fouille des règles d'associton consiste à énumérer, étant donné un seuil de support minimum *minupp* et un seuil de *confidence* *minconf*, l'ensemble $\{X \to Y \mid X, Y \in \Omega, supp(X \to Y) \geq minsupp, conf(X \to Y) \geq minconf\}$.

**Définition 4** (Règle d'association fermée). Une règle $X \to Y$ est dite *fermée* ssi $X \to Y$ est une règle d'association *valide* et $X \cup Y$ est un *itemset* fermé.

## 3.3 Fouille des itemsets

Dans cette section, nous présentons nos différents travaux réalisés dans le cadre de la résolution du problème de l'énumération des itemsets fréquents. Nous décrivons notre approche déclarative basée sur une formulation de ce problème en logique propositionnelle. Nous détaillons les différentes améliorations proposées ainsi que des extensions pour énumérer des motifs particuliers.
### 3.3.1 Approche symbolique

Dans [Jabbour et al. 2013d], nous avons proposé d'exprimer le problème de la fouille des itemsets en un problème d'énumération de modèles d'une formule propositionnelle. Cet encodage permet d'avoir une bijection entre les itemsets de la table de transactions et les modèles de la formule propositionnelle correspondante. Formellement, nous introduisons deux types de variables booléennes, celles qui représentent les items et celles qui représentent les transactions. Pour chaque item a (resp. transaction $t_i$) une variable propositionnelle, notée $p_a$ (resp. $q_i$), est associée. Les itemsets recherchés correspondent aux modèles de la formule constituée des contraintes (3.1), (3.2) et (3.3).

La contrainte (3.1), décrite également dans [Henriques et al. 2012]), permet de capturer la table de transactions. Plus précisément, un itemset apparaît dans une transaction d'identifiant $i$ ($q_i = \text{vrai}$) si cet itemset est formé d'un sous-ensemble des items de la transaction $i$. Ce qui peut être exprimé via une simple fonction booléenne (3.1). Pour exiger que l'itemset recherché apparaît dans au moins $\text{minsupp}$ transactions, nous utilisons la fameuse contrainte de cardinalité (3.2). Nous avons mentionné que cette contrainte est récurrente dans beaucoup de transformation de problèmes d'applications vers CP ou SAT. D'ailleurs c'est autour de la réflexion sur cette contrainte que l'encodage basé sur le principe des tiroirs a été proposé (section 2.8).

$$ \bigwedge_{i=1}^{m} (\neg q_i \leftrightarrow \bigvee_{a \in \Omega \setminus T_i} p_a) \qquad (3.1) $$

$$ \sum_{i=1}^{m} q_i \geq \text{minsupp} \qquad (3.2) $$

$$ \bigwedge_{a \in \Omega} (\neg p_a \rightarrow \bigvee_{i \in [1..n] \mid a \notin T_i} q_i) \qquad (3.3) $$

De plus, afin d'exprimer qu'un itemset est fermé, nous considérons la contrainte (3.3). En effet, pour un item a, si l'itemset recherché apparaît uniquement dans un sous-ensemble de transactions contenant a, alors cet itemset doit contenir a. Notons que la contrainte de fermeture exige l'ajout de $|\Omega|$ clauses, une clause pour chaque item.

L'encodage par formulation vers SAT présente un avantage majeur. En effet, la recherche de certains itemsets particuliers peut se traduire aisément par ajout de contraintes booléennes à la formulation de base contrairement aux approches spécialisés nécessitant un changement dans le programme lui même. En effet, l'énumération des itemsets de supports inférieurs à up nécessite l'ajout de la contrainte $\sum_{i=1}^{m} q_i \leq up$ ou encore pour restreindre l'énumération aux itemsets de tailles supérieurs à lb est obtenu en ajoutant $\sum_{a \in \Omega} p_a \geq lb$. Ce pouvoir d'expressivité permet de disposer d'une approche déclarative capable d'enrichir la formulation de base par de nouvelles contraintes utilisateurs dont l'intégration est assez simple.

La contrepartie de la déclarativité de notre approche réside dans la taille des formules obte- nues. En effet, le nombre de clauses de la contrainte (3.1) est égale à $\sum_{i=1}^{m} (|\Omega| - |T_i| + 1)$. Or, très souvent, $|T_i| \ll |\Omega \setminus T_i|$ ce qui rend le nombre de clauses très proche de $|\Omega| \times |D|$. De plus la taille des clauses issues de la contrainte (3.3) est large. Tout cela constitue un vrai obstacle lorsque
l'on considère des données volumineuses. Pour remédier à ce problème, nous nous sommes inté-
ressés à trouver des solutions prometteuses permettant de passer à l'échelle en s'appuyant sur la
décomposition ou la parallélisme comme nous l'exposons dans la suite de ce manuscrit.

**3.3.2 Solveur adaptatif**

La traduction d'un problème dans un nouveau formalisme ne s'accompagne pas nécessairement par l'efficacité escomptée. En effet, certaines propriétés structurelles des problèmes initiaux ne sont pas facilement expressible dans la formulation. Dès lors, il est nécessaire de voir dans quelle mesure ces informations structurelles peuvent être prises en compte dans la conception d'un solveur dédié. Pour le problème de la fouille d'itemsets fréquents, plusieurs questions sont soulevées. L'heuristique VSIDIS est elle la plus appropriée pour ces problèmes ? l'apprentissage de clauses est il encore nécessaire ? Quelle polarité pour les variables ? Pour répondre à ces questions, nous avons mené une étude empirique [Dlala et al. 2016b] pour déterminer le paramétrage le plus approprié pour ce type de problèmes. Tout d'abord, le nombre de modèles est souvent assez élevé (des millions voir des dizaines de millions de modèles) pour les problèmes d'énumération. Par conséquent, nous avons constaté qu'un solveur CDCL utilisant simultanément l'apprentissage de clauses et les clauses bloquantes ralentit considérablement la recherche. Par contre une approche simple de type DPLL s'est montrée plus efficace. Concernant l'heuristique de choix de variables, nous avons comparé les performances de VSDIS [Zhang et al. 2001] à *MOMS* [Jeroslow & Wang 1990] qui procède en choisissant la variable la plus fréquente dans la CNF ce qui est équivalent à choisir l'item le moins fréquent dans la table de transactions. *MOMS* s'est distinguée en dominant VSIDS sur les problèmes considérés. Finalement, pour la polarité des variables, la conclusion est qu'affecter les variables à *vrai* permet d'obtenir les meilleurs performances. Toutefois dans le cas particulier de l'énumération des itemsets top-k, l'affectation à *faux* est, par contre, plus efficace.

Un autre problème lié à l'approche déclarative est celui de la contrainte (3.2). Bien que des
algorithmes de transformation de contraintes de cardinalité polynomiaux existent, la traduction
en CNF de cette contrainte n'est pas recommandée. Nous avons pu constater que gérer cette
contrainte par un simple propagateur permet de garantir des performances plus élevées au détri-
ment probablement d'une légère perte en élagage de l'espace de recherche.

**3.3.3 Motifs maximaux**

Parmi les approches utilisées pour réduire la taille de la sortie pour l'extraction des itemsets
fréquents, celles qui consistent à énumérer les itemsets fréquents fermés ont été largement étu-
diées permettant de réduire considérablement la taille de la sortie et par conséquent une meilleure
exploration des données en pratique. Néanmoins, dans de nombreuses applications, notamment
pour les données denses, la taille de l'ensemble des itemsets fermés [Zaki & Hsiao 2002] reste
très élevé [Gouda & Zaki 2005]. Pour réduire encore plus la taille de la sortie, il est commode
de considérer un sous-ensemble d'itemsets fermés dits *maximaux* qui sont une forme de conden-
sation des itemsets fréquents bien qu'il ne permettent pas de retrouver les supports de chacun
des itemsets. Un itemset fréquent est maximal s'il n'a pas de sur-ensemble qui est fréquent
[Jr. 1998, Lin & Kedem 1998, Burdick et al. 2001, Zou et al. 2002, Gouda & Zaki 2005].
Les approches déclaratives peuvent s'adapter parfaitement à ce sous-problème. En effet, dans l'approche SAT, pour énumérer les itemsets maximaux, il suffit d'ajouter la contrainte (3.4) qui permet de forcer l'itemset à être maximale.

$$ \bigwedge_{a \in \Omega} (\neg p_a \rightarrow \sum_{i \mid a \in T_i} q_i < \text{minsupp}) \qquad (3.4) $$

Toutefois, cette contrainte concentre les problèmes récurrents liée à la transformation de problèmes issues d'applications vers SAT. En effet, elle est composée de plusieurs contraintes de cardinalité conditionnelle dont la transformation en CNF peut devenir rapidement fastidieuse. Dans [Dlala et al. 2018], nous avons présenté un nouvel algorithme SATMAX qui fait une utilisation originale des solveurs SAT pour énumérer efficacement tous les motifs maximaux d'une table transactions. Plus précisément, SATMAX utilise une recherche arborescente basée sur un solveur de type DPLL affectant les items en priorité à vrai afin de maximiser le taille de l'itemset recherché. Pour éviter d'énumérer les itemsets non-maximaux, une clause bloquante est ajoutée après chaque modèle trouvé, constituée des items affectés à faux, forçant les prochains itemsets à ne pas être sous-ensembles de ceux déjà trouvés. Des techniques de simplifications ont été également intégrées pour rendre la résolution plus rapide. Par ailleurs, nous avons utilisé la décomposition comme celle décrite dans la section 3.3.4 pour passer à l'échelle. Les premiers résultats obtenus sont très satisfaisants. En effet, pour certaines données et certaines valeurs du seuil du support minimum, notre approche obtient de meilleurs performances que Eclat [Borgelt 2012], un des meilleurs algorithmes spécialisés pour énumérer les itemsets fréquents maximaux.

### 3.3.4 Décomposition & approche parallèle

Si les approches déclaratives comme celles que nous avons proposé [Jabbour et al. 2013e, Boudane et al. 2016] permettent d'intégrer aisément des contraintes utilisateurs au problème initiale, la taille des problèmes transformés est toutefois un vrai obstacle quand à la scalabilité de ces approches. À titre d'exemple, pour la table retail<fnref n="1" /> contenant 88128 transactions et 14245 items, le nombre de clauses de la contrainte (3.1) dépasse les 120 millions de clauses. S'il est prouvé que les solveurs CDCL peuvent résoudre des problèmes de grande taille, énumérer les modèles d'une formule de plusieurs dizaine de millions de clauses reste toutefois un palier difficile à franchir. Afin de permettre à notre approche déclarative de passer à l'échelle, nous avons proposé dans [Jabbour et al. 2015b] d'utiliser la décomposition comme mécanisme de division du problème de la fouille des itemsets fréquents. Notre approche consiste à ramener le problème de l'énumération des itemsets d'une table de transactions en l'énumération disjointes de plusieurs sous-table de petite taille en utilisant le paradigme *diviser pour régner*. L'idée principale est de décomposer la base de transactions en utilisant des chemins de guidage (voir figure 3.2) basées sur les items. Pour illustrer notre approche, considérons un item $a \in \Omega$. L'ensemble des itemsets fréquents peut être divisé en deux catégories : ceux contenant $a$ (les modèles de $\Phi_D \wedge p_a$) et ceux où $a$ n'appairait pas (les modèles de $\Phi_D \wedge \neg p_a$). Ceux qui contiennent $a$ sont alors ceux de la table constituée des transactions contenant $a$ alors qu'énumérer ceux qui ne contiennent pas $a$ consiste à supprimer $a$ de la table initiale. De plus, comme les sous-formules obtenues sont indépendantes,

<footnote n="1">1. http://fimi.ua.ac.be/data/</footnote>
<figure><img src="image_5.png" /><figcaption>FIGURE 3.2 – Arbre des chemins de guidage</figcaption></figure>

celles-ci peuvent être résolues en parallèle. Dans [Dlala et al. 2015, Dlala et al. 2010], nous avons conçu un solveur *paraSATMiner*<fnref n="2" /> qui permet de lancer l'énumération des itemsets fréquents fermés en séquentiel ou en parallèle en utilisant la décomposition. Nous avons défini un nouveau problème permettant de trouver l'ordre de décomposition le plus efficace. Plus intéressant encore, cette nouvelle approche s'est montrée particulièrement plus efficace que les approches CP récentes [Lazaar et al. 2016, Schaus et al. 2017], proposant l'énumération des itemsets fréquents fermés en utilisant des contraintes globales, et permet de résoudre des problèmes de grande taille jusqu'au là inaccessibles.

### 3.3.5 Symétries et motifs ensemblistes

Les symétries sont principalement étudiées en fouille de graphes (e.g. [Huan et al. 2003, Desrosiers et al. 2007, Vanetik 2010]). Nous avons poursuivi nos travaux en fouille de données afin de trouver des fertilisations croisées entre la fouille de données et l'intelligence artificielle mais cette fois ci en exportant les techniques proposées pour l'élimination des symétries dans SAT vers la fouille des itemsets fréquents. La symétrie dans une table de transactions est définie comme une permutation entre les items de la table la laissant invariante. D'ailleurs, comme le problème des itemsets fréquents peut être exprimé par des contraintes, les symétries de la table de transactions ne sont autre que les symétries de la formule CNF associée.

Pour découvrir les symétries d'une table de transactions, nous avons proposé de la transformer en un graphe. Les sommets représentent les items et les transactions et des arêtes lient tout sommet représentant un item aux transactions auxquelles il appartient. Les sommets des items sont différenciés de ceux des transactions dans le but d'éviter de générer des symétries entre un item et une transaction. La construction d'un tel graphe permet de profiter des nombreux algorithmes existants pour la découverte de symétries [McKay 1990, Ramani et al. 2006]. Par exemple, la permutation $\sigma = (b, m)(p, t)$ est une symétrie de la table $D_1$.

Afin d'exploiter les symétries en fouille de données, nous avons proposé deux approches différentes. La première [Jabbour et al. 2012] consiste à exploiter les symétries comme moyen de simplification de la table de transactions. En effet, notre approche consiste à exploiter les symétries pour réduire la table de transactions en supprimant certains items. À titre d'exemple si $\sigma = (a, b)$ est une symétrie binaire d'une table de transactions $D$, alors il est possible de supprimer

<footnote n="2">2. http://www.cril.univ-artois.fr/decMining/</footnote>
<table><caption>Table transactionnelle $D_1$</caption><thead><tr><td>tid</td><td>itemset</td></tr></thead><tbody><tr><td>001</td><td>s, o, t, m</td></tr><tr><td>002</td><td>s, p, o, b</td></tr><tr><td>003</td><td>c, a</td></tr><tr><td>004</td><td>e</td></tr></tbody></table>

<figure><img src="image_6.png" /><figcaption>Graphe associé à $D_1$</figcaption></figure>

b de toute transaction ne contenant pas a. Ce mécanisme a été est généralisé pour une symétrie de taille quelconque.

Dans un autre travail de recherche [Jabbour et al. 2013a], nous avons intégré l'élimination des symétries dans un algorithme de type *a priori*. À chaque niveau, lors de la génération de candidats, si un itemset est fréquent tous ses symétriques le sont aussi et inversement. Par conséquent, l'utilisation des symétries permet d'éviter d'interroger la table de transactions pour certains itemsets candidats et par conséquent d'obtenir un gain en temps de traitement. Notons que contrairement à l'approche proposée dans [Jabbour et al. 2012] où la sortie contient un sous-ensemble des itemsets (un représentant pour chaque classe d'équivalence).

### 3.3.6 Modèles Top-k et motifs Top-k

Dans les problèmes issues du monde réel, comme c'est le cas de la fouille de données, un problème important concerne l'énorme taille de la sortie rendant difficile la tâche d'extraire des informations pertinentes. Par conséquent, il est essentiel de contrôler la taille de la sortie lors de l'exploration des masses de données. Restreindre la génération des itemsets à des formes condensées comme les fermés, les maximaux, sont quelques-unes des approches largement étudiées dans la littérature. La contrainte de support consistue l'autre manière de limiter la taille de la sortie. Cette contrainte permet à l'utilisateur de contrôler, au moins dans une certaine mesure, la taille de la sortie en ne considérant que les itemsets dont le support dépasse un seuil prédéfini. Cependant, il est difficile pour l'utilisateur de fixer un seuil approprié. Comme indiqué dans [Fu et al. 2000], un seuil trop petit peut conduire à la génération d'un grand nombre de motifs, alors qu'une valeur trop élevée mène à un nombre très réduit. Basé sur un ordre complet entre les ensembles d'items, dans [Fu et al. 2000], les auteurs ont proposé d'extraire les *k* itemsets les plus pertinents de longueur arbitraire. Dans [Han et al. 2002], la tâche proposée consiste à extraire des itemsets fréquents et fermés dits top-*k* de longueur supérieure à une borne inférieure *min*, où *k* est le nombre d'itemsets fermés fréquents à extraire, et *min* est la longueur minimale de chaque ensemble d'éléments. Il a été démontré qu'il est beaucoup plus facile de définir la longueur minimale des ensembles d'objets à extraire que de définir le seuil de support habituel.

Le cadre logique des top-*k* SAT défini dans [Jabbour et al. 2013e, Jabbour et al. 2017d] peut aisément être combiné avec l'approche déclarative basée sur la logique propositionnelle pour énumérer les itemsets top-*k*. Nous avons étudié dans [Jabbour et al. 2013e] une telle adaptation. Deux algorithmes sont introduits pour calculer les itemsets top-*k* fréquents où la relation de préférence est le support. La borne de la contrainte du support est alors modifiée dynamiquement pour éviter l'énumération des itemsets qui ne sont pas top-*k*. Ce cadre a été également étendu au cas des
motifs séquentiels [Jabbour et al. 2017d].

### 3.3.7 Motifs skyPatterns

Pour pouvoir extraire les informations les plus pertinentes, il est nécessaire tout d'abord d'inclure au maximum dans le formalisme utilisé toutes les connaissances utilisateurs. Leur absence rend l'extraction fastidieuse et coûteuse et ne permet pas de distinguer les connaissances relevantes qui sont noyés dans le reste des connaissances extraites. En pratique, les items et les transactions peuvent avoir plus au moins d'importance selon le problème considéré. Les tentatives faites consistent à pondérer chaque item en lui associant un poids [Tao et al. 2003, Cai et al. 1998, Yun & Leggett 2005, Tao et al. 2003]. De plus, un poids sur les transactions est généralement dérivé en agrégeant les poids des items de chacune des transactions. La motivation principale derrière ceci, est de définir un support pondéré permettant de satisfaire la propriété de l'antimonotonie, propriété qui est généralement violée dans ce cadre. Cependant, dans les applications du monde réel, l'importance d'une transaction donnée n'est pas toujours corrélée aux poids de ces items. Par exemple, supposons que la base de données des transactions code un ensemble de documents publiés par les membres d'une institution de recherche dans les conférences internationales. Chaque publication associée à une conférence donnée (identifiant de transaction), implique un ensemble d'auteurs (articles). On peut associer un poids à chaque conférence en fonction de sa signification ou classement des conférences, tandis que les auteurs peuvent être pondérés en fonction de leurs âges, par exemple, les jeunes auteurs sont préférés. Dans ce contexte, un modèle intéressant peut être vu comme l'ensemble des jeunes auteurs publiant dans les conférences les plus sélectives.

Dans [Jabbour et al. 2016a], nous avons proposé un cadre logique traitant des préférences pour la fouille des itemsets fréquents prenant en compte les pondérations sur les items et les transactions. Ce modèle exploite la logique de pénalité [Walsh 2007, Brafman & Domshlak 2009, Kaci 2011, Domshlak et al. 2011] et les encodages basés sur SAT du problème d'extraction d'itemset. Les itemsets recherchés sont ceux pareto dominant ou skypatterns [Soulet et al. 2011].

### 3.3.8 Motifs ensemblistes sous incertitude

Jusqu'à présent, nous nous sommes intéressés à la fouille de données certaines c'est-à-dire que chaque élément apparaissant dans une transaction est connu avec certitude. Cependant, dans certaines applications du monde réel, les quantités massives de données sont souvent entachées d'imperfection et d'incertitude. Par exemple, les positions des objets obtenus par GPS ou RFID, les données collectées à partir de capteurs, et les calculs statistiques sont intrinsèquement bruyants. Par conséquent, le problème de trouver des itemsets sous incertitude a gagné un réel intérêt dans la communauté fouille de données. En effet, plusieurs approches et algorithmes ont été proposés [Chui et al. 2007, Chui & Kao 2008, Leung et al. 2008]. Le but des techniques mentionnées ci-dessus est de générer des modèles satisfaisant certaines contraintes spécifiques. En effet, de nombreuses propriétés (par exemple fréquence, maximalité, anti-monotonie) ont été étudiées et mises en œuvre dans différentes techniques de fouille de données.

En fouille d'itemsets sous incertitude, une table de transaction incertaine $D = \{T_1, T_2, ..., T_n\}$ est un ensemble de transactions où chaque item $a_i$ d'une transaction $j$ est associé avec une proba-
bilité $p(a_j, T_i) = p_{ji}$. La probabilité existentielle d'une itemset $I$ dans $T_i$ ($1 \le i \le n$), noté $p(I, T_i)$ est définie par $p(I, T_i) = \prod_{a_j \in I, I \subseteq T_i} p_{ji}$. Le support d'un itemset appelé *expected support* et noté ExpSN est défini $ExpSN(I, D) = \sum_{T_i \in D} p(I, T_i)$.

Le problème de la fouille des itemsets fréquents d'une table de transactions incertaine $D$ consiste à énumérer l'ensemble $\{I \in \Omega | \text{ExpSN}(I, D) \ge \text{minexpsupp}\}$.

Dans [Dlala et al. 2016a], nous avons proposé une extension de notre cadre déclaratif du cas certain au cas incertain. Dans ce cas, la contrainte de l'expected support peut s'écrire comme suit :

$$ \sum_{i=1}^{n} \prod_{a \in T_i} (p(a, T_i) \times p_a \wedge q_i + \neg p_a \wedge q_i) \geq \text{minexpsupp} \quad (3.5) $$

La contrainte (3.5) est particulière. Elle est non-linéaire et ses coefficients ne sont généralement pas entiers. Afin de tirer profit de cette contrainte, nous avons proposé une approche incremental énumérant les itemsets d'une taille fixée. L'objectif étant de rendre la contrainte de l'expected support linéaire pour une meilleure intégration dans les solveurs SAT. Notre approche permet de limiter le nombre des itemsets fréquents sans faux négatifs, i.e., les itemsets qui ne sont pas fréquents et que la relaxation n'a pas pu éliminer.

## 3.4 Fouille de règles d'association

Les résultats encourageants obtenus dans le contexte de la fouille des itemsets fréquents permettent d'étendre le cadre déclaratif aux règles d'association. À cela deux motivations : la première est que les techniques usuelles d'extraction de règles d'association suivent une approche en deux étapes. La seconde, est que la pertinence des règles à extraire est exprimée par des contraintes. Dans la suite nous présentons nos travaux dans ce cadre.

### 3.4.1 Approche symbolique

Dans [Boudane et al. 2016], nous avons proposé d'étendre l'encodage proposé pour les itemsets pour extraire les règles d'association. Cette extension est assez naturelle et obtenue en duplicate la contrainte (3.1) pour capturer les deux itemsets X et Y de la règle $X \to Y$. Les contraintes (3.6),(3.7), (3.8), (3.9), (3.10) et (3.11) traduisent le problème de recherche des règles d'association fréquentes et fermées.

$$ \bigwedge_{a \in \Omega} (\neg x_a \vee \neg y_a) \quad (3.6) $$

$$ \bigwedge_{i=1}^{m} (\neg p_i \leftrightarrow \bigvee_{a \in \Omega \setminus T_i} x_a) \quad (3.7) $$

$$ \bigwedge_{i=1}^{m} (\neg q_i \leftrightarrow \neg p_i \vee (\bigvee_{a \in \Omega \setminus T_i} y_a)) \quad (3.8) $$

$$ \sum_{i=1}^{m} q_i \geq \text{minsupp} \quad (3.9) $$

$$ \frac{\sum_{i=1}^{m} q_i}{\sum_{i=1}^{m} p_i} \geq \text{minconf} \quad (3.10) $$
$$ \bigwedge_{a \in \Omega} \left( \bigwedge_{i=1}^{m} (q_i \to a \in T_i) \to x_a \lor y_a \right) \qquad (3.11) $$

Notons que la contrainte (3.10) est réécrite sous la forme $\sum_{i=1}^{m} q_i - \minconf \sum_{i=1}^{m} p_i \geq 0$. Souvent $\minconf$ est exprimée en pourcentage i.e., $\minconf = k\%$ (avec $k \in \mathbb{N}$) permettant de réécrire (3.10) sous forme de la contrainte pseudo-booléenne suivante $100 \sum_{i=1}^{m} q_i + k \sum_{i=1}^{m} \neg p_i \geq k \times m$.

En plus de la fouille des règles d'association standards, dans [Boudane et al. 2016], nous avons montré que d'autres type de règles peuvent être encodées efficacement. C'est le cas par exemple des règles indirectes [Tan et al. 2000] dont le but est d'extraire les paires d'items $\{a, b\}$ tel que $a \to b$ n'est pas une règle valide (rare) par contre les deux items sont impliqués séparément dans des règles d'association fréquentes avec la même conséquence, i.e., il existe un itemset X tel que $\{a\} \to X$ et $\{b\} \to X$ sont des règles valides.

L'avantage de la recherche en une seule phase s'est confirmé dans les résultats expérimentaux qui ont montré que notre approche peut être compétitive vis à vis des approches spécialisées [Fournier-Viger et al. 2014].

### 3.4.2 Règles non-redondantes

De façon similaire au problème de la fouille des itemsets fréquents, l'ensemble des règles d'association peut être également très large. La taille d'un tel ensemble de règles n'aide pas l'utilisateur à retrouver facilement les informations potentiellement pertinentes. Une telle observation a conduit à différentes approches visant à supprimer les règles jugées redondantes [Bastide et al. 2000, Fournier-Viger & Tseng 2013, Zaki 2004, Gasmi et al. 2005]. Les règles de type conditions minimales conséquences maximales (MNR) [Kryszkiewicz 1998b] (voir définition 5) sont celles qui couvrent toutes les règles d'association [Kryszkiewicz 1998a].

**Définition 5 (Règle non redondante).** $X \to Y$ est une règle non redondante minimale ssi il n'existe pas de règle $X' \to Y$ différente de $X \to Y$ t.q. (i) $\text{Supp}(X \to Y) = \text{Supp}(X' \to Y')$, (ii) $\text{Conf}(X \to Y) = \text{Conf}(X' \to Y')$ et (iii) $X' \subseteq X$ et $Y \subseteq Y'$.

Pour éliminer les règles redondantes, généralement les approches spécialisées partagent les deux étapes suivantes : (1) trouver l'ensemble des générateurs minimaux (voir définition 6) et l'ensemble des itemsets fermés, et (2) générer les règles non-redondantes en considérant les deux ensembles déjà extraits dans la première étape.

**Définition 6 (Générateur minimal).** Soit X un itemset fermé. Un itemset $X' \subseteq X$ est un générateur minimal de X ssi $\text{Supp}(X', D) = \text{Supp}(X, D)$ et il n'existe pas $X'' \subseteq X$ t.q. $X'' \subset X$ et $\text{Supp}(X'', D) = \text{Supp}(X, D)$.

Nous avons proposé dans [Boudane et al. 2017b] d'étendre le cadre déclaratif proposé dans [Boudane et al. 2016] pour extraire les règles minimales non redondantes en une seule étape. La redondance est éliminée élégamment par ajout de la contrainte (3.12).

$$ \sum_{b \in \Omega} x_b \neq 1 \to \left( \bigwedge_{a \in \Omega} x_a \to \bigvee_{(T_i | a \notin T_i) \ b \notin T_i \cup \{a\}} \left( \bigwedge \neg x_b \right) \right) \qquad (3.12) $$
(3.12) est composée de plusieurs contraintes de cardinalité conditionnelles ($y \rightarrow \sum_{i=1}^{n} x_i \leq k$) (voir section 2.9). Par ailleurs, nous avons montré également qu'une restriction de notre encodage permet d'extraire les générateurs minimaux.

Nous avons exploré également une autre caractérisation des règles non-redondantes établi par Zaki et al. [Zaki 2004]. Il s'agit de règles d'association appelées *règles les plus générales* dont l'antécédent est le plus réduit et la conséquence (en termes d'inclusion) est une classe d'équivalente des règles ayant le même support et la même confidence.

## 3.5 Fouille de motifs séquentiels

Dans cette section, nous présentons un autre cadre déclaratif à base de contraintes pour extraire les motifs séquentiels. Une séquence de données peut être vue comme une séquence d'éléments, tandis que le motif peut être vu comme une sous-séquence pouvant contenir des caractères génériques ou des jokers en ce sens qu'ils correspondent à n'importe quel item [Parida et al. 2000, Pisanti et al. 2003, Arimura & Uno 2007].

### 3.5.1 Définitions et cadre formel

Soit $\Omega$ un ensemble fini d'items, appelé alphabet. Une sequence d'items $s$ sur $\Omega$ est une simple séquence de symboles $s_0 \cdots s_{n-1}$ appartenant à $\Omega$.

Nous notons par $|s|$ la taille et par $\mathcal{P}_s$ l'ensemble $\{0, \dots, |s| - 1\}$ de toutes les positions de ces symboles. *Un jocker* est un nouveau symbole $\circ$ qui n'est pas dans $\Omega$. Ce symbole peut représenter n'importe quel symbole de l'alphabet.

Un motif sur $\Omega$ est une séquence $p = p_0 \cdots p_{m-1}$, telle que $p_0 \in \Omega$, $p_{m-1} \in \Omega$ et $p_i \in \Omega \cup \{\emptyset\}$ pour $i = 1, \dots, m-2$.

Nous dirons que $p$ est inclu dans $s = s_0 \cdots s_{n-1}$ à la position $l \in \mathcal{P}_s$, notée $p \sqsubseteq_l s$, si $\forall i \in \{0 \cdots m-1\}$, $p_i = s_{l+i}$ or $p_i = \emptyset$. Nous dirons également que $p$ est inclut dans $s$, noté $p \sqsubseteq s$, si $\exists l \in \mathcal{P}_s$ tel que $p \sqsubseteq_l s$. La couverture de $p$ dans $s$ est définie comme l'ensemble $\mathcal{L}_s(p) = \{l \in \mathcal{P}_s | p \sqsubseteq_l s\}$. De plus, le support de $p$ dans $s$ est définit comme la valeur de $|\mathcal{L}_s(p)|$.

**Définition 7 (Problème FPS).** Soit $s$ une séquence, $p$ un motif et $\lambda \ge 1$ un seuil minimum, appelé également quorum. Nous dirons que $p$ est un motif fréquent dans $s$ if $|\mathcal{L}_s(p)| \ge \lambda$.

Le problème de la fouille des motifs fréquents dans une séquence d'items (FPS) consiste à calculer l'ensemble FPS($s$, $\lambda$) de tous les motifs fréquents.

Par exemple, considérons la séquence $s = aaccbcabcba$ et le motif $p = a \circ c$. Nous avons $\mathcal{L}_s(p) = \{0, 1, 6\}$, puisque $p \sqsubseteq_0 s$, $p \sqsubseteq_1 s$ et $p \sqsubseteq_6 s$. Dans ce cas, si le seuil minimum est égale à 3, alors le motif $p$ est un motif fréquent dans $s$.

**Définition 8 (Motif fermé).** Un motif fréquent $p$ d'une séquence $s$ est dit fermé si pour tout motif fréquent $q$ satisfaisant $p \sqsubseteq q$, il n'existe pas d'entier $d$ tel que $\mathcal{L}_s(q) = \mathcal{L}_s(p) + d$, avec $\mathcal{L}_s(p) + d = \{l + d \mid l \in \mathcal{L}_s(p)\}$.

Clairement, l'ensemble des motifs fréquents fermés est une représentation condensée de l'ensemble des motifs fréquents. En effet, les motifs fréquents peuvent être obtenus à partir des fermés en remplaçant les éléments par des caractères génériques (jockers).
Comme pour les motifs ensemblistes, la propriété de l'anti-monotonie est importante. Elle stipule que si $p_1$ et $p_2$ sont deux motifs tel que $p_1 \subseteq p_2$, alors si $|\mathcal{L}_s(p_2)| \ge \lambda$ alors $|\mathcal{L}_s(p_1)| \ge \lambda$.

### 3.5.2 Approche symbolique

Nous avons proposé deux approches pour la fouille des motifs séquentiels [Coquery et al. 2012, Jabbour et al. 2013c]. Nous décrivons ici l'encodage SAT pour le problème d'extraction de motifs séquentiels fréquents avec des caractères génériques dans le cas d'une séquences d'items proposée dans [Jabbour et al. 2013c]. À cette fin, nous fixons, sans perte de généralité, un alphabet $\Omega = \{a_1, \dots, a_k\}$, une séquence $s = s_0, \dots, s_{m-1}$ sur $\Omega$ et un seuil minimum $n \ge 1$. Nous associons à chaque item $a$ apparaissant dans $s$ un ensemble distinct de variables propositionnelles $k_a$, notées $p_{a,0}, \dots, p_{a,k_a-1}$ où $k_a = \max(\mathcal{L}_s(a)) + 1$. La variable $p_{a,l}$ est utilisée pour représenter le fait que l'élément $a$ est à la position $l$ dans le modèle candidat. De plus, nous utilisons $k_a = \max(\mathcal{L}_s(a)) + 1$ variables propositionnelles pour chaque item $a$ car l'ensemble $\{0, \dots, \max(\mathcal{L}_s(a))\}$ représente toutes les positions possibles de $a$. Clairement, la dernière position de $a$ dans chaque modèle candidat ne peut pas être supérieur à sa dernière position dans la séquence $s$. De plus, nous associons pour chaque position possible $l$ dans $0..m-1$ du modèle candidat une variable propositionnelle distincte, notée $q_l$.

Nous avons proposé plusieurs contraintes visant à capturer le motif recherché. (3.13) permet de forcer le modèle candidat à commencer par un item non générique. Celle de (3.14) permet de capturer les positions du motif candidat. elle est obtenue en exprimant que les valeurs de vérité des variables représentant les positions possibles du motif candidat (les variables de la forme $q_l$) sont déterminées à partir de celles des variables représentant les items et leurs positions possibles (les variables de la forme $p_{a,l}$)

$$ \bigvee_{a \in \Omega} p_{a,0} \qquad (3.13) $$

$$ \bigwedge_{0 \le l \le m-1} \left( \bigvee_{a \in \Omega, 0 \le i \le k_a-1} (p_{a,i} \wedge (l+i > m-1 \vee s_{l+i} \neq a)) \right) \leftrightarrow \neg q_l \qquad (3.14) $$

Cette formule exprime le fait que le modèle candidat n'est pas à la position $l$ si et seulement s'il existe un élément $a$ appartenant à ce modèle à la position $i$ tel qu'il n'est pas à la position $l+i$ dans la séquence. Par exemple, lorsque le modèle candidat commence par $a$ et que cet élément n'est pas à la position $l$ dans la séquence, nous savons que $l$ n'est pas une position pour le motif candidat. Notons que pour un modèle $\mathcal{B}$ de (3.14) et une position $l$ dans son modèle correspondant, si nous avons $\mathcal{B}(p_{a,l}) = 0$ pour chaque item $a$ avec $l \le k_a - 1$, alors cela signifie que le motif contient un joker à la position $l$.

Étant donnée un modèle $\mathcal{B}$ de (3.13) $\wedge$ (3.14) tel qu'il existe $0 \le l_0 \le m-1$ avec $\mathcal{B}(q_{l_0}) = 1$, nous utilisons $P_{\mathcal{B}}$ pour représenter le motif candidat associé à $\mathcal{B}$.

**Exemple 2.** Considérons la séquence $s = abaca$ construite sur $\Omega = \{a, b, c\}$. L'ensemble des variables associées à $a, b, c$ sont $\{p_{a,0}, p_{a,1}, p_{a,2}, p_{a,3}, p_{a,4}\}$, $\{p_{b,0}, p_{b,1}\}$, et $\{p_{c,0}, p_{c,1}, p_{c,2}, p_{c,3}\}$ respectivement. La formule (3.13) $\wedge$ (3.14) dans ce cas est :

$$ (p_{a,0} \vee p_{b,0} \vee p_{c,0}) \wedge $$
$$
\begin{align*}
((p_{b,0} \lor p_{c,0} \lor p_{a,1} \lor p_{c,1} \lor p_{c,2} \lor p_{a,3}) \leftrightarrow \neg q_0) \land \\
((p_{a,0} \lor p_{c,0} \lor p_{b,1} \lor p_{c,1} \lor p_{a,2} \lor p_{c,3} \lor p_{a,4}) \leftrightarrow \neg q_1) \land \\
((p_{b,0} \lor p_{c,0} \lor p_{a,1} \lor p_{b,1} \lor p_{c,2} \lor p_{a,3} \lor p_{c,3} \lor p_{a,4}) \leftrightarrow \neg q_2) \land \\
((p_{a,0} \lor p_{b,0} \lor p_{c,1} \lor p_{b,1} \lor p_{a,2} \lor p_{c,2} \lor p_{a,3} \lor p_{c,3} \lor p_{a,4}) \leftrightarrow \neg q_3) \land \\
((p_{b,0} \lor p_{c,0} \lor p_{a,1} \lor p_{b,1} \lor p_{c,1} \lor p_{a,2} \lor p_{c,2} \lor p_{a,3} \lor p_{c,3} \lor p_{a,4}) \leftrightarrow \neg q_4)
\end{align*}
$$

Soit $\mathcal{B}$ une interprétation booléenne sur la formule définie comme suit :

$$
- \mathcal{B}(p_{a,0}) = 1 \text{ and } \mathcal{B}(p_{b,0}) = \mathcal{B}(p_{c,0}) = 0;
$$

$$
- \mathcal{B}(p_{a,1}) = \mathcal{B}(p_{b,1}) = \mathcal{B}(p_{c,1}) = 0;
$$

$$
- \mathcal{B}(p_{a,2}) = 1 \text{ and } \mathcal{B}(p_{c,2}) = 0;
$$

$$
- \mathcal{B}(p_{a,3}) = \mathcal{B}(p_{c,3}) = 0;
$$

$$
- \mathcal{B}(p_{a,4}) = 0;
$$

$$
- \mathcal{B}(q_0) = \mathcal{B}(q_2) = 1 \text{ and } \mathcal{B}(q_1) = \mathcal{B}(q_3) = \mathcal{B}(q_4) = 0.
$$

On peut aisément remarquer que $\mathcal{B}$ est un modèle de la formule précédente. De plus, le motif $P_g$ corresponds à $a \circ a$.

Afin d'énumérer les motifs avec un support supérieur ou égale au seuil de support minimal $minsupp$, il suffit d'ajouter la contrainte de cardinalité suivante :

$$
\sum_{l=0}^{m-1} q_l \geq \minsupp \qquad (3.15)
$$

Pour énumération des motifs fréquents fermés, nous avons introduit une condition nécessaire, mais pas suffisante. L'idée de base consiste à maximiser le nombre d'éléments (différents du jocker) du côté droit du motif candidat.

$$
\bigwedge_{a \in \Omega, 0 \le i \le k_a - 1} \left( \bigwedge_{0 \le l \le m - 1} q_l \rightarrow s_{l+i} = a \right) \rightarrow p_{a,i} \quad (3.16)
$$

En d'autres termes, cette formule exprime le fait qu'un caractère générique est utilisé sur le côté droit du modèle candidat uniquement lorsque l'utilisation d'un item à la même position réduit le nombre de positions de ce motif. Par exemple, considérons la séquence *abcabc* et le motif *a* ◦ *c*. L'interprétation booléenne qui correspond à ce modèle ne satisfait pas la formule (3.16) puisque nous pouvons remplacer ◦ par *b* sans réduire le nombre de positions ({0,2}).

De la même manière que la formule (3.16), la formule suivante permet de maximiser le nombre d'éléments sur le côté gauche du motif candidat :

$$
\bigwedge_{a \in \Omega, 1 \le i \le k'_a - 1} \neg \left( \bigwedge_{0 \le l \le m - 1} q_l \rightarrow s_{l-i} = a \right) \quad (3.17)
$$

où $k'_a = n - \min(\mathcal{L}_s(a))$. Les entiers de 1 à $k'_a - 1$ représentent toutes les positions possibles de l'item $a$ sur le côté gauche du motif candidat. La formule (3.17) spécifie qu'aucun motif n'est accepté si nous pouvons ajouter un élément sur son côté gauche et conserver le même nombre de positions.
## 3.6 Clustering de formules booléennes

Les techniques de classification sont considérées comme une étape importante de l'analyse de données. On distingue deux types de classification : la classification est dite *supervisée* si on connaît à priori les descriptions des classes qu'on veut. Dans l'autre cas, celle dite *non-supervisée* ou *clustering* c'est à dire lorsque les classes sont construites à partir des caractéristiques des objets et dont le but est de regrouper des objets dans des catégories ou des classes de sorte que ceux qui appartiennent au même groupe ont des propriétés similaires en se basant sur des critères bien définis.

Nous nous sommes intéressés au clustering, une technique visant à partitionner un ensemble d'objets en sous-ensembles homogènes et bien séparés appelés clusters. L'homogénéité signifie que les objets dans un même cluster sont très similaire, par contre la séparation exprime qu'un objet dans un cluster doit être différent des objets des autres clusters. Le problème de clustering a été largement étudié pour son application dans plusieurs domaines, à savoir la biologie [Wittkop et al. 2010], l'analyse des images [Matas & Kittler 1995] et dans le commerce [Wang et al. 1999], etc. Les données peuvent être transactionnelles, séquentielles, arborescentes, des graphes, textes, ou même de nature symbolique. Ce dernier type de données est particulièrement adapté à la modélisation d'objets complexes et hétérogènes généralement décrits par un ensemble de variables de différents types e.g., intervalles, multi-catégorielles ou modaleds [Billard & Diday 2012, Diday & Esposito 2003]. Nous pouvons également citer le regroupement conceptuel, proposé il y a plus de trente ans dans [Michalski 1980], défini comme une tâche d'ap preventissage automatique qui considère un ensemble de descriptions d'objets (événements, faits, observations, etc.) et produit un système de classification sur eux. Le regroupement conceptuel ne se limite pas à partitionner les données, mais génère également des clusters qui peuvent être résumés par une description conceptuelle.

Aujourd'hui, les données sont de nature complexe et hétérogène. Ces données complexes peuvent représenter les désirs des clients ou les préférences recueillies par différentes façons possibles issues de sondages ou de questionnaires. Par exemple, on peut citer les systèmes de configuration généralement conçus pour fournir des produits personnalisés répondant aux différentes exigences du client habituellement modélisé par des contraintes ou des formules logiques [Hotz et al. 2014].

Dans [Boudane et al. 2017a], nous avons introduit un nouveau cadre de clustering, dans lequel les objets complexes sont décrits par des formules booléennes. Cela est tout à fait plausible. Considérons le cadre d'un sondage où les questions posées sont ordonnées et certaines questions dépendent des réponses des précédentes questions. Cela peut parfaitement être formulé en logique propositionnelle.

La question que nous avons considéré est comment partitionner un ensemble des formules propositionnelles S. Ce problème qu'on note $\mathcal{P}(k, S)$ est défini formellement comme suit.

**Définition 9** (Solution de $\mathcal{P}(k, S)$). Soit $S = \{\Phi_1, \dots, \Phi_n\}$ un ensemble de formules propositionnelle. C est une solution de $\mathcal{P}(k, S)$ ssi C est une partition de S de taille k et pour tout $C_i \in C$, $C_i \not= \emptyset$.

Notons que la contrainte $C_i \not= \emptyset$, dite contrainte de cohérence, exige la cohérence logique de chaque cluster, i.e., si $C_i = \{\Phi_1^i, \dots, \Phi_m^i\}$, alors $\Phi_1^i \wedge \dots \wedge \Phi_m^i \not= \emptyset$.
Les algorithmes de l'état de l'art de clustering peuvent être adaptés au cas des objets de type formules propositionnelles. Néanmoins, cette adaptation requiert de définir une distance (ou similarité) entre deux formules, ce qu'est un centroïde d'un cluster de formule, et une fonction objective à optimiser.

Pour définir une distance entre formules, nous avons considéré le coefficient de similarité de Jaccard, issue de la mesure de similiarité de Tversky [Tversky 1977], et définit comme ci-dessous. En effet, une formule booléenne peut être vue comme l'ensemble de ces modèles (forme normale disjonctive DNF).

$$s_J(\Phi_1, \Phi_2) = \frac{|M(\Phi_1 \wedge \Phi_2)|}{|M(\Phi_1 \vee \Phi_2)|}$$

À partir de ce coefficient, on peut définir la mesure de distance $d_J(\Phi_1, \Phi_2) = 1 - s_J(\Phi_1, \Phi_2)$.

Intuitivement, étant donné un cluster $C_i$ (sous-ensemble de formules), le centroïde peut être défini comme la conjonction de ses formules $O_{C_i} = \bigwedge_{\Phi \in C_i} \Phi$. Cette formulation peut être améliorée en considérant la distance de hamming avec les modèles qui ne sont pas dans l'intersection. La formulation de la fonction objective est similaire à celle définie de manière standard suivante :

$$C^* = \underset{C}{\operatorname{argmin}} \sum_{i=1}^{k} \sum_{C_i \in C} Q(C_i)$$

Suivant la définition de la qualité du cluster, plusieurs fonctions peuvent être instanciées. $Q(c)$ peut être substituée par la somme des distances au centroïde (distance euclidienne) $\sum_{\Phi \in C_i} d_J(\Phi, O_{C_i})$. Dans [Boudane et al. 2017a], nous avons considéré celle de la définition 10.

**Définition 10.** Soit $C = \{\Phi_1, \dots, \Phi_n\}$ un cluster de formules booléennes. Nous définissons la qualité de $C$ comme :

$$Q(C) = \frac{|M(\Phi_1 \wedge \dots \wedge \Phi_n)|}{|M(\Phi_1 \vee \dots \vee \Phi_n)|}$$

Dans [Boudane et al. 2017a], nous avons montré que les adaptions proposées des algorithmes de l'état de l'art du clustering comme le k-means [Macqueen 1967], les algorithmes hiérarchiques [Sneath & Sokal 1973, Karypis et al. 1999] et les algorithmes basés sur la densité [Ester et al. 1996] peuvent échouer à fournir un regroupement adéquat en satisfaisant le nombre de clusters fixé à cause de la contrainte de cohérence des clusters. Afin de pallier ce problème, nous avons introduit un nouvel algorithme hiérarchique descendant pour une représentation ensembliste des formules. Plus précisément, notre algorithme procède par une phase de division en se basant sur la notion d'ensemble intersectant<fnref n="3" /> (en anglais Hitting Set) de l'hypergraphe dont les sommets est l'union des modèles des formules et les hyper-arêtes sont les modèles de chaque formule. Le calcul du premier ensemble intersectant minimum $H^0$ permet de disposer des premires centroïdes. Cela permet de former les clusters de formules en attribuant chaque formule à un cluster si l'un de ces modèles est un centroïde. D'ailleurs, $|H^0|$ constitue la borne inférieure du clustering qu'il est possible de réaliser sous la contrainte de cohérence des clusters. Si $|H^0| > k$, alors la division est réitérée en choisissant le cluster de mauvaise qualité $C_m$ (voir Définition 10) et en remplaçant $C$

<footnote n="3">3. Un sous-ensemble $H$ est dit ensemble intersectant d'un ensemble d'ensembles $F$ si $\forall E \in F, H \cap E \neq \emptyset$. De plus, $H$ est dit irréductible (ou minimal) si tout sous-ensemble strict de $H$ n'est pas un ensemble intersectant</footnote>
par $C = \bigcup_{\Phi \in C_m} (\Phi \setminus (\bigcap_{\Phi' \in C_m} \Phi'))$ et $k = k - |H^0|$ où les modèles communes aux formules du cluster sont préalablement supprimés avant la division, jusqu'à l'obtention des $k$ clusters demandés.

Le calcul d'ensemble intersectant minimal est connu pour être un problème NP-difficile et l'évaluation de la qualité des clusters fait intervenir l'appel à un oracle #SAT appartenant à la classe #P-Complet lorsque la forme normale disjonctive des formules est considérée. Cela constitue deux problèmes de complexité élevée. Pour réduire la complexité calculatoire et éviter principalement l'appel à l'oracle #SAT, nous avons proposé une formulation en MaxSAT incrémentale permettant de réaliser un tel clustering.
<figure><img src="image_7.png" /></figure>
## CHAPITRE 4
# Graphes

### 4.1 Introduction

Les graphes constituent un outil général et puissant de modélisation des relations structurelles entre les données. Ils ont été largement utilisé dans plusieurs domaines d'application, incluant les interactions en bio-informatique, l'analyse de liens dans les réseaux, les documents XML, etc. L'importance prise par les réseaux sociaux depuis quelques années a rendu ce domaine de plus en plus attractif et incontournable et remis au goût du jour certaines questions comme l'étude des structures topologiques des graphes, la détection de communautés et regroupement [Newman & Girvan 2004, Xie et al. 2011, Gregory 2009, Shen et al. 2009, Yang & Leskovec 2013] mais dans un environnement où les données sont volumineuses nécessitant des approches pour compacter ces représentations en vue de leur traitement.

Généralement, les réseaux réels impliquent des concentrations élevées d'arêtes dans des groupes spéciaux de sommets, et de faibles concentrations entre ces groupes. À titre d'exemple, dans le graphe de la toile mondiale (www), des concentrations denses peuvent correspondre à des groupes de pages traitant de sujets identiques ou connexes. En raison de leur degré de connectivité, ces communautés/clusters peuvent parfois correspondre à certaines classes de graphes tels que les (quasi)-cliques, les graphes bipartis, etc. Cependant, l'extraction de structures dans les graphes des bases de données sont coûteuses en raison de la complexité des graphes de données de plus en plus volumineux. Par conséquent, il est difficile de comprendre l'information/structure codée dans ces graphes par de simples visualisations.

Dans la suite nous tentons à travers les travaux effectués dans le cadre de la détection de communautés dans les graphes et l'approche de compression pour une représentation plus concise de ces derniers de comprendre les structures des réseaux complexes.

#### 4.1.1 Définitions et notations

Nous considérons un réseau comme un graphe non orienté $G = (V, E)$ constitué d'un ensemble de sommets $V$ et d'un ensemble d'arêtes $E \subseteq V \times V$ qui lient des paires de sommets. Pour de raisons de simplicité, $n$ désigne le nombre de sommets dans $G$ (c'est-à-dire $n = |V|$) et $m$ le nombre d'arêtes de $G$ (c'est-à-dire $m = |E|$). Le degré d'un sommet $u \in V$, désigné par $d(u)$, est défini comme étant le nombre d'arêtes incidentes. Pour deux sommets $u, v \in V$, on note par $dist(u, v)$ la distance entre $u$ et $v$. Étant donné une arête $e = (u, v) \in E$, la distance entre $e$ et un sommet $w \in V$ est définie comme étant $dist(e, w) = \min\{dist(u, w), dist(v, w)\}$. Si pour tout $u, v \in V$, $(u, v) \in E$, alors $G$ représente une clique. Si $V = X \cup Y$ tel que $X \cap Y = \emptyset$ et $X \times X \cap E = \emptyset$ et $Y \times Y \cap E = \emptyset$, alors $G$ est dit biparti. De plus, si $X \times Y = E$, alors $G$ est dit biparti complet. Nous notons un graphe biparti par $G(X \cup Y, E)$.
En théorie des graphes, une communauté est définit comme un groupe de sommets plus étroitement connectés les uns avec les autres qu'avec le reste du réseau. Dans les graphes réels, les sommets s'organisent en groupes étroitement liés, appelés communément *communautés*, clusters ou modules. Souvent, certaines communautés dans les réseaux peuvent se chevaucher car les sommets peuvent appartenir à plusieurs communautés à la fois.

Dans la littérature, différentes mesures ont été proposées pour quantifier la qualité des communautés. Parmi celles-ci, on peut citer la *modularité* [Newman & Girvan 2004] et la fonction $F_1$ *score*.

**Modularité** : Étant donné un découpage en communautés disjointes ou recouvrantes, la modularité permet d'évaluer leurs qualités par le calcul de la différence entre la proportion de liens se trouvant à l'intérieur des communautés et la proportion de liens qui pourraient être à l'intérieur de ces mêmes communautés, en moyenne, dans un graphe aléatoire de même distribution de degrés. Cette fonction est définie comme suit :

$$Q = \frac{1}{2m} \sum_{C \in C_G} \sum_{i,j \in C} \frac{1}{O_i O_j} \left[ A_{ij} - \frac{d_i d_j}{2m} \right] \quad (4.1)$$

où $C_G$ est l'ensemble de communautés dans le graphe $G$; $O_u$ est le nombre de communautés auxquelles appartient le sommet $u$; et $d_u$ est le degré du sommet $u$.

**F₁ score** : Soient $\hat{C}$ (resp. $C^*$) l'ensemble de communautés détectées (resp. réelles) associées au graphe $G$. La fonction $F_1$ score vise à quantifier le niveau de correspondance entre $C^*$ et $\hat{C}$ [Yang & Leskovec 2013]. Autrement dit, nous devons déterminer quelle communauté $C_i \in C^*$ correspond à $\hat{C}_i \in \hat{C}$. Ensuite, le score $F_1$ est défini comme la moyenne de la communauté réelle la plus proche de chaque communauté détectée et la meilleure communauté détectée correspondant à chaque communauté réelle. Formellement, cette fonction est définie de la manière suivante :

$$\frac{1}{2} \left( \frac{1}{|C^*|} \sum_{C_i \in C^*} F_1(C_i, \hat{C}_{g(i)}) + \frac{1}{|\hat{C}|} \sum_{\hat{C}_i \in \hat{C}} F_1(C_{g'(i)}, \hat{C}_i) \right) \quad (4.2)$$

où la meilleure correspondance entre $g$ et $g'$ est définie comme suit :

$$g(i) = \arg \max_j F_1(C_i, \hat{C}_j), \quad g'(i) = \arg \max_j F_1(C_j, \hat{C}_i)$$

et $F_1(C_i, \hat{C}_j)$ est la moyenne harmonique de la précision<fnref n="1" /> et le rappel<fnref n="2" />.

## 4.2 Détection de communautés

La découverte des structures cachées d'un graphe est un problème fondamental dans l'analyse de grands graphes de données. Dans la littérature, plusieurs approches ont été proposées pour résoudre ce problème difficile. De plus, la détection de communautés dans un graphe est une méthode efficace pour comprendre les caractéristiques des réseaux de données. Elle constitue une étape cruciale dans l'étude de la structure et la dynamique des réseaux sociaux et biologiques

<footnote n="1">1. La précision entre deux communautés $C$ et $C'$ est définie comme suit : $\frac{|C \cap C'|}{|C|}$.</footnote>

<footnote n="2">2. Le rappel entre deux communautés $C$ et $C'$ est définie comme suit : $\frac{|C \cap C'|}{|C'|}$.</footnote>
[Newman 2010, Adamcsek et al. 2006]. Par exemple, la détection de communautés permet de mieux comprendre les mécanismes métaboliques et les interactions protéine-protéine (IPP), les réseaux trophiques écologiques, les réseaux sociaux, les réseaux de collaboration, les réseaux d'information de documents interconnectés, et même les réseaux de produits co-achetésc. Dans la suite, nous présentons nos différents travaux effectués dans cette thématique de recherche.

4.2.1 Communauté k-liée centrée

Dans [Jabbour et al. 2017c], nous avons proposé une nouvelle approche de détection de com-
munautés avec chevauchement dans les grands réseaux en se basant sur la logique proposition-
nelle. Utiliser la satisfiabilité pour étudier les réseaux complexes met en lumière une nouvelle
perspective pour combiner les progrès dans la résolution du problème SAT et la détection des com-
munautés. Notre approche consiste à décomposer un graphe G(V, E) donné en communautés tout
en fixant le diamètre de chaque communauté comme c'est le cas dans [Alba 1973]. Pour ce faire,
nous avons défini la notion de communauté k-liée centrée associée à un sommet u comme l'en-
semble de sommets qui sont à une distance au plus k de u, i.e., C(u, k) = {v ∈ V | dist(u, v) ≤ k}.
Cela constitue une manière particulière de fixer le diamètre de la communauté. Dès lors, nous
avons formulé le problème de détection de communautés en un problème de recherche d'une dé-
composition minimale ou maximale en groupes k-liées. En d'autre termes, nous recherchons un
sous-ensemble minimal ou maximal S ⊆ V de sommets centraux tels que tout autre sommet est à
une distance au plus k d'un des sommets de S.

$$
\min/\max \{|S|, S \subseteq V \text{ et } f(S) = V\} \quad f(S) = \bigcup_{u \in S} C(u, k) \quad (4.3)
$$

Ensuite, nous avons exprimé une variante de (4.3) en un problème d'optimisation MaxSAT
dont la formulation est la suivante :

$$
\bigwedge_{u \in V} (x_u \rightarrow \bigwedge_{v \in C(u, \frac{k}{2})} \neg x_v) \qquad (4.4)
$$

$$
\bigwedge_{u \in V} \bigvee_{v \in C(u, \frac{k}{2})} x_v \qquad (4.5)
$$

$$
\min / \max \sum_{u \in V} x_u \quad \text{subject to (4.4) } \wedge (4.5) \qquad (4.6)
$$

Des évaluations empiriques ont permis de conclure que la valeur *k* = 4 est la plus appro-
priée, permettant de maximiser les valeurs de modularité et de F₁ score. Nous avons égale-
ment proposé une nouvelle méthode à base de préférences pour étendre le modèle défini dans
[Jabbour et al. 2017c]. L'idée consiste à prendre en considération l'importance de chaque som-
met par rapport à son voisinage en donnant plus de poids aux sommets dont le voisinage est plus
connecté. Plusieurs notions existent pour caractériser l'importance d'un sommet dans un graphe.
Parmi lesquelles, on trouve le degré de centralité, la densité, etc. Notre approche consiste à prendre
en compte les préférences dans le modèle [Jabbour et al. 2017c] afin de sélectionner un centroïde
parmi les sommets candidats. Pour cela, le score de chaque sommet *u* est calculé en fonction de
la densité de la communauté $C_u$ où $u$ est le centroïde de $C_u$. Formellement, la densité de $u$ est calculée par la fonction suivante :

$$g(C_u) = \frac{2 \times m_{C_u}}{n_{C_u}(n_{C_u} - 1)}$$

où $m_{C_u}$ est le nombre d'arêtes entre les sommets de $C_u$ et $n_{C_u} = |C_u|$.

Ensuite, le sommet $u$ est un centroïde si $g(C_u)$ est maximale. Le modèle utilise une nouvelle fonction objective qui intègre des poids dans le premier modèle [Jabbour et al. 2017c]. Cette fonction est exprimée de la manière suivante :

$$\min / \max \sum_{u \in V} w_u \times x_u \quad \text{subject to (4.4) } \land \quad (4.5) \qquad (4.7)$$

### 4.2.2 Communauté k-clique-star

L'identification des communautés dans un réseau social peut être considérée comme un problème de densité des sous-graphes. Dans ce contexte, différents modèles mathématiques ont été étudiés pour l'extraction des communautés dans les réseaux du monde réel. Le modèle le plus intuitif pour l'analyse de réseaux sociaux est sans aucun doute la clique [Luce 1950]. Une telle structure, de préférence clique maximale, constitue la structure communautaire idéale, que l'on voudrait trouver. Cependant, générer des communautés avec une telle propriété structurelle est intraitable. De plus, la clique est trop restrictive. En effet, les cliques de petite taille sont les plus fréquentes dans les réseaux du monde réel, tandis que des cliques de grandes tailles sont généralement rares [Cohen 2008]. Autrement dit, les graphes qui apparaissent dans de nombreux réseaux réels ont plutôt une topologie de "petit monde" dans laquelle les sommets sont fortement groupés avec une longueur du chemin entre eux très faible [Wasserman & Faust 1994]. Par conséquent, d'autres formes plus souples de sous-graphes cohésifs ont été proposées. Leskovec a présenté un modèle basé sur la distance appelé k-clique [Leskovec et al. 2010], et Alba a proposé un modèle basé sur le diamètre appelé k-club [Alba 1973]. D'une manière générale, ces modèles relaxent l'accessibilité entre les sommets de 1 à k. Cependant, ces structures ne permettent pas de résoudre non plus les problèmes d'énumération ou l'intraitabilité du calcul. En outre, d'autres travaux se sont focalisés sur le degré de contrainte de la clique, comme le k-plex [Saito et al. 2008], le k-core[Seidman 1978], le DN-Graph [Wang & Cheng 2012], et le k-truss [Shao et al. 2014].

Dans [Jabbour et al. 2018], grâce à l'observation qu'une clique de taille $k$ peut être vue comme deux cliques de taille $k'$ et $k''$ telle que $k = k' + k''$ et les deux cliques forment un graphe biparti, nous avons proposé de relaxer l'une des deux cliques donnant lieu à la notion de k-clique-star (voir définition 11). Cette structure consiste en une clique et un ensemble de sommets (externe à la clique) connectés à tous ses éléments. Ici la clique est une sorte de centroïde.

**Définition 11 (k-clique-star).** Un graphe $G = (V, E)$ est dit k-clique-star ($k > 1$) s'il existe un sous-graphe $G' = (V', E')$ de $G$ tel que $G'$ est un k-clique, et $\forall u \in V \setminus V'$, $\forall v \in V'$, $(u, v) \in E$. $G'$ est appelé le centroïde de $G$.

Nous avons également montré que cette structure permet de garantir une borne de densité. Nous avons proposé de décomposer le graphe en un ensemble de k-clique-star maximaux. Cet
ensemble n'est autre que les communautés recherchées. Nous avons montrons aussi que chaque *k-clique-star* représente une extension d'une clique maximale par des arêtes additionnelles.

### 4.2.3 Compression de graphes à base contraintes pseudo-booléennes

Beaucoup de problèmes du monde réel sont modélisés efficacement comme des graphes. Cependant, ces représentations sont généralement de très grande taille conduisant à un calcul de complexité croissant dans le traitement de tels graphes. Partant de l'observation qu'un graphe arbitraire contient des structures cachées correspondantes à des classes particulières de graphes, dans [Jabbour et al. 2016c] nous nous sommes intéressés à la question de découvrir ces structures spécifiques et de les exploiter pour améliorer la compacité en se basant sur le formalisme logique. Pour cela, nous avons associé à chaque sommet une variable propositionnelle. Lorsqu'il n'y pas d'ambiguïté, nous confondons chaque sommet et sa variable booléenne associé.

Pour illustrer ce propos, considérons le cas de trois exemples de graphes représentés dans la figure 4.1. Le premier est la clique. Il est facile de déduire qu'il existe une bijection entre les arêtes de $G$ et les impliquants premiers de la contrainte linéaire suivante. En effet, toute paire $(x_i, x_j)$, $i \neq j$ est un modèle de la contrainte.

$$ \sum_{i=1}^{n} x_i = 2 $$

Le second est le cas de la quasi-clique, i.e., la clique avec une arête en moins $(x_1, x_2)$. Tout couple de variables solution de l'équation suivante est une arête de la quasi-clique.

$$ x_1 + x_2 + 2 \sum_{i=3}^{n} x_i \geq 3 $$

Le dernier cas intéressant est celui des graphes bipartis complets. Dans ce cas, la même correspondance existe entre les arêtes du graphe et les modèles de l'équation linéaire suivante :

$$ 2 \sum_{u \in U} x_u + 3 \sum_{v \in V} x_v = 5 $$

<figure><img src="image_8.png" /><figcaption>a. clique</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>b. quasi-clique</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>c. biparti parfait</figcaption></figure>

<caption>FIGURE 4.1 – Exemples de graphes</caption>

Les exemples précédents montrent que le formalisme logique peut offrir une alternative de représentation de choix pour les graphes tout en réduisant la taille de la représentation. Dans
[Jabbour et al. 2016c], nous avons décrit les classes de graphes bipartis G = (X ∪ Y, E) pouvants être exprimés par des contraintes pseudo booléennes de la forme (4.8).

$$
k \leq AX^T + BY^T \leq k', \quad A \in \mathbb{Z}^n, B \in \mathbb{Z}^m \qquad (4.8)
$$

Nous avons prouvé que les graphes imbriqués (Figure 4.2.a) et les graphes séquences (Figure 4.2.b), peuvent être exprimés d’une manière plus succincte en utilisant ces contraintes. Nous avons également présenté un algorithme basé sur une heuristique capable de partitionner un graphe en un ensemble de sous-graphes imbriqués disjoints.

<figure><img src="image_11.png" /></figure>

<figure><img src="image_12.png" /><figcaption>FIGURE 4.2 – Quelques classes de graphe</figcaption></figure>
# Représentation de connaissances & Raisonnement

## 5.1 Introduction

Le raisonnement en présence d'incohérence est un thème qui a reçu une attention particulière dans la littérature. En effet, il existe différentes situations où nous pouvons être ramener à travailler avec des informations conflictuelles. À titre d'exemple, lorsque différents experts ou capteurs fournissent des données contradictoires, plusieurs règles sont simultanément applicables dont les conclusions sont contradictoires, ou encore plusieurs avis divergents concernant l'évaluation d'un candidat ou d'un objet. Il est usuel qu'en présence d'incohérences de ne pas utiliser les méthodes classiques de déduction, qui trivialisent en inférant toutes les formules du langage. Il est donc primordial que la capacité de raisonner en présence de ces incohérences soit assurée.

Il peut s'avérer utile d'évaluer à quel point une base de connaissances est incohérente pour s'en servir afin de choisir par exemple, parmi un ensemble de bases, la base la moins conflictuelle. De même, savoir quelles sont les formules qui apportent beaucoup ou peu de conflit à la base de connaissances, peut être d'une grande utilité pour de nombreuses tâches, par exemple pour identifier les formules les plus problématiques afin de résoudre les conflits. L'autre possibilité lorsque l'on veut raisonner non trivalement à partir d'une base incohérente est de considérer certaines approches comme les logiques paraconsistantes, la théorie de l'argumentation, ou encore les méthodes basées sur les ensembles maximaux cohérents.

Ce qui suit résume nos contributions portant sur l'évaluation de la qualité des données dont les modes d'acquisition sont variés et présentent différentes incohérences et imperfections. Nous présentons ensuite nos travaux sur les approches argumentatives pour le raisonnement en présence des ontologies incohérentes.

## 5.2 Gestion et mesure de l'incohérence

L'incohérence est souvent inévitable dans les bases de données et dans les systèmes multi-agents. Quantifier le degré l'incohérence des bases de connaissances des agents facilite la compré-hension d'un agent de son environnement et lui fournit une aide pour la prise de décision. Certains travaux ont émergé ces dernières années pour quantifier d'incohérence des bases de connaissances comme celles fondés sur les sous-ensembles minimaux incohérents [Hunter & Konieczny 2010, Grant & Hunter 2011, Mu et al. 2011, Xiao & Ma 2012], les sous-ensembles maximaux cohérents, ou celles qui consistent à calculer la proportion du langage affectée par l'incohérence
[Konieczny et al. 2003, Oller 2004, Grant & Hunter 2008, Ma et al. 2011]. Les mesures appartenant à cette deuxième catégorie sont souvent basées sur une sémantique paraconsistante car cela offre des modèles à des bases de connaissances logiquement incohérentes.

## 5.2.1 Définitions et notations

Nous considérons une base de connaissances *K* formée d'un ensemble fini de formules propositionnelles. Pour un sous-ensemble *S*, |*S*| indique sa cardinalité. Nous dirons que *K* est incohérente si *K* ⊢ ⊥.

Un ensemble de formules *M* est dit ensemble minimal incohérent (MUS) de *K* ssi (1) *M* est incohérent et (2) tout sous-ensemble strict de *M* est cohérent. L'ensemble des ensembles minimaux incohérents de *K* est noté *MUSes*(*K*). Les MUSes constituent les explications les plus fines, en termes du nombre de formules, de l'incohérence de la base de connaissances *K*. Bien évidement, les formules qui ne font parti d'aucun MUS sont dites des formules libres. L'ensemble des formules libres de *K* est noté *free*(*K*). Dans le cas contraire, elle est dite non libre. Nous notons cet ensemble *unfree*(*K*). Parallèlement à la notion de MUS, on peut définir les ensembles maximaux cohérents. Un ensemble *M* est dit maximal cohérent si (1) il est cohérent et (2) tout sur-ensemble strict de *M* est incohérent. Nous notons *MSSes*(*K*) l'ensemble des sous-ensemble maximaux cohérents de *K*. Il existe une dualité entre les MUSes et les MSSes via la notion d'ensemble intersectant.

Formellement, une mesure d'incohérence peut être définie comme suit :

**Définition 12.** *Etant donné un langage propositionnel $\mathcal{L}$. Une mesure d'incohérence est une fonction $I : \mathcal{L} \to \mathbb{R}^+$ qui associe une valeur réelle pour toute base $K \in \mathcal{L}$.*

Afin de définir des mesures d'incohérence rationnelles, plusieurs recherches se sont intéressés à définir des propriétés qu'une mesure idéale doit satisfaire [Hunter & Konieczny 2010, Jabbour et al. 2014c, Besnard 2014]. Dans la suite nous listons les plus importantes parmi elles.

- *Cohérence* : $I(K) = 0$ ssi $K$ est cohérente.

- *MinInc* : $I(M) = 1$ if $M \in MUSes(K)$.

- *Indépendance Libre* : $I(K \cup \{\alpha\}) = I(K)$ si $\alpha \in free(K \cup \{\alpha\})$.

- *Monotonie* : si $K \subseteq K'$, alors $I(K) \le I(K')$.

- *Additivité* : $I(K_1 \cup \dots \cup K_n) = \sum_{i=1}^n I(K_i)$ si $MUSes(K_1 \cup \dots \cup K_n) = MUSes(K_1) \uplus \dots \uplus MUSes(K_n)$, tel que $\uplus$ est l'union disjointe sur la famille d'ensembles.

- *Dominance* : si $\alpha \preceq \beta$ et $\alpha \vdash \beta$, alors $I(K \cup \{\beta\}) \le I(K \cup \{\alpha\})$.

Dans nos travaux présentés ci-dessous, nous avons pris le soin à la fois de critiquer certaines de ces mesures et d'en proposer des nouvelles tout en argumentant à travers de nouvelles propriétés.

## 5.2.2 Mesure de degré d'incohérence via les preuves minimales

Peu de travaux ont été proposés pour la caractérisation de la responsabilité de chaque formule d'une base de connaissances dans l'incohérence de la base. Le problème avec ces mesures est qu'elles ne donnent pas des résultats très satisfaisants parce qu'elles affectent d'une manière uniforme le degré d'incohérence entre les différents formules responsables du conflit. Pour améliorer
le comportement de cette famille de mesures, nous avons introduit dans [Jabbour & Raddaoui 2013] la notion de *preuve minimale* (ensemble minimal de formules à l'origine de l'inférence d'un littéral) afin de caractériser dans un cadre uniforme la responsabilité/participation de chaque formule dans l'incohérence de toute la base originale. Intuitivement, dans cette approche le degré d'incohérence d'une formule est le nombre de fois où cette formule intervient dans la production de conflit dans la base. Cela permet d'inspecter plus finement les conflits au niveau des formules. De manière assez naturelle, notre mesure s'étend pour quantifier à quel point une base de connaissances est incohérente. Notre approche satisfait les propriétés logiques de base que toute mesure d'incohérence intuitive doit satisfaire comme la consistance et la monotonie. Par ailleurs, nous avons montré l'utilité de cette mesure de conflit pour la résolution de l'incohérence dans les bases de connaissances.

Il est intéressant de noter qu'il a été prouvé dans [Thimm 2016] que notre mesure d'incohérence est la mesure la plus expressive de toutes les mesures de l'état de l'art.

### 5.2.3 Additivité restreinte

Dans [Jabbour et al. 2014c], nous nous somme intéressés à la propriété d'additivité. Cette propriété permet d'additionner le degré de conflit des sous-bases sous la condition que les seuls MUSes déductibles à partir de leur union est l'union des MUSes des sous-bases. Nous avons argumenté en faveur de l'insuffisance de cette condition et l'étendons en requérant également la disjonction en termes de formules non libre entre les sous-bases (voir Définition 13).

**Définition 13** (Indépendance-Additivité). *Soient $K$ et $K'$ deux bases de connaissances. $I(K \cup K') = I(K) + I(K')$ si $un\,free(K) \cap un\,free(K') = \emptyset$ et $MUSes(K \cup K') = MUSes(K) \cup MUSes(K')$.*

À la lumière de cette nouvelle propriété, nous avons établi une borne inférieure des mesures d'incohérences. Cette borne a donné lieu à une nouvelle métrique qui consiste à calculer la taille maximale de l'ensemble de MUSes disjoints deux à deux (i.e, formant un set packing maximal) et qui est fermé par union (Définition 14).

**Définition 14** (Set packing). *Soit $U$ un univers et $S$ une famille de sous-ensemble de $U$. Un set packing est un sous-ensemble $P \subseteq S$ tel que, $\forall S_i, S_j \in P$ avec $S_i \neq S_j, S_i \cap S_j = \emptyset$.*

Dans [Jabbour et al. 2016b], nous avons généralisé cette notion aux ensembles. Cela a donné lieu à un nouveau problème appelé *set packing fermé* qui est une extension du problème bien connu de *set packing* proposé et étudié en recherche opérationnelle. Nous avons montré que ce nouveau problème est aussi difficile que le set packing standard de point de vue de complexité (Décider s'il existe un set packing fermé de taille inférieure ou égale à $k$ est NP-Complet). La fermeture par union peut être obtenue en utilisant la définition suivante :

**Définition 15** (Fermeture). *Soit $U$ un univers et $S$ une famille de sous-ensemble de $U$. Nous définissons la fonction $f_S : 2^S \to 2^S$ comme $f_S(P) = \{S_i \in S \mid S_i \subseteq \cup_{S' \in P} S'\}$. Alors, un set packing $P \subseteq S$ est dit fermée si $P$ est un point fixe de la fonction $f_S$, i.e., $f_S(P) = P$.*

Par ailleurs, nous avons proposé une extension de la mesure basée sur la borne inférieure en associant un vecteur pour chaque base de connaissances. Ce vecteur est une partition en set packing fermés maximaux de la base en question. De plus, deux mesures d'incohérences ont été
instanciées en agrégeant les valeurs de ce vecteur soit en considérant une somme pondérée ou en utilisant la fraction continue de ce vecteur. Nous avons également formulé le problème de set packing fermé et sa version pondéré en problèmes d'optimisation basés sur MaxSAT et la programmation linéaire 0/1.

### 5.2.4 Sous-additivité

Dans [Jabbour et al. 2017c], nous avons poursuivi l'exploration des mesures d'incohérences de point de vue syntaxique. Partant de l'observation que la disjonction entre MUS est un facteur accentuant la valeur de l'incohérence, nous avons proposé une nouvelle propriété appelée sous-additivité (Définition 16) qui est une contre-partie de la propriété de l'indépendance-additivité décrite précédemment.

**Définition 16** (Sous-Additivité). Si $MUSes(K \cup K') = MUSes(K) \uplus MUSes(K')$ et $unfree(K \cup K') \neq unfree(K) \uplus unfree(K')$, alors $I(K \cup K') < I(K) + I(K')$.

Afin de définir une mesure satisfaisant la propriété de la sous-additivité, nous définissons $G_{mus}^K(V, E)$ comme le graphe associé aux MUSes de K tel que $V = MUSes(K)$, et $(M, M') \in E$ ssi $M \cap M' \neq \emptyset$. De plus, nous dirons que S est une couverture en MUS (MC) de K ssi S est une couverture par sommets de $G_{mus}^K(V, E)$.

Lorsque deux MUSes partagent des formules, leur incohérence doit être définie sur des valeurs différentes pour satisfaire la propriété de sous-additivité. À cette fin, nous définissons d'abord une partition d'arêtes du graphe des MUSes de K.

**Définition 17.** Nous définissons une partition en arêtes de $G_{mus}^K$ comme

$$P_e = \bigcup_{M \in V} P_e(M) \text{ t.q. } P_e(M) \subseteq \{(M, M') \in E\}$$

La définition 17 stipule que chaque arête entre deux MUSes M et M' appartient soit à $P_e(M)$ soit à $P_e(M')$. De plus, une partition en arêtes $P_e$ peut contenir des ensembles vides et sa taille $|P_e| = |MUSes(K)|$. Et cela permet de quantifier la contribution de chaque MUS M en fonction du nombre d'arêtes de $P_e(M)$.

Maintenant, nous définissons la mesure d'incohérence d'une partition en arêtes comme suit :

**Définition 18.** Soit $P_e$ une partition en arêtes $G_{mus}^K$. Nous définissons la mesure d'incohérence de $P_e$ comme

$$Inc^f(P_e) = \sum_{M \in V} f(|P_e(M)|)$$

avec f est une fonction strictement décroissante sur $\mathbb{N}$ qui satisfait $f(0) = 1$ et bornée par un réel $0 < c < 1$.

Comme f est une fonction strictement décroissante sur la taille des éléments de la partition, cela signifie que si une arête est ajoutée à $P_e(M)$, la contribution de M à la mesure d'incohérence de $P_e$ diminue. En d'autres termes, le degré d'incohérence d'un MUS M dépend du nombre d'arêtes attribuées à $P_e(M)$. Différentes fonctions f peuvent être identifiées. Par exemple, on peut considérer $f_1(n) = 1 - c + c^{n+1}$ ou encore $f_2(n) = 1 - c + \frac{c}{n+1}$ tel que $0 < c < 1$.
En utilisant la partition $P_e$, nous avons défini le degré d'incohérence de K comme

$$ Inc(K) = \max_{P_e} Inc^f(P_e) $$

Le calcul de $Inc(K)$ dépend de la fonction $f$ utilisée. Comme on peut le voir avec l'exemple suivant, dans le cas où $f = f_1$ ou $f_2$, on obtient une fonction non-linéaire à optimiser.

**Exemple 3.** Pour l'exemple de la figure 5.1, en utilisant les fonctions $f_1$ et $f_2$, le calcul des mesures d'incohérences revient à optimiser les fonctions suivantes :

$$ Inc^{f_1}(P_e) = 5(1-c) + c^{1+x_{e_1}+x_{e_2}+x_{e_5}} + c^{1+\neg x_{e_2}+x_{e_3}} + c^{1+\neg x_{e_1}+\neg x_{e_3}} + c^{1+x_{e_4}} + c^{1+\neg x_{e_4}+\neg x_{e_5}} \quad (5.1) $$

$$ Inc^{f_2}(P_e) = 5(1-c) + \frac{1}{1+x_{e_1}+x_{e_2}+x_{e_5}} + \frac{1}{1+\neg x_{e_2}+x_{e_3}} + \frac{1}{1+\neg x_{e_1}+\neg x_{e_3}} + \frac{1}{1+x_{e_4}} + \frac{1}{1+\neg x_{e_4}+\neg x_{e_5}} \quad (5.2) $$

<figure><img src="image_13.png" /><figcaption>FIGURE 5.1 – De l’hypergraphe au graphe des MUSes de K</figcaption></figure>

Exploiter la structure des MUSes pour définir de nouvelles mesures d'incohérence a fait l'objet d'un autre travail. Dans [Jabbour & Sais 2016], nous avons considéré les ensembles indépendants de MUSes, i.e., ensemble de MUSes disjoints deux à deux. Cette structure permet de mieux capturer la structure de MUSes en termes d'intersection et offre la possibilité d'étendre plusieurs mesures d'incohérence existantes. À la lumière de cette notion, nous avons associé à chaque base de connaissances la séquence $\langle \delta_0 \dots \delta_i \dots \delta_n \rangle$ où $\delta_i$ est le nombre des sous-ensemble de MUS indépendants de taille $i$ permettant de définir la mesure $Inc(K) = \log(\delta_1 + \dots + \delta_n)$. Cette mesure vaut $Inc(K) = \sum_{i=1}^n C_n^i = \log(2^n) = n = |MUSes(K)|$ lorsque les MUSes sont disjoints deux à deux.

### 5.2.5 Dominance faible

Dans [Jabbour et al. 2014d, Jabbour et al. 2014e, Jabbour et al. 2017b], nous nous sommes intéressés à l'une des propriétés des mesures d'incohérences nommée dominance. Cette propriété stipule que le degré de conflit ne peut pas accroître si une formule est substituée par l'une de ces conséquences logiques. Cette propriété est rarement satisfaite par les différentes
mesures de l'état de l'art. Nous avons proposé dans [Jabbour et al. 2017c, Jabbour et al. 2014d, Jabbour et al. 2014d] une version moins forte de cette propriété appelée dominance faible, jugée plus intuitive que l'originale à notre avis car elle est basée sur une notion de conséquence logique plus restreinte mais rationnelle.

**Définition 19 (Dominance Faible).** Si $\alpha \nparallel \beta$ et $PI(\beta) \subseteq PI(\alpha)$, alors $I(K \cup \{\alpha\}) \ge I(K \cup \{\beta\})$.

Basée sur cette notion de conséquence logique restreinte, nous avons à la fois explorer deux questions fondamentales. De point de vue sémantique, nous avons donné une caractérisation logiques des variables conflictuelles et montrer leur utilité face aux approches existantes basées sur des sémantiques multi-valuées. Par ailleurs, nous avons introduit la notion de MUS déduit (DMUS) permettant de caractériser des MUSes construits en utilisant la conséquence logique restreinte définie précédemment. Nous avons également montré que le raisonnement avec les MUSes déduits permet de capturer plus finement les sous-ensembles insatisfiables au sein d'un ensemble de formules. Nous avons présenté également une nouvelle mesure permettant de satisfaisant la propriété de la dominance faible.

### 5.2.6 Restauration de la cohérence

Nous nous somme également intéressés dans [Jabbour & Sais 2016] à la restauration de la cohérence d'une base de connaissance incohérente, l'autre question fondamentale dans le cadre de la gestion de l'incohérence. Nous nous sommes focalisés précisément sur les méthodes basées sur la restauration de la cohérence par suppression de formules. Dans ce contexte, nous avons introduit une approche permettant de supprimer le nombre minimum de formules nécessaire pour restaurer la cohérence tout en évitant de supprimer complètement des MUSes. L'objectif est de préserver le plus possible les connaissances de la base originale. Nous avons formulé ce problème sous l'appellation de couverture minimale de MUSes définit comme suit.

**Définition 20 (Couverture Minimale de MUSes).** Le problème de Couverture Minimale de MUSes est défini comme le problème de trouver le plus petit ensemble intersectant qui couvre le nombre minimum de MUSes(K).

Intuitivement, pour un ensemble intersectant $H$, on associe l'ensemble $C_{mus}(H)$ définit par $C_{mus}(H) = \{M \in MUSes(K), M \subseteq H\}$. Cela permet de définir une relation de préférences entre les ensembles intersectants comme suit :

$$H_1 \le H_2 \text{ ssi } |C_{mus}(H_1)| \le C_{mus}(H_1) \text{ ou } |C_{mus}(H_1)| = |C_{mus}(H_2)| \text{ et } |H_1| \le |H_2|$$

Notre objectif est donc de trouver les ensembles intersectants préférés par rapport à la relation $\le$. En relaxant ou en contraignant la relation de préférence $\le$, nous avons pu définir plusieurs problèmes sous-jacents. À titre d'exemple, le problème qui consiste à trouver un ensemble intersectant ne couvrant aucun MUS (lorsque les MUSes sont préalablement calculées), est identique à SIM-UNSAT défini dans le cadre propositionnel et dont les instances sont formées de clauses totalement positives $P$ et d'autres totalement négatives obtenue à partir de $P$ en inversant chaque littéral $p$ en $\neg p$. Ce problème fait partie d'un ensemble de problèmes proposés par Thomas Eiter en 1996 [Eiter 1996] et dont la complexité est encore une question ouverte. Le problème de
décision associé à notre approche généralise celui de SIM-UNSAT. Dans [Jabbour 2016], nous avons étudié plusieurs variantes de notre nouveau problème. Nous avons également formulé des encodages en MaxSAT de ce problème de couverture minimale et ses variantes.

**5.3 Théorie de l'argumentation**

Il est parfois difficile d'assurer la cohérence d'une base de connaissances. Il faut alors être capable de raisonner en présence de contradictions. Une classe d'approches de raisonnement en présence d'informations incertaines et incohérentes est récemment proposée, dite théorie de l'argumentation [Dung 1995]. L'argumentation est un modèle attrayant pour raisonner avec des connaissances imparfaites ou conflictuelles; elle est essentiellement fondée sur la justification d'une conclusion plausible par des raisons en faveur de celle-ci. Depuis quelques années, l'argumentation formelle est devenue un thème de recherche très populaire et elle a un large éventail d'applications pour plusieurs domaines comme le juridique, le médical, la prise de décision, la négociation entre agents, etc. Elle est aussi étudiée dans diverses disciplines comme la psychologie, la philosophie et la linguistique.

Nous présentons dans cette section nos approches autour du raisonnement à base d'argumentation.

**5.3.1 Enumération des extensions Top-k**

Le cadre d'argumentation abstrait initié par Dung dans [Dung 1995] représente simplement un système d'argumentation par un graphe où les sommets sont les arguments et les arcs les attaques entre ces arguments. Ensuite le problème est de définir les arguments qui peuvent être conjointement acceptés, c'est le rôle des différentes sémantiques proposées.

Ce cadre argumentatif abstrait a récemment reçu un intérêt considérable. Malgré leur simpli-
cité, ce cadre fournit un outil puissant qui capte différentes approches de raisonnement nonmono-
tone. Malheureusement, dans ces systèmes, la plupart des tâches de raisonnement souffrent d'une
complexité très élevée. En particulier, l'énumération de toutes les extensions<fnref n="1" /> est généralement
un problème intraitable, puisque le nombre d'extensions peut être exponentiel dans le pire des cas.
Ainsi, la réduction de la taille de la sortie dans le cadre d'argumentation abstrait est clairement
une question de recherche très importante.

Dans [Jabbour et al. 2016d], nous nous sommes intéressés au problème qui consiste à sélec-
tionner les "meilleures" extensions d'un sytsème d'argumentation abstrait. Cette sélection se fait
par agrégation afin d'optimiser la recherche et de manipuler moins de quantités de données. Plus
précisément, vue que l'espace des alternatives considérées est de grande taille à cause de sa struc-
ture combinatoire, il est illusoire de vouloir représenter et de maintenir des préférences données
sous forme explicite. Pour se faire, nous avons exploité les préférences au niveau de la sémantique
de choix des extensions afin de réduire la taille de sortie. Contrairement aux approches existantes
qui consistent à injecter les préférences au niveau atomique (sur les arguments), nous avons dé-
fini des relations de préférence sur des ensembles d'arguments. Ensuite, nous avons présenté un

<footnote n="1">1. Une extension est un ensemble d'arguments acceptables. Dans le système de Dung [Dung 1995], plusieurs sémantiques sont données à l'acceptabilité des arguments.</footnote>
algorithme de calcul des extensions Top-k en se basant sur une relation de préférence spécifiée par l'utilisateur. En effet, une extension est dite Top-k sous une sémantique donnée si elle admet moins de k extensions préférées à celle-ci par rapport à une relation de préférence donnée. Différentes notions de préférence ont été introduites conduisant à différentes politiques de choix des extensions. Finalement, une étude expérimentale sur divers benchmarks a démontré l'efficacité de l'approche proposée.

## 5.3.2 Raisonnement sur des ontologies conflictuelles

Dans le cadre de nos travaux sur l'argumentation dans un cadre de logique, nous avons étudié le problème de raisonnement sur des ontologies en présence de conflit [Bouzeghoub et al. 2017]. En effet, le web sémantique constitue un environnement dans lequel les agents humains et machines vont communiquer selon une base sémantique. Il utilise la notion d'ontologies pour la conceptualisation et l'extraction des connaissances du domaine et les stocke en termes de concepts et de propriétés dans la machine d'une manière compréhensible et traitable. En raison de leurs capacités de décidabilité et d'expressivité, les ontologies ont joué un rôle fondamental pour décrire la sémantique des données non seulement dans le web sémantique émergents, mais aussi dans l'in-génierie des connaissances traditionnelles et les systèmes de traitement de l'information. Néan-mois, l'augmentation du nombre d'ontologies développées et maintenues sur le web, génère inévitablement des incohérences. Dans ce contexte, nous avons étendu la théorie de l'argumenta-tion déductive de Besnard & Hunter dans le contexte de la logique SHIOQ [Baader et al. 2010], un fragment expressif de la logique de description. Différentes notions de conflit ont été étudiées, à savoir l'incohérence qui signifie qu'une des classes de l'ontologie est nécessairement vide d'in-dividu et l'inconsistance qui implique l'absence d'un modèle. Cela nous a permis, contrairement aux approches existantes, la détection automatique et la localisation des incohérences séman-tiques. Nous avons également étendu notre approche argumentative au cadre des ontologies in-certaines afin de prendre en compte l'aspect incertain des données disponibles et d'analyser les réponses aux requêtes en se basant sur des logiques de description possibilistes. Dans ce contexte, nous avons exploré les différentes manières d'utiliser les poids sur les arguments pour définir des nouvelles relations d'inférence, ce qui permet de prendre en compte l'incertitude tout au long du processus d'inférence. Nous avons en particulier montré que plusieurs relations d'inférences de l'état de l'art peuvent être capturées via notre cadre d'argumentation possibiliste.
# Composition de services web

## 6.1 Introduction

Les évolutions impressionnantes du monde de l'informatique et de l'internet ont entrainé le développement de nouveaux paradigmes d'interaction entre applications. Notamment, l'architecture orientée service (Service Oriented Architecture, ou SOA) qui a été mise en avant afin de permettre des interactions entre applications distantes. Cette architecture est construite autour de la notion de service, qui est matérialisé par un composant logiciel assurant une fonctionnalité particulière et accessible via son interface. Un service est toujours accompagné d'une description fournissant aux applications les informations nécessaires à son utilisation. Cette évolution liée aux technologies internet et web est un facteur important dans la création et l'explosion de l'informatique dans les nuages ou *Cloud Computing*. Ce dernier fournit un ensemble de ressources informatiques partagées telles que les applications, le stockage, le calcul, la mise en réseau et le développement. Cette technologie vise à permettre l'accès à de larges ressources de calcul de manière totalement virtualisée, en les regroupant et en offrant une vue système unique. La diffusion rapide des services web et des services orientés systèmes constitue un pas important vers un changement radical dans le processus de développement logiciel.

Les services web constituent un bon paradigme pour concevoir et créer des applications complexes. Ce paradigme est utilisé par l'informatique dans les nuages, plus précisément par le SaaS, en tant qu'élément principal avec des descriptions d'interface bien définies. Ces services web sont définis comme un ensemble d'opérations abstraites et de messages qui doivent souvent être combinés pour former un service complexe à l'aide du mécanismes de composition.

La composition dynamique des services Web exige que les consommateurs de services découvrent des fournisseurs de services répondant à des exigences fonctionnelles et non fonctionnelles données, notamment des exigences de coût et de qualité de service, telles que la performance et la disponibilité. Les attributs de qualité de service d'un service web incluent des mesures telles que le temps de réponse, le débit, la sécurité et la disponibilité faisant référence à ce qu'on appelle la *qualité de services*.

Au fil des années, le nombre de services web avec des fonctionnalités similaires et une qualité de service irrégulière a considérablement augmenté. La sélection des services web devient compliquée, ce qui rend nécessaire de garantir une composition avec une meilleure qualité de service bien que cette tâche est difficile (problème NP-hard).

Le problème de composition de services web consiste à trouver automatiquement une séquence optimale (ou de meilleure qualité) de services web satisfaisant la requête de l'utilisateur. La littérature est riche d'approches de composition de services web [Nacer et al. 2015, Shiaa et al. 2008, Rodriguez-Mier et al. 2011, Okutan & Cicekli 2010, Wu & Khoury 2012, Balbiani et al. 2010].
Dans la suite nous donnes une description des méthodes à base de contraintes proposées dans
le cadre de la composition de services web.

## 6.2 Définitions et cadre formel

Les applications en tant que service sont construites à partir d'un ensemble de services web accessibles via internet. Un fournisseur différent peut proposer un ensemble de services Web avec les mêmes fonctionnalités. Un service web est une technologie qui permet aux applications de communiquer à distance via Internet, et cela indépendamment des plates-formes et des langues sur lesquelles ils s'appuient. Pour cela, les services web s'appuient sur un ensemble de protocoles internet largement utilisés, tels que XML, HTTP, pour communiquer.

Un service web est considéré comme un composant logiciel avec ses paramètres d'entrée *I* et ses paramètres de sortie *O*.

**Définition 21.** Un service web est un triplet $w = (I, O, Q)$ tel que :

- *I* : est un ensemble de paramètres d'entrée,

- *O* : est un ensemble de paramètres de sortie,

- *Q* : représente la qualité de service associée à *w*.

Lorsque c'est utile, pour un service web $w = (I, O, Q)$, nous notons $I(w) = I$, $O(w) = O$, et $Q(w) = Q$. De plus, nous omettons de mentionner la qualité de service $w = (I, O)$ lorsqu'elle n'est pas requise.

Pour décider de la relation d'invocation de $w_1 = (I_1, O_1)$ à $w_2 = (I_2, O_2)$ dans la composition, il est nécessaire de comparer sémantiquement les sorties $O_1$ de $w_1$ avec les entrées $I_2$ de $w_2$. Pour cela, nous devons calculer une similarité sémantique entre deux paramètres ; c'est-à-dire qu'il faut trouver une relation entre deux représentations de connaissances. Une fonction de jonction décrit la correspondance sémantique entre deux paramètres et formulée comme suit.

**Définition 22 (Fonction de Jonction).** Étant donné deux services Web $w_1 = (I_1, O_1, Q_1)$

et $w_2 = (I_2, O_2, Q_2)$, une fonction de jonction renvoie true

si $i.type = o.type$ tel que $i \in I_2$ et $o \in O_1$,

ou $i.type$ est un sous-type de $o.type$.

Étant donné un ensemble *W* de services web disponibles et une requête $w_r = (I_r, O_r)$, le problème de composition de services web consiste à trouver un service web $w = (I, O) \in W$ tel que $I_r \subseteq I$ et $O_r \in O$. Cependant, souvent, il n'existe pas de service web unique répondant aux exigences de la requête. Dans ce cas, le but est de trouver un ensemble de services web à combiner pour satisfaire la requête.

Nous avons proposé des transformations vers la logique propositionnelle afin de trouver une
composition de services web optimale maximisant la qualité de service QoS. Deux approches ont
été proposées.
## 6.3 Composition de services web à base d'ensembles minimaux incohérents

Dans [Wakrime & Jabbour 2015], nous avons montré que la recherche d'une composition optimale est équivalente à la recherche du plus petit MUS. Pour une telle modélisation, nous avons associé à chaque paramètre d'entre $i_k$ (resp. de sortie $o_k$) une variable propositionnelle $p_{i_k}$ (resp. $q_{o_k}$). Pour chaque service web $w$ une variable propositionnelle $r_w$ est également associée. La jonction est exprimée par l'égalité entre un paramètre d'entrée $i_k$ et un paramètre de sortie $i_{k'}$ par $p_{i_k} = q_{o_k'}$ lorsque cette dernière est possible.

L'encodage est obtenu en considérant la contrainte de l'équation (6.1). Pour chaque service web $w$, cette contrainte stipule que si les paramètres d'entrée de $w$ sont actifs, alors le service web est actif pour composition ; et par conséquent le service pourrait être utilisé dans la composition. De plus, si le service web $w$ est actif alors ces paramètres de sortie le sont également.

$$ \bigwedge_{(\langle i_1 \dots i_k \rangle, \langle o_1 \dots o_{k'} \rangle) \in W} (p_{i_1} \wedge \dots \wedge p_{i_k} \rightarrow r_w) \wedge (r_w \rightarrow q_{o_1} \wedge \dots \wedge q_{o_{k'}}) \quad (6.1) $$

Notons que pour une requête utilisateur de la forme $w_r = (\langle i_1 \dots i_n \rangle, \langle o_1 \dots , o_m \rangle)$, une composition est possible si la formule $\Phi_w = (6.1) \wedge p_{i_1} \wedge \dots \wedge p_{i_n} \wedge \neg q_{o_1} \wedge \dots \wedge \neg q_{o_m}$ est insatisfiable par propagation unitaire $(\Phi_w \vdash_* \perp)$. De plus, trouver la composition optimale est équivalent à trouver un MUS de la plus petite taille possible contenant $p_{i_1} \wedge \dots \wedge p_{i_n} \wedge \neg q_{o_1} \wedge \dots \wedge \neg q_{o_m}$ et contenant le nombre minimum de services web $W$. Dès lors, les techniques de recherche du MUS de taille minimum peuvent être utilisées directement pour trouver une composition optimale. Nous avons proposé également une extension de cette approche pour prendre en compte la qualité de service (QoS).

## 6.4 Composition de services web à base d'impliquants premiers

Dans [Wakrime & Jabbour 2017], nous avons proposé une autre approche *bottom-up* pour trouver une composition de services web optimale. L'encodage est composé des deux contraintes suivantes :

$$ r_w \rightarrow \bigwedge_{i \in I \setminus I_r} \bigvee_{w' \mid i \in O(w')} r_{w'} \quad \text{pour tout } w = (I, O) \in W \quad (6.2) $$

$$ \bigvee_{w \mid o \in O(w)} r_w \quad \text{pour tout } o \in O_r \quad (6.3) $$

La contrainte (6.2) est obtenue en fusionant deux contraintes. La première stipule qu'un service web est actif à la composition si tous ces paramètres d'entrée le sont aussi, i.e., $r_w \rightarrow \bigwedge_{i_k \in I(w)} p_{i_k}$. La seconde indique qu'un paramètre d'entrée $i_k$ est actif s'il fait partie de l'entrée de la requête de l'utilisateur $i \in X$ ou s'il est également le paramètre de sortie d'au moins un service web actif, i.e., $p_{i_k} \rightarrow \bigvee_{w' \mid i \in O(w')} r_{w'}$. La seconde contrainte (6.3) traduit le fait que les paramètres de sorties de la requête doivent être actifs. Cela est facilement exprimé par le fait que chacun de ces paramètres doit être la sortie d'au moins un service web qui est lui même actif.
Contrairement à l'approche [Wakrime & Jabbour 2015], l'avantage de ce nouvel encodage est qu'il est restreint aux variables booléennes représentant les services web. Ensuite la formule obtenue est reverse-horn. Par conséquent, l'existence d'une composition est équivalente à la satisfiabilité de la formule reverse-horn qui peut être vérifié en temps linéaire. Nous avons prouvé que les impliquants premiers correspondent aux compositions minimales et ceux de la plus petite taille correspondent exactement aux compositions optimales en nombre de services web.

La formulation générale du problème de la composition de services web avec la QoS (à minimiser) lorsque cette dernière est additive, peut être formulée via le problème bien connue de MinSAT de la manière suivante :

$$ \min \sum_{w \in W} Q(w)w_r \quad \text{subject to (6.2) } \land (6.3) $$

Par ailleurs dans [Wakrime et al. 2015], nous avons traité le cas des requêtes qui n'aboutissent pas. Nous avons proposé un cadre à base de contraintes pour trouver le minimum de changement par ajout de paramètres d'entrée afin de rendre la réponse à la requête possible. L'objectif étant d'offrir à l'utilisateur une alternative à sa requête qui pourrait éventuellement répondre à ses exigences.
Durant ces dix dernières années, nous avons exploré diverses thématiques de recherche. Certaines en adéquation avec les axes de recherche du CRIL, d'autres constituent des thématiques d'ouverture comme la fouille de données, l'apprentissage et la composition de services web. Nous avons mis en lumière de multiples connexions qui nous ont permis d'opérer de riches fertilisations croisées. Nous avons essayé de répondre à plusieurs questions liées à la résolution effective des problèmes de décision, au raisonnement en présence d'incohérence et à l'efficacité des approches logiques pour la fouille de motifs ensemblistes et séquentiels. Par exemple, nous avons défini un cadre logique pour calculer les Top-k motifs via la définition d'un nouveau problème, appelé Top-k SAT, un concept nouveau en logique propositionnelle. Nous avons étendu le concept de symétries largement exploré en SAT/CP vers la fouille de motifs ensemblistes et proposé des approches logiques pour la fouille des motifs ensemblistes et séquentiels. Certaines contraintes, comme la contrainte de cardinalité et sa variante conditionnelle, récurrentes dans ces transformations, ont fait l'objet d'une étude spécifique ayant conduit à de nouveaux encodages efficaces. Nos contributions à l'amélioration de résolution pratique du problème SAT sont essentielles et touchent à différents aspects, allant de l'amélioration de l'apprentissage des clauses, à la définition de nouvelles mesures de qualité des clauses apprises en passant par la mise en œuvre de stratégies de recherche plus efficaces (e.g., redémarrages dynamiques). Notre approche parallèle de type portfolio a poussé encore plus loin les limites des solveurs SAT modernes. Nos propositions d'amélioration de l'échange de clauses et du contrôle de leurs qualités a été mise à profit dans ce cadre et dans le cas distribué.

Nos contributions au raisonnement en présence d'incohérence ont fait émerger d'autres questions intermédiaires aussi complexes mais autant importantes comme l'extension des problèmes bien connus de "Set Packing" et "SIM-UNSAT", en respectivement "Set Packing Fermé" et "SIM-UNSAT Généralisé" que nous avons étudié et analysé du point de vue de la complexité.

Parmi les autres problématiques en vogue à l'heure actuelle et que nous avons abordé, on peut citer celle liée à la taille des données de plus en plus volumineuses. Nous avons proposé plusieurs techniques pour différentes représentations. D'un côté, nous avons introduit un cadre pour compacter les problèmes de contraintes (ensemble de clauses (SAT) et contraintes tables ou en extension (CP)) en utilisant la fouille de données. Pour les graphes, nous avons défini une approche de compression basée sur les contraintes pseudo-booléennes. Nous avons également proposé des approches symboliques pour la détection de communautés dans les grands graphes de données. Finalement, nous avons utilisé des techniques de décomposition et l'approche parallèle étudiée en logique pour améliorer sensiblement l'efficacité des approches déclaratives de fouille de motifs ensemblistes sur des données de grandes tailles.

Sur les aspects liés à la modélisation de problèmes, nous avons montré que la composition de services web peut être encodée en logique propositionnelle, tout en proposant des approches pour
une composition optimale qui prend en compte la qualité des services web.

Pour résumer ce bilan, nous citons certains de nos travaux que nous pouvons modestement qualifier de précurseur (ou parmi les premiers) dans le domaine. Il s'agit de nos contributions autours de(s) :

1. approches de type portfolio pour la résolution parallèle du problème SAT,

2. restarts dynamiques,

3. l'apprentissage de clauses à partir des succès,

4. la fouille de séquences par des approches contraintes,

5. l'utilisation des symétries en QBF,

6. la détection et l'élimination des symétries en fouille de données,

7. l'utilisation de la fouille de données pour extraire des motifs pour la compression de formules booléennes et de réseaux de contraintes,

8. la représentation des graphes par une disjonction de contraintes pseudo-booléennes,

9. le clustering de données complexes représentées par des formules logiques,

10. approches logiques pour la détection de communautés.

Nos travaux antérieurs ouvrent de nombreuses perspectives qui méritent d'être explorées. J'ai fait le choix de limiter ma présentation autours de trois grandes directions de recherche :

**Fouille de données & Contraintes** : Encouragé par les récents développements, notre projet a pour cadre la fouille de données par contraintes. Il s'articulera autour de deux problématiques de recherche :

1. Extraction de motifs sous contraintes : Il s'agit de poser un cadre plus flexible et générique pour prendre en compte les contraintes, les préférences et les critères d'intérêts que l'utilisateur souhaite optimiser. Cette étude ne se limitera pas aux données transactionnelles, nous proposons d'élargir le cadre de cette étude à d'autres types de données comme les séquences et les graphes attribués. Pour l'extraction de connaissances à partir des bases de données transactionnelles, nous avons initié l'étude de deux problématiques avec un potentiel applicatif plus large. Il s'agit de la découverte de motifs profitables (générant un profit élevé), appelé « high utility itemset mining », une problématique ayant émergée récemment. Ce problème vient répondre à une limitation importante du cadre classique, qui considère que les items ont la même importance. Or dans de nombreuses applications, les items peuvent être différenciés par plusieurs attributs associés comme la quantité, le prix ou plus généralement l'utilité. Dans ce cadre, les motifs ne sont ni monotones ni anti-monotones rendant le problème d'énumération plus difficile. Or les approches déclaratives à base de contraintes peuvent être très utiles dans ce cadre, car elles disposent de mécanismes d'élagages de l'espace de recherche plus spécifique. Le second problème concerne la découverte de motifs graduels à partir de bases de données numériques, permettant de capturer des relations entre attributs en termes de variations. Ce problème trouve de très nombreuses applications dans divers domaines incluant les données médicales, biologiques ou statistiques.
2. Fouille qualitative de données : l'objectif est de proposer de nouvelles caractérisations des motifs à extraire en intégrant des notions de pertinences plus fortes comme la robustesse et la stabilité. Ceci nous permettra de réduire significativement la taille de la sortie en se focalisant sur les motifs les plus pertinents. Certains types de modèles robustes définis dans le cadre de la logique peuvent trouver ici une possible extension en fouille de données. Nous intégrerons également diverses propriétés structurelles comme les symétries pour réduire la taille de l'espace de recherche des algorithmes d'énumération.

3. Analyse logique des données : L'analyse logique des données (LAD) est une méthodologie principalement basée sur la notion de motif. Considérant une base de données constituée de deux groupes d'observations booléennes (appelées observations positives et négatives), la méthode LAD consiste à trouver un sous-ensemble d'attributs ayant les mêmes valeurs sur certaines observations de l'ensemble positif alors que ces valeurs ne peuvent pas être observées dans le groupe négatif. Ce sous-ensemble s'appelle un motif et le but est de trouver des motifs partagés par autant d'observations positives que possible. Cette approche proposée il y'a plus de 20 ans par Peter L. Hammer, est essentiellement connue dans la communauté des mathématiques discrètes par ces liens aux travaux autours sur les fonctions booléennes partiellement définies. Elle reste largement ignorée par la communauté fouille de données. Les nombreuses formulations connues sont basées sur des modélisations sous forme de programmes lineaires 0/1 avec un nombre quadratique de contraintes linéaires. La première piste serait de réduire cette complexité en espace pour un réel passage à l'échèle. Nous envisageons également d'élargir le champ d'application de la LAD au domaine du test logiciel.

4. Fouille de données symbolique : Aujourd'hui les données peuvent être plus complexes, de nature hétérogènes, contextuelles et multi-sources. Elles peuvent représenter par exemple les désirs ou préférences des clients collectés de différentes manières. Extraire des connaissances à partir de ces données complexes passe par une étape de pré-traitement qui consiste à trouver la représentation la plus appropriée. La logique peut constituer un formalisme de choix pour décrire ces données ou entités complexes. Il s'agit ensuite de mettre en œuvre des nouvelles approches d'extraction de connaissances adaptées à de telles représentations. Notre premier travail autour du clustering symbolique est un pas dans cette direction.

5. Détection de communautés : Dans ce cadre, nous souhaitons élargir nos travaux à la détection de communautés dans les graphes orientés et attribués. Il s'agit de tenir compte des informations (attributs, flux) étiquetant les liens ou les arcs. La non prise en compte de ces informations est une réelle simplification de la notion de communauté qui est caractérisée non pas par les liens mais aussi par les informations attachées aux sommets et aux arêtes.

**Fertilisation croisée entre la fouille de données et l'IA** : Nous avons montré que les domaines de l'IA et de la fouille de données peuvent tirer un réel bénéfice d'une fertilisation croisée. Dans ce cadre, nous souhaitons approfondir cette voie de recherche fructueuse dans plusieurs directions. La première consiste à étudier les possibilités d'intégration de divers paradigmes de l'IA comme par exemple le raisonnement sur les connaissances extraites (post-traitement), l'intégration des symétries dans diverses tâches de fouille de données, le pré-traitement des données par
des approches issues de la compilation des bases de connaissances et la prise en compte des préférences dans le processus de fouille de données. Divers types de solutions en logique peuvent être étendu pour définir des motifs plus robustes. Il s'agit aussi de voir dans quelle mesure la fouille de données (extraction de motifs, clustering, détection de communautés) peut être utile pour analyser et extraire diverses formes de structures dans les formules SAT, dans les réseaux de contraintes CSP et dans les graphes, pour compressor et améliorer la résolution de problèmes dans ces formalismes.

**Extraction, analyse et visualisation de motifs complexes à partir des données issues de processus migratoires** : Dans le cadre du projet CNRS Mastodons QDoSSI<fnref n="1" />, une collaboration est en cours avec des chercheurs en sciences humaines et sociales (SHS) autours de l'analyse et de la compréhension des processus à l'œuvre dans la construction des parcours migratoires. Notre domaine d'analyse se concentre sur des données structurées (e.g., biographie migratoires) et non structurés (e.g., récits de vie) collectées par les laboratoires SHS sur des terrains différents (e.g., Afrique subsaharienne, et moyen orient) et portent sur des populations diverses (e.g., migrants, réfugiées, etc.).

Ce projet multidisciplinaire ouvre la voie au développement de nouvelles techniques en rupture avec l'existant dans le domaine des bases de données et de l'extraction des connaissances :

- Qualité des données et pré-traitement : les données mobilisées sont hétérogènes avec des temporalités et des représentativités variables. Elles présentent diverses imperfections, comme la présence de données manquantes, de données mal orthographiées ou encore de données entachées d'incertitudes et d'imprécisions. Ceci pose le problème de la mesure, de l'intégration et de l'évaluation de l'impact de la qualité des données sur les résultats d'analyses dans un contexte spatio-temporel évolutif.

- Extraction de motifs complexes à partir de données complexes : notamment, l'extrac-
tion des connaissances complexes (ici les parcours/graphes) à partir de données textuelles
et/ou relationnelles. Les graphes extraits, et enrichis sémantiquement, ouvrent la voie à
de nouveaux champs d'extraction de connaissances, d'analyses et d'interrogations de ces
structures combinatoires.

— Visualisation de graphes attribués : les graphes attribués associés aux parcours migratoires sont complexes et renseignent sur les lieux et les étapes parcourues par les migrants. L'objectif est de proposer des techniques de visualisations de graphes capable de mettre en valeur la richesse et la diversité des informations associées aux sommets et aux arêtes. Cette visualisation doit être dynamique et interactive. Il s'agit également de projeter ce graphe sur une carte géographique.

<footnote n="1">1. Qualité des données multi-Sources : un double défi pour les sciences sociales et les sciences de l'Informatique – url : http://www.cril.univ-artois.fr/qdossi/</footnote>
— Titulaire de la PEDR depuis octobre 2013.

— Délégation CNRS, CRIL CNRS UMR 8188, 2017, 6 mois.

## 8.1 Valorisation scientifique

### 8.1.1 Distinctions

— Prix du meilleur papier (Best Student Paper Awards), Imen Ouled Dlala, Saïd Jabbour, Lakhdar Saïs, Yakoub Salhi, and Bouteina Ben Yaghlane, Parallel SAT Based Closed Frequent Itemsets Enumeration, (AICCSA'2015), Marrakech, Maroc.

— Nomination pour le prix du meilleur papier (Best Student Paper Runner-Up), Saïd Jabbour et Badran Raddaoui, Measuring Inconsistency Through Minimal Proofs, Twelve European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU), 2013, (89 soumissions – 44 papiers acceptés – 4 papiers nominés)

— Prix du meilleur article de la conférence (Best Paper Awards), Youssef Hamadi, Saïd Jabbour, Lakhdar Saïs, "Learning for Dynamic Subsumption", 21st IEEE International Conference on Tools with Artificial Intelligence (ICTAI), Newark, New Jersey, USA, 2-4 November 2009

### 8.1.2 Logiciels

— Solveurs SAT

**X-MiniSAT** (2014)<fnref n="1" /> : solveur SAT de type CDCL basé sur nos derniers résultats sur les stratégies d'élimination de clauses apprises. Sur la instances de la dernière compétition internationale SAT 2013, X-MiniSAT obtient des résultats significativement meilleurs (sur les instances de la catégorie Application) que les vainqueurs de cette compétition. X-MiniSAT peut être considéré comme un solveur état-de-l'art.

**ManySAT**<fnref n="2" /> : un solveur SAT de type CDCL incluant toutes les fonctionnalités des solveurs SAT modernes (analyse de conflits, heuristique basée sur les activités, etc.) et celles issues de nos résultats sur SAT et sur la résolution parallèle de SAT.

**Transferts** : ManySAT est utilisé en

— **Cryptography** : Macquarie University, Australia

<footnote n="1">1. http://www.cril.univ-artois.fr/ Saïs/X-SAT/X-MiniSAT.html</footnote>

<footnote n="2">2. http://www.msr-inria.inria.fr/ jabbour/manysat.htm</footnote>
— Parity games : University of Munich

— Bounded Model Checking : IBM Germany Research & Development GmbH in Boeblingen

— Software Verification : ManySAT adapté et intégré dans Microsoft Z3 SMT solver, Microsoft Redmonds, USA

**Distinctions** : (Résultats des différentes éditions de la compétition internationale et de la SAT race : http://www.satcompetition.org/)

— Meilleur solveur SAT parallèle (médaille d'or) à la SAT Race 2008 (track parallèle), Guangzhou, Chine, 2008

— Jury special prize (1st rank) Compétition SAT 2009, Swansea, United Kingdom, 2009

— Médaille d'argent et de bronze à la SAT Race 2010, Edinburgh, Scotland, UK, 2010.

**LySAT**<fnref n="3" /> : solveur SAT de type CDCL incluant toute les fonctionnalités des solveurs SAT modernes (analyse de conflits, heuristique basée sur les activités, etc.) et celles issues de nos résultats récents sur l'amélioration des techniques d'analyse de conflits, subsumption dynamique, restarts dynamique, etc.

**Distinction** : 2 médailles de bronze à la compétition SAT 2009 (track séquentiel)<fnref n="4" />

— **Outils de Fouille de Données** <fnref n="5" />

**Sym4IM** : Détection et élimination des symétries dans les problèmes de fouille d'itemsets.

**paraSATMiner** : solveur parallèle pour l'extraction des itemsets fréquents fermée.

**SatMax** : solveur pour l'extraction des itemsets fréquents maximaux.

**Sat4Seq** : librairie pour la recherche de motifs intéressants en utilisant la programmation par contraintes et SAT.

**MineToCompress** : outil utilisant la fouille d'itemsets pour compressor des formules CNF en utilisant le principe d'extension de Tseitin.

### 8.1.3 Distinctions : compétitions de solveurs

— ManySAT 1.1 et 1.5 : Médaille d'argent et médaille de bronze à la SAT Race 2010, Edinburgh, Scotland, UK, 2010 (Track parallèle)

— LySAT : 2 médailles de bronze, Competition internationale SAT2009, Swansea, Wales, UK, 2009 (Track séquentiel)

— ManySAT : prix du meilleur solveur SAT parallèle (prix spécial du jury), Competition internationale SAT2009, Swensee, UK, 2009 (Track parallèle)

— ManySAT : prix du meilleur solveur SAT parallèle (Médaille d'or), SAT Race 2008, Guangzhou, China, 2008

### 8.1.4 Brevets

— "Controlled constraint sharing in parallel problem solvers" <fnref n="6" />, en collaboration avec Microsoft Research, Cambridge, UK.

<footnote n="3">3. http://www.msr-inria.inria.fr/jabbour/ (executable disponible)</footnote>

<footnote n="4">4. http://www.cs.swan.ac.uk/csoliver/SAT2009/</footnote>

<footnote n="5">5. http://www.cril.univ-artois.fr/decMining/</footnote>

<footnote n="6">6. https://patents.google.com/patent/US8346704</footnote>
8.1.5 Collaboration industriels (passées et en cours)

— Microsoft Research Cambridge (UK)

La collaboration entre le CRIL et Microsoft a donnée lieu à de nombreux résultats de recherche incluant la mise en oeuvre du premier solveur SAT parallèle de type portfolio ManySAT ayant dominé les compétitions internationales de 2008 à 2010. Le solveur ManySAT est intégré dans Z3, le solveur SMT de Microsoft Research Redmonds. Ce résultat a par exemple fait la une du site Microsoft Research News & Highlights 7. Il est à noter que de nombreux solveurs parallèles de type portfolio ont été ensuite mis en oeuvre.

Bourse de thèse : Financement : Microsoft Research Cambridge, UK. Durée : 3 ans (septembre 2009 - septembre 2012). Budget : 100K Euros. Thèse soutenue à l'Université d'Artois par Long Guo (Co-encadrée avec Lakhdar Saïs)

— Membre **Projet PAJERO** soutenu par le programme, "Innovation Stratégique Industrielle" d'OSEO, (2011-2015).

Ce projet comprend 3 laboratoires (PRISM (Versailles), I3S (NICE) et CRIL (Lens)) ainsi que 3 entreprises (HSW, ICAPS et EquiTime). L'objectif consiste à développer une plateforme logicielle permettant, la gestion complexe de ressources multiples (ressources humaines, planification, gestion des temps et activités associées).

— RATP - ING/STF/QS/AQL - Paris : Département Ingénierie, Unité Systèmes du Transport Ferroviaire, Entité Qualification des Systèmes, Atelier de Qualification des Logiciels. Une collaboration est actuellement en cours avec la RATP (Paris), autour des outils de modél checking. Le but du projet est d'intégrer nos solveurs SAT dans l'atelier de preuve de la RATP.

**Objectifs** : Preuve formelle pour l'évaluation des systèmes de sécurité ferroviaire et notamment leur partie logicielle. La preuve formelle permet d'explorer l'exhaustivité des comportements d'un système et, ainsi, d'améliorer significativement le niveau de confiance dans la sécurité. Participants RATP : David Bonvoisin, Responsable de l'Atelier de Qualification Logicielle du département ING et Nazim Benaissa, Responsable d'études en sécurité ferroviaire au sein du laboratoire AQL.

Participants CRIL : Yakoub Salhi, Jean-François Condotta, Saïd Jabbour et Lakhdar Saïs.
Durée : 2 ans, 2015 - 2017. Budget : 150K Euros (Hors Taxes)

8.1.6 Projets de recherche nationaux

— Membre au niveau CRIL, du projet Mastodons - CNRS, QDoSSI : Qualité des données multi-Sources : un double défi pour les sciences sociales et les sciences de l'Informatique, janvier 2016 - décembre 2018.

— Membre au niveau CRIL, du projet ANR programme Défis DAG : Approche déclarative pour énumérer des motifs intéressants, janvier 2010 - décembre 2013.

<footnote n="7">7. http://research.microsoft.com/news/featurestories/publish/ManySAT.aspx?0hp=n1</footnote>
— Co-Responsable du projet Bonus Qualité Recherche (BQR), "Vers un calcul efficace des mesures d'incohérence" CRIL, Université d'Artois, 2014-2015.

— Co-Responsable du projet Bonus Qualité Recherche (BQR), "Raisonnement efficace en logique modale", CRIL, Université d'Artois, 2011-2013.

## 8.2 Encadrement de la recherche et animation scientifique

### 8.2.1 Activités d'encadrement

#### Sommaire

— Co-Encadrement de 4 thèses soutenues

— Co-encadrement de 4 thèses en cours dont 3 en Co-Tutelle

— Encadrement de 8 Masters recherche

— Co-Encadrement d'un postdoctorant (Yakoub Salhi) dans le cadre du projet ANR DAG, 01 octobre 2011 au 31 septembre 2012

— Co-Encadrement d'un postdoctorant (Mehdi Khiarri) dans le cadre du projet ANR DAG, 01 septembre 2012 au 31 juillet 2013

— Co-Encadrement d'un postdoctorant (Florian Legendre) dans le cadre du projet ANR TUPLES, 01 octobre 2014 au 30 avril 2015

#### Co-Encadrement (en cours)

1. Ikram Nakkache MANA, depuis Janvier 2018. *Approches déclaratives pour la fouille de motifs séquentiels* (Co-Tutelle avec l'Algérie)

2. Fatima Zahra MANA, depuis Janvier 2017. *Les systèmes de reconnaissances basées sur la fusion de données multi-biométriques* (Co-Tutelle le Maroc)

3. Nizar MHADHBI, depuis octobre 2015. *Fouilles de graphes et applications aux réseaux sociaux* (Bourse du gouvernement tunisien). (Soutenance fixée : décembre 2018)

4. Imen OULED DLALA, depuis septembre 2015. *Enumeration de motifs dans les données in-certaines*. (Co-Tutelle avec la Tunisie) (Soutenance 12 décembre 2018)

#### Thèses soutenues

1. Abdelhamid BOUDANE, septembre 2015 - août 2018. *Fouilles de données par Contraintes* (Bourse du gouvernement d'Algérie). *Soutenance : septembre 2018*.

2. Jerry LONLAC, septembre 2010 - octobre 2014. *Contribution à la résolution du problème de la Satisfiabilité Propositionnelle (SAT)* (financée par le MAE). *Soutenance : octobre 2014*

3. Benoît HÖESSEN, septembre 2011 - octobre 2011. *Solving the Boolean Satisfiability problem* using the parallel paradigm (financée par le Projet Pajero). *Soutenance : octobre 2014*

4. Long Guo, septembre 2009 - Juillet 2013. *Résolution séquentielle et parallèle du problème de la satisfiabilité propositionnelle* (financement par Microsoft research Cambridge (UK)). *Soutenance : décembre 2013*

#### Master recherche