Cours Logique et Calculabilité

L3 Informatique 2013/2014

Texte par Séverine Fratani, avec addenda par Luigi Santocanale

Version du 28 janvier 2014
2
Table des matières

1 Introduction 5
1.1 Pourquoi la logique ? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.1.1 La formalisation du langage . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.1.2 La formalisation du raisonnement . . . . . . . . . . . . . . . . . . . . . . . . 5
1.2 Logique et informatique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.3 Contenu du cours . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2 Calcul propositionnel 7
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.2 Syntaxe du calcul propositionnel : les formules . . . . . . . . . . . . . . . . . . . . 7
2.3 Sémantique du calcul propositionnel . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.3.1 Modèles d’une formule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.3.2 La conséquence logique (d’un ensemble de formules) . . . . . . . . . . . . . 12
2.3.3 Décidabilité du calcul propositionnel . . . . . . . . . . . . . . . . . . . . . . 17
2.4 Equivalence entre formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.4.1 La substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.4.2 Equivalences classiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.4.3 Formes normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.5 Le problème SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.5.1 Définition du problème . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.5.2 Un problème NP-complet . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.5.3 Modélisation - Réduction à SAT . . . . . . . . . . . . . . . . . . . . . . . . 23
2.5.4 Algorithmes de résolution de SAT . . . . . . . . . . . . . . . . . . . . . . . 25
2.5.5 Sous-classes de SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.5.6 Les SAT-solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.5.7 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.5.8 Sur la modélisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
2.6 Systèmes de preuve . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.6.1 Définition d’un système formel . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.6.2 La résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.6.3 Correction, complétude et décidabilité . . . . . . . . . . . . . . . . . . . . . 38
2.6.4 Systèmes de preuve à la Hilbert . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.7 Résumé . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

3 Calcul des prédicats 45

3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.2 Préliminaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.2.1 Les fonctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.2.2 Les relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.3 Un exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.3.1 Interprétation 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.3.2 Interprétation 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.3.3 Interprétation 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.3.4 Interprétation 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

3
4 TABLE DES MATIÈRES

3.3.5 Interprétation 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.3.6 Interprétation 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.3.7 Comparaison des interprétations . . . . . . . . . . . . . . . . . . . . . . . . 48
3.4 Expressions et formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.4.1 Les termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.4.2 Le langage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.4.3 Les formules du calcul des prédicats . . . . . . . . . . . . . . . . . . . . . . 50
3.4.4 Occurrences libres et liées d’une variable . . . . . . . . . . . . . . . . . . . . 51
3.5 Sémantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.5.1 Structures et valuations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.5.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.5.3 Un exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
3.5.4 Vocabulaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.6 Manipulation de formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.6.1 Substitution de variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.6.2 Equivalences classiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.6.3 Formes Normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
3.7 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.7.1 Substitions et MGUs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.7.2 Algorithme d’unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
3.7.3 Correction et completude . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
3.8 Résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
3.8.1 Substitution, sur les formules propostionnelles . . . . . . . . . . . . . . . . . 63
3.8.2 Les règles du calcul de la résolution . . . . . . . . . . . . . . . . . . . . . . 64
3.8.3 Utilisation d’un démonstrateur automatique . . . . . . . . . . . . . . . . . . 67

4 Calculabilité 73
4.1 Machines de Turing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
4.2 Problèmes de décision . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.3 Un problème indécidable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
4.4 Thèse de Chruch . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
4.5 Indecidabilité de la logique du premier ordre . . . . . . . . . . . . . . . . . . . . . . 75
Chapitre 1

Introduction

1.1 Pourquoi la logique ?

1.1.1 La formalisation du langage
Le mot logique provient du grec logos (raison, discours), et signifie "science de la raison". Cette
science a pour objets d’étude le discours et le raisonnement. Ceux-ci dépendent bien entendu du
langage utilisé. Si on prend le langage courant, on se rend compte facilement :
— qu’il contient de nombreuses ambiguïtés : nous ne sommes pas toujours sûrs de la sémantique
d’un énoncé ou d’une phrase. Par exemple : « nous avons des jumelles à la maison ». (Deux
filles ou des lunettes optiques ?) Ou « il a trouvé un avocat » (le professionnel ou le fruit ?)
— qu’il est difficile de connaître la véracité d’un énoncé : « il pleuvra demain », « Jean est
laid », « la logique c’est dur ».
— qu’il permet d’énoncer des choses paradoxales :
1. « Je mens » : comme pour tout paradoxe de ce type, on aboutit à la conclusion que si
c’est vrai alors c’est faux. . . et inversement.
2. « Je suis certain qu’il n’y a rien de certain »
3. Un arrêté enjoint au barbier (masculin) d’un village de raser tous les hommes du village
qui ne se rasent pas eux-mêmes et seulement ceux-ci. Le barbier n’a pas pu respecter
cette règle car :
— s’il se rase lui-même, il enfreint la règle, car le barbier ne peut raser que les hommes
qui ne se rasent pas eux-mêmes ;
— s’il ne se rase pas lui-même (qu’il se fasse raser ou qu’il conserve la barbe), il est en
tort également, car il a la charge de raser les hommes qui ne se rasent pas eux-mêmes.
4. Paradoxe de Russel : c’est la version mathématique du paradoxe du barbier : soit a
l’ensemble des ensembles qui ne se contiennent pas eux-même. Cet ensemble n’existe pas
car on peut vérifier que a 2 a ssi a 2
/ a.
Tout ceci fait que les langues naturelles ne sont pas adaptées au raisonnement formel. C’est
pourquoi par exemple, on vous a appris un langage spécifique pour faire des preuves en mathéma-
tique. Une preuve mathématique ne peut être faite en utilisant tout le vocabulaire de la langue
naturelle car les énoncés et les preuves deviendraient alors ambiguës. Le langage utilisé en mathé-
matique est celui de la logique classique (en réalité, c’est un langage un peu plus souple, entre la
logique classique et la langue naturelle).

1.1.2 La formalisation du raisonnement

Une fois le langage formalisé, ce qui intéresse les logiciens c’est le raisonnement, et en particulier,
la définition de systèmes formels permettant de mécaniser le raisonnement. Au début du 20ième
siècle, le rêve du logicien est de faire de la logique un calcul et de mécaniser le raisonnement et
par suite toutes les mathématiques. En 1930, Kurt Gödel met fin à cette utopie en présentant son
résultat d’incomplétude : il existe des énoncés d’arithmétique qui ne sont pas prouvable par un

5
6 Chapitre 1. Introduction

système formel de preuve. Il n’existe donc pas d’algorithme qui permette de savoir si un énoncé
mathématique est vrai.

1.2 Logique et informatique

Malgré ce résultat négatif, l’arrivée de l’informatique à partir des années 30 marque l’essor de
la logique.
Elle est présente dans quasiment tous les domaines de l’informatique :
— vous verrez par exemple en cours d’architecture que votre ordinateur est formé de circuits
logiques.
— la programmation n’est au fond que de la logique. Dans les année 60, la correspondance
de Curry-Howard, établie une correspondance preuve/programme : une relation entre les
démonstrations formelles d’un système logique et les programmes d’un modèle de calcul.
— le traitement automatique des langues,
— l’intelligence artificielle,
— la logique apparait également dans toutes les questions de sureté.
On demande maintenant de plus en plus de prouver la sureté des programmes et des pro-
tocoles. Pour cela on modélise les exécutions des programmes, on exprime les propriétés de
sûreté par une formule logique, puis on vérifie que les modèles satisfont bien la formule.
A cette effet, d’innombrables logiques ont étés développées, comme les logiques temporelles
qui permettent de raisonner sur l’évolution de certains systèmes au cours du temps. Il existe
même des logiques pour formaliser les règles des pare-feu, afin d’éviter d’avoir des systèmes
de règle incohérents.
— et plein d’autres que j’oublie.
Il existe également des logiciels qui permettent de prouver des formules logique (automatique-
ment ou semi-automatiquement). En particulier on a des logiciels permettant de générer du code
vérifié : on entre une abstraction du programme a réaliser, on prouve sur cette abstraction de façon
plus ou moins automatique mais sûre, les propriétés de sûreté souhaitées ; et le logiciel produit du
code certifié.
L’informatique est donc indissociable de la logique. Heureusement tout bon informaticien n’est
pas obligé d’être un bon théoricien de la logique, mais il doit être capable maitriser son utilisation.

1.3 Contenu du cours

On s’intéressera principalement à (des fragments de) la logique classique, qui est la logique
utilisée pour les mathématiques, et forme la base de presque toutes les autres logiques.
Nous allons nous intéresser aux fragment suivants :
— la logique propositionnelle ;
— la logique du premier ordre.
Pour chacune de ces logiques, nous nous poserons principalement les questions suivantes :
— Quelle est sa syntaxe ? I.e., comment écrire une phrase dans le langage de la logique considéré.
— Quel est sa sémantique ? C’est-à-dire, étant une phrase, savoir lui attribuer un sens. Cette
question ouvre à une autre qui est "de quel forme sont les modèles d’une formule", c’est
à dire : mon langage parle d’objets, qui se placent dans un univers précis : quel est cet
univers ?
— La logique est elle-décidable ? Etant donné une phrase (formule) du langage, existe-il une
procédure effective permettant d’évaluer cette formule.
— Existe-il un système formel de calcul permettant de "prouver" qu’un énoncé est vrai ou
faux.
D’autres questions se posent évidement mais se sont principalement celles-ci qui intéressent l’in-
formaticien.
Chapitre 2

Calcul propositionnel

2.1 Introduction
Les formules (ou phrases, ou énoncés) du calcul propositionnel sont de deux types : ou bien
une formule est une proposition atomique, ou bien elle est composée à partir d’autres formules
à l’aide des connecteurs logiques ^, ¬, _, ) (et, non, ou, implique, que l’on appelle connecteurs
propositionnels).
Considérons, par exemple, l’énoncé arithmétique « 2+2 = 4 ou 3+3 = 5 ». Cet énoncé peut se
considérer comme construit des propositions atomiques « 2+2 = 4 » et « 3+3 = 5 », via le connecteur
propositionnel ou. Une analyse similaire peut se faire pour les énoncés du langage naturel. On
considère l’énoncé « s’il pleut, alors le soleil se cache », que l’on reconnaîtra être équivalent à « il
pleut implique que le soleil se cache », comme obtenu des deux propositions atomiques « s’il pleut »
et « le soleil se cache » via le connecteur propositionnel implique.
Une proposition atomique est un énoncé simple, ne pouvant prendre que les valeurs "vrai" ou
"faux ", et ce de façon non ambiguë ; elle donne donc une information sur un état de chose. De
plus une proposition atomique est indécomposable : « le ciel est bleu et l’herbe est verte » n’est
pas une proposition atomique mais la composition de deux propositions atomiques. Dans l’analyse
du langage naturel, on ne peut pas considérer comme des propositions : les souhaits, les phrases
impératives ou les interrogations.
Nous avons déjà vu des exemples de formules composées. Considérons maintenant l’énoncé
« s’il neige, alors le soleil se cache et il fait froid ». C’est une formule composée, via le connecteur
implique, depuis la formule atomique « il neige » et la formule composée « le soleil se cache et il fait
froid ». On peut donc composer des formules à partir d’autres formules composées. La valeur de
vérité d’une formule composée se calcule comme une fonction des formules dont elle est composée.
Le calcul des propositions est la première étape dans la définition de la logique et du rai-
sonnement. Il définit les règles de déduction qui relient les phrases entre elles, sans en examiner
le contenu ; il est ainsi une première étape dans la construction du calcul des prédicats, qui lui
s’intéresse au contenu des propositions.
Nous partirons donc en général de faits : "p est vrai, q est faux" et essaierons de déterminer si
une affirmation particulière est vraie.

2.2 Syntaxe du calcul propositionnel : les formules

Le langage du calcul propositionnel est formé de :
— symboles propositionnels Prop = {p1 , p2 , . . .} ;
— connecteurs logiques {¬, ^, _, )} ;
— symboles auxiliaires : parenthèses et espace.

Remarque 2.1. Dans la littérature logique on utilise plusieurs synonymes pour symbole proposi-
tionnel ; ainsi variable propositionnelle, proposition atomique, formule atomique, ou encore atome
sont tous des synonymes de symbole propositionnel.

7
8 Chapitre 2. Calcul propositionnel

L’ensemble Fcp des formules du calcul propositionnel est le plus petit ensemble tel que :
— tout symbole propositionnel est une formule ;
— si ' est une formule alors ¬' est une formule ;
— si ', sont des formules alors ' _ , ' ^ et ' ) sont des formules.

Les symboles auxiliaires ne sont utilisés que pour lever les ambiguïtés possibles : par exemple,
la formule p _ q ^ r est ambiguë, car elle peut se lire de deux façons différentes, ((p _ q) ^ r) ou bien
(p _ (q ^ r)).
Exemple 2.2. p, p ) (q _ r) et p _ q sont des formules propositionnelles ; ¬(_q) et f (x) ) g(x)
n’en sont pas.
A cause de la structure inductive de la définition, une formule peut-être vue comme un arbre
dont les feuilles sont étiquetés par des symboles propositionnels et les noeuds par des connecteurs.
Par exemple, la formule p ) (¬q ^ r) correspond à l’arbre représenté Figure 2.2.

p ^

¬ r

Figure 2.1 – Représentation arborescente de la formule p ) (¬q ^ r)

Notation 2.3. On utilise souvent en plus le connecteur binaire , comme abréviation : ' , est
l’abréviation de (' ) ) ^ ( ) '). De la même façon, on ajoute le symbole ? qui correspond à
Faux et le symbole > qui correspond à Vrai. Ces deux symboles sont aussi des abréviations, ils ne
sont pas indispensables au langage. (Par exemple ? peut être utilisé à la place de p ^ ¬p et > à la
place de p _ ¬p.)
Définition 2.4 (Sous-formule). L’ensemble SF (') des sous-formules d’une formules ' est défini
par induction de la façon suivante.
— SF (p) = {p} ;
— SF (¬') = {¬'} [ SF (') ;
— SF (' ) = {' } [ SF (') [ SF ( ) (où désigne un des symboles ^, _, )).
Par exemple, SF (p ) (¬q ^ r)) = {p, q, r, ¬q, ¬q ^ r, p ) (¬q ^ r)}. Quand on voit une formule
comme un arbre, une sous-formule est simplement un sous-arbre (voir Figure 2.2).
Définition 2.5 (Sous-formule stricte). est une sous-formule stricte de ' si est une sous-formule
de ' qui n’est pas '.

2.3 Sémantique du calcul propositionnel

Il faut maintenant un moyen de déterminer si une formule est vraie ou fausse. La première
étape est de donner une valeur de vérité aux propositions atomiques. L’évaluation d’une formule,
dépend donc des valeurs choisies pour les symboles propositionnels. Ces valeurs sont données par
une valuation.
Définition 2.6 (Valuation). Une valuation est une application de Prop dans {0, 1}. La valeur 0
désigne le "faux" et la valeur 1 désigne le "vrai".
2.3 Sémantique du calcul propositionnel 9

p ^

¬ r

Figure 2.2 – Représentation arborescente des sous-formules de p ) (¬q ^ r)

Une valuation sera souvent donnée sous forme d’un tableau. Par exemple, si Prop = {p, q}
p q
alors la valuation v : p 7! 1, q 7! 0 s’écrit plus simplement v :
1 0
Une fois la valuation v choisie, la valeur de la formule se détermine de façon naturelle, par
extension de la valuation v aux formules de la façon suivante :

Définition 2.7 (Valeur d’une formule).

— v(¬') = 1 ssi v(') = 0 ;
— v(' _ ) = 1 ssi v(') = 1 ou v( ) = 1 ;
— v(' ^ ) = 1 ssi v(') = 1 et v( ) = 1 ;
— v(' ) ) = 0 ssi v(') = 1 et v( ) = 0.

La définition précédente peut apparaître trompeuse car circualire : afin d’expliquer la logique,
nous somme en train de l’utiliser (ssi, ou, et . . . ). Par ailleurs, on peut se servir de la définition
suivante qui est en effet équivalente à la Définition 2.7 :

Définition 2.8 (Valeur d’une formule (bis)).

— v(¬') = 1 v(') ;
— v(' _ ) = max(v('), v( )) ;
— v(' ^ ) = min(v('), v( )) ;
— v(' ) ) = v(¬' _ ).

Cette dernière définition est purement combinatoire car elle repose sur la structure de l’ensemble
ordonné fini { 0 < 1 } ; nous supposons en fait que cette structure est évidente et claire par soi-même
qu’il n’y a pas besoin de la justifier par d’autres moyens.

Exercice 2.9. Proposez un algorithme qui, étant donné une formule ' du calcul propositionnel et
une valuation v, calcule v('). Quel type de structure de données utiliser pour coder les formules ?
Quel type de structure de données utiliser pour coder les valuations ?

Notez que la définition 2.8 correspond aux tables de vérité des connecteurs logiques (dont vous
avez sûrement entendu parler) :

p q p^q p q p_q p q p)q

p ¬p 0 0 0 0 0 0 0 0 1
0 1 0 1 0 0 1 1 0 1 1
1 0 1 0 0 1 0 1 1 0 0
1 1 1 1 1 1 1 1 1

Remarque 2.10 (Langage naturel et langage formel). Remarquez la définition particulière de

l’implication : on l’entend en général comme un "si ..., alors ...", on voit ici que l’énoncé "si 1+1=1,
alors la capitale de la France est Marseille" est vrai, puisque toute phrase ' ) est vraie dès
10 Chapitre 2. Calcul propositionnel

lors que ' est évaluée à faux. Ceci est peu naturel, car dans le langage courant, on ne s’intéresse à
la vérité d’un tel énoncé que lorsque la condition est vraie : "s’il fait beau je vais à la pêche" n’a
d’intérêt pratique que s’il fait beau. . . Attribuer la valeur vrai dans le cas ou la prémisse est fausse
correspond a peu près à l’usage du si .. alors dans la phrase suivante : "Si Pierre obtient sa Licence,
alors je suis Einstein" : c’est à dire que partant d’une hypothèse fausse, alors je peux démontrer
des choses fausses (ou vraies). Par contre, il n’est pas possible de démontrer quelque chose de faux
partant d’une hypothèse vraie.
D’autres exemples où il est difficile de coder le langage naturel via le langage formel :
— comment coderiez vous, en langage formel, l’énoncé français « Soit il est frais, soit il est
chaud » ?
— et comment coderiez vous l’énoncé anglais « Either I cannot understand French, or my
professor doesn’t know how to speak it » ?

On peut ajouter la définition de la valeur de l’abréviation , : v(' , ) = 1 ssi v(') = v( ).

Ce qui correspond à la table de vérité suivante :

p q p,q
0 0 1
0 1 0
1 0 0
1 1 1

Exercice 2.11. Définissons l’ensemble Prop('), des variables propositionnelles contenues dans
' 2 Fcp , par induction comme suit :

Prop(p) = { p } ,
Prop(¬') = Prop(') ,
Prop(' ) = Prop(') [ Prop( ) , 2 { ^, _, ) } .

Montrez que :
— Prop(') = Prop \ SF ('), pour tout ' 2 Fcp ;
— si v(p) = v 0 (p) pour tout p 2 Prop('), alors v(') = v 0 (').

2.3.1 Modèles d’une formule

Définition 2.12. L’ensemble des valuations d’un ensemble de variables propositionnelles Prop
est noté Val(Prop) (ou juste Val lorsqu’il n’y a pas d’ambiguité sur Prop). Val(Prop) est donc
l’ensemble des fonctions de Prop dans {0, 1}.

Par exemple, si Prop = {p, q, r}, alors Val est représenté par la Table 2.3.1, dans lequel chaque
ligne est une valuation de Prop :

p q r
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1

Table 2.1 – L’ensemble Val(Prop) des valuations de Prop = {p, q, r}

Définition 2.13 (Modèle d’une formule). Un modèle de ' est une valuation v telle que v(') = 1.
On note mod(') l’ensemble des modèles de '.
2.3 Sémantique du calcul propositionnel 11

Exemple 2.14. Si Prop = {p, q, r} et ' = (p _ q) ^ (p _ ¬r) alors l’ensemble des modèles de ' est
p q r
0 1 0
1 0 0
mod(') =
1 1 1
1 1 0
1 1 1
Définition 2.15 (Satisfaisabilité). Une formule ' est satisfaisable (ou consistante, ou encore
cohérente) si elle admet un modèle (i.e., s’il existe une valuation v telle que v(') = 1, i.e. si
mod(') 6= ?).
Définition 2.16 (Insatisfaisabilité). Une formule ' est insatisfaisable (ou inconsistante, ou
incohérente) si elle n’admet aucun modèle (i.e., si pour toute valuation v, v(') = 0, i.e., si
mod(') = ?)
Définition 2.17 (Tautologie). Une formule ' est une tautologie (ou valide) si v(') = 1 pour
toute valuation v (i.e., si mod(') = Val). On note |= ' pour dire que ' est une tautologie.
Un exemple de tautologie est ' _ ¬', c’est à dire le tiers exclus.
Exercice 2.18. Montrez que les formules suivantes sont des tautologies :
p ) p, p ) (q ) p) , (p ) (q ) r)) ) ((p ) q) ) (p ) r)) , ((p ) q) ) p) ) p .
Définition 2.19 (Equivalence). On dit que ' est équivalente à si les deux formules ont les
mêmes modèles (i.e. si mod(') = mod( )). On note alors ' ⌘ .
Exemple 2.20. Les opérateurs ^, _ sont associatifs-commutatifs. Deux formules identiques à
associativité-commutativité près sont équivalentes. Remplacer une sous-formule d’une formule
' par une formule équivalente 0 donne une formule notée '[ 0
]. Cette substitution préserve
les modèles, i.e., mod(') = mod('[ 0
]).
Exercice 2.21. Prouvez les équivalences suivantes :
'_?⌘' '^?⌘? (' ^ ) ^ ✓ ⌘ ' ^ ( ^ ✓)
'_>⌘> '^>⌘' (' ^ ) _ ✓ ⌘ (' ^ ✓) _ ( ^ ✓)
'_ ⌘ _' '^ ⌘ ^' (' _ ) ^ ✓ ⌘ (' ^ ✓) _ (' ^ ✓)
'_'⌘' ¬(' _ ) ⌘ (¬') ^ (¬ ) (' _ ) _ ✓ ⌘ ' _ ( _ ✓)
¬¬' ⌘ ' '^'⌘' ¬(' ^ ) ⌘ (¬') _ (¬ ) .
Proposition 2.22. Soient ' et deux formules, on a :
1. mod(¬') = Val mod(') ;
2. mod(' _ ) = mod( ) [ mod( ) ;
3. mod(' ^ ) = mod( ) \ mod( ) ;
4. |= ' ) ssi mod(') ✓ mod( ).
Démonstration. 1. pour toute valuation v 2 Val,
v 2 mod(¬') ssi v(¬') = 1
ssi v(') = 0
ssi / mod(')
v2
ssi Val mod(')

2. pour toute valuation v 2 Val,

v 2 mod(' _ ) ssi v(') = 1 ou v( ) = 1
ssi v 2 mod(') ou v 2 mod( )
ssi mod(') [ mod( )
12 Chapitre 2. Calcul propositionnel

3. pour toute valuation v 2 Val,

v 2 mod(' ^ ) ssi v(') = 1 et v( ) = 1

ssi v 2 mod(') et v 2 mod( )
ssi mod(') \ mod( )

4.

|= ' ) ssi pour toute valuation v 2 Val, v(' ) ) = 1

ssi pour toute valuation v 2 Val, v(¬' _ ) = 1
ssi pour toute valuation v 2 Val, v(') = 0 ou v( ) = 1
ssi pour toute valuation v 2 Val, v(')  v( )
ssi mod(') ✓ mod( )

Définition 2.23 (Conséquence logique). Une formule est conséquence logique d’une formule
' si tout modèle de ' est un modèle de (i.e., si mod(') ✓ mod( )). On note alors ' |= .

Remarque 2.24. Attention à la confusion dans les deux notations !

— v |= ' où v est une valuation, i.e., l’assignation d’une valeur aux propositions atomiques
de la formule ; c’est un raccourcis assez fréquent pour v(') = 1 ;
— |= ' où est une formule.

Proposition 2.25. Soient ' et deux formules propositionnelles.

1. ' |= si et seulement si |= ' ) .
2. ' ⌘ si et seulement si |= ' , .

Démonstration. 1. Conséquence directe du point 4 de la Proposition 2.22

2. |= ' , ssi 8v 2 Val, v(' , ) = 1 (par la définition de tautologie) ssi 8v 2 Val, v(') = v( )
(par la table de verité de ,) ssi 8v 2 Val, v 2 mod(') ssi v 2 mod( ) ssi mod(') = mod( )
ssi ⌘ '.

2.3.2 La conséquence logique (d’un ensemble de formules)

Les formules propositionnelles peuvent être vues comme des contraintes sur les propositions
atomiques. Par exemple, p ^ q contraint p et q à être vraies, où p ) q contraint q à être vraie toute
fois que p est vraie. Il est donc très courant de considérer des ensembles de formules proposition-
nelles pour modéliser des problèmes de satisfaction de contraintes. Une valuation satisfaisant toute
formule de l’ensemble pourra donc se considérer comme une solution du problème.
On étend les définitions vues précédemment aux ensembles de formules.

Définition 2.26 (Modèle). Un modèle d’un ensemble de formules est une valuation v telle que
v(') = 1 pour tout ' 2 . On note mod( ) l’ensemble des modèles de .

Cet ensemble de modèles est donc l’ensemble des valuations qu’on peut attribuer aux variables
si on veut respecter toutes les contraintes de .

Définition 2.27 (Satisfaisabilité/Consistance, Insatisfaisabilité/Contradiction). Un ensemble de

formules est
— satisfaisable (ou consistant, ou cohérent) s’il admet au moins un modèle (i.e., si
mod( ) 6= ?) ;
— insatisfaisable (ou contradictoire, ou inconsistant, ou encore incohérent) s’il n’ad-
met aucun modèle ( i.e., si mod( ) = ?), on note alors |=?.

Un ensemble contradictoire ne peut être satisfait : par exemple l’ensemble = {p, ¬p} est
insatisfaisable.
2.3 Sémantique du calcul propositionnel 13

Définition 2.28 (Conséquence logique). Une formule ' est conséquence logique de si et seule-
ment si toute valuation qui donne 1 à toutes les formules de donne 1 à ' (i.e., si mod( ) ✓ mod(')),
on note alors |= '. On note cons( ) l’ensemble des conséquences logiques de .
Remarque 2.29. Attention aux deux notations :
— |= ' où est une formule ;
— |= ' où est un ensemble de formule.
Remarquez, par ailleurs que ' |= si, et seulement si, { ' } |= ; les deux dernières notations sont
donc cohérentes entre elles.
Voici des relations élémentaires entre les relations que nous venons de présenter.
Proposition 2.30. |= ' ssi [ {¬'} est contradictoire.
Démonstration. |= ' ssi
pour toute valuation v
— soit v est un modèle de et v(') = 1
— soit v n’est pas un modèle de
ssi pour toute valuation v
— soit v est un modèle de et v(¬') = 0
— soit v n’est pas un modèle de
ssi pour toute valuation v, v n’est pas un modèle de [ {¬'}
ssi [ {¬'} est contradictoire.
Proposition 2.31. Pour tous ensembles de formules ⌃, ,
mod(⌃ [ ) = mod(⌃) \ mod( ).

En particulier, si ⌃ ✓ alors mod( ) ✓ mod(⌃).

Cette proposition se comprend bien si on voit un ensemble de formules comme un ensemble de
contraintes sur les variables propositionnelles. Plus on ajoute de contraintes, et moins il reste de
possibilités pour résoudre ces contraintes.
Démonstration de la Proposition 2.31. Pour toute valuation v :
v 2 mod(⌃ [ ) ssi pour tout ' 2 ⌃ [ , v(') = 1
ssi pour tout ' 2 ⌃, v(') = 1 et pour tout 2 , v( ) = 1
ssi v 2 mod(⌃) et v 2 mod( )
ssi v 2 mod(⌃) \ mod( ).
La preuve de la Proposition suivante est laissée en exercice.
Proposition 2.32. Si 0
✓ et 0
|= ', alors |= '.
Proposition 2.33. {'1 , . . . 'n } |= ssi |= ('1 ^ . . . ^ 'n ) )
Cette proposition exprime le fait qu’un ensemble fini de formules propositionnelles peut toujours
être vu comme une seule formule formée de la conjonction des formules de l’ensemble. Une formule
étant un objet fini, ce résultat ne se généralise pas au cas des ensembles de taille non bornée. Dans
le cas où est infini, il faudra utiliser le théorème de compacité (Théorème 2.39) qui permet de
ramener les problèmes de satisfaisabilité et de contradiction d’un ensemble de taille quelconque à
celle d’ensemble finis.
Démonstration. Remarquons que
mod({ '1 , . . . , 'n }) = mod({ '1 } [ . . . [ { 'n })
= mod({ '1 }) \ . . . \ mod({ 'n }) (par la Proposition 2.31)
= mod('1 ) \ . . . \ mod('n ) (par la Remarque 2.29)
= mod('1 ^ . . . ^ 'n ) . (par la Propositon 2.22)
Donc, on a que mod({ '1 , . . . , 'n }) ✓ mod( ) si et seulement si mod('1 ^ . . . ^ 'n ) ✓ mod( ) et,
par la Proposition 2.22, la dernière relation est vraie ssi ('1 ^ . . . ^ 'n ) ) est une tautologie.
14 Chapitre 2. Calcul propositionnel

Proposition 2.34. |= ' si, et seulement si, mod( ) = mod( [ {'}).

La proposition peut se comprendre comme suit. Une conséquence logique ' d’un ensemble
est une nouvelle contrainte déduite directement de . Puisqu’elle découle de , elle ne peut pas
apporter des “vraies” contraintes supplémentaires que celles apportées par . Cela signifie que les
modèles de et ceux de [ {'} sont exactement les mêmes.
Démonstration de la Proposition 2.34. La proposition découle du fait que mod( [{'}) = mod( )\
mod({'}), et que la relation mod( ) ✓ mod(') est équivalente à mod( ) \ mod({'}) = mod( ).

Exemple 2.35. L’ensemble = {(p ) s) _ q, ¬q} possède comme conséquence logique p ) s.

Bien entendu, les modèles de sont exactement les modèles de [ {p ) s}.
La Proposition 2.34 implique également une méthode de simplification d’un ensemble de for-
mules : si contient une formule ' conséquence logique de {'}, alors ' peut être retirée de
l’ensemble de contraintes sans en modifier la sémantique, mod( ) = mod( {'}). L’exemple
suivant éclaircit cette méthode.
Exemple 2.36. Avec cet exemple, nous allons tirer avantage des propositions et remarques pré-
cédentes pour résoudre un ensemble de contraintes ayant une certaine complexité.
On dispose de 4 variables propositionnelles, pA , pB , pC , pD , qui obéissent aux contraintes sui-
vantes :
'1 : pB ^ ¬pC
'2 : pA ) (pC _ pD )
'3 : ¬pC ^ (pB _ pA )

Soit 1 = {'1 , '2 , '3 }, cet ensemble forme l’ensemble des prémisses à partir desquelles nous
allons essayer de déduire les valeurs que les variables propositionnelles peuvent prendre.
On se pose les questions suivantes :
1. Peut-on simplifier l’ensemble 1 de façon à ne pas changer l’ensemble de ses modèles, et donc
de ses conséquences ?
(a) On remarque que la contrainte '3 est une conséquence logique de la contrainte '1 .
En effet, pour toute valuation v,
— v satisfait '1 ssi v(pC ) = 0 et v(pB ) = 1,
— v satisfait '3 ssi v(pC ) = 0 et (v(pA ) = 1 ou v(pB ) = 1).
D’où, mod('1 ) ✓ mod('3 ).
(b) Soit 2 = {'1 , '2 }, on a mod( 2 ) = mod( 1 ). En effet, par définition,
mod( 1 ) = mod('1 ) \ mod('2 ) \ mod('3 ) = mod('1 ) \ mod('2 ) = mod( 2 ).
Donc les conséquences de 1 et 2 sont les mêmes et on peut alors simplifier 1 par 2.
2. Quel est l’ensemble des modèles de 2?

Modèles de '1 : Modèles de '2 :

pA p B pC pD p A pB pC pD
0 1 0 0 0 0 0 0
0 1 0 1 0 0 0 1
1 1 0 0 0 0 1 0
1 1 0 1 0 0 1 1
0 1 0 0
0 1 0 1
0 1 1 0
0 1 1 1
1 0 0 1
1 0 1 0
1 0 1 1
1 1 0 1
1 1 1 0
1 1 1 1
2.3 Sémantique du calcul propositionnel 15

L’ensemble M des modèles de 2 est l’intersections des modèles de '1 et '2 :

pA pB pC pD
0 1 0 1
1 1 0 1
3. 2 est-il consistant ? contradictoire ?
2 admet un modèle, il est donc consistant et non contradictoire.
4. Quelles conséquences logiques pouvons nous tirer de l’ensemble 2 ?
Les conséquences logiques de 2 sont toutes les formules dont l’ensemble des modèles contient
M . On a donc entre autres :
¬pC , pB , pB ^ ¬pC 2 cons( )
5. Ajoutons maintenant une nouvelle contrainte : 3 = {¬pB ^ ¬pD } [ 2 . On a mod( 3) =
mod( 2 ) \ mod(¬pB ^ ¬pD ) = ?. Donc mod( 3 ) = ? et 3 est contradictoire.

2.3.2.1 Compacité
Le théorème de compacité sert à caractériser la conséquence logique dans les cas où l’ensemble
des formules est infini en ne considérant que des sous-ensembles finis. Par ailleurs, ce théorème
jouera un rôle cruciale plus tard, dans le cadre de la preuve de complètude pour la calcul de la
résolution (Théorème 3.66).

Le théorème de compacité Pour commencer, nous avons besoin du lemme suivant appelé
Lemme de König.

Lemme 2.37 (König). Tout arbre infini à branchement fini possède une branche infinie.

Démonstration. Supposons que T , qui est à branchement fini, soit infini. On définit une branche
infinie dans T , ce qui mènera à la conclusion. Pour construire cette branche, on montre, par
induction sur les entiers, que la propriété suivante :

P (n) ::= il existe une branche e0 , . . . , en telle que le sous arbre issu de en est infini

est vraie de tout entier n 0.

(Base de l’induction). Pour n = 0, on choisit e0 = r (la racine de l’arbre) qui par hypothèse
est la racine d’un arbre infini.
(Étape inductive). On suppose P (n) vraie et on montre P (n + 1). Par hypothèse, il existe une
branche e0 , . . . , en telle que le sous arbre issu de en est infini. Considérons les successeurs
immédiats de en , disons en1 , . . . , enk : si tous étaient racines de sous-arbres finis, disons de
cardinaux p1 , . . . , pk , alors il en serait de même de en (avec un cardinal d’au plus p1 +...+pk+1 ),
contradiction. Donc l’un d’entre eux est le en+1 recherché.

Nous aurons besoin du Lemme dans la forme suivante :

Lemme 2.38. Tout arbre a branchement fini et dont toutes les branches sont finies, est fini.

Théorème 2.39 (Compacité). Un ensemble de formules propositionnelles est satisfaisable ssi

tout sous-ensemble fini de est satisfaisable.

Par contraposée, le Théorème de compacité peut s’énoncer de la façon suivante :

Théorème 2.40 (Compacité). Un ensemble de formules propositionnelles est contradictoire si,

et seulement si, il existe un sous-ensemble fini de contradictoire.

Remarquons que l’implication « si un sous-ensemble fini de est contradictoire, alors est

contradictoire » est trivialement vraie. Nous nous limiterons à prouver l’implication inverse.
16 Chapitre 2. Calcul propositionnel

p0
0 1

p1
0 1 0 1

p 0 ) p1 p2

Figure 2.3 – Début de l’arbre sémantique avec le noeud d’échec 10 étiqueté

Démonstration. On fait la preuve dans le cas où Prop = {p0 , p1 , p2 , . . . , pn , . . .} est un ensemble

dénombrable.
Nous avons besoin d’une construction importante appelée « arbre sémantique » ou « arbre de
Herbrand ». L’arbre sémantique associé est un arbre binaire infini dont toutes les arêtes à gauches
sont étiquetées par 0 (le « faux ») et celles à droites sont étiquetées par 1 (le « vrai »). Chaque
niveau de l’arbre est associé à une proposition. La racine (le niveau 0) est associé à p0 : chaque fois
que l’on descend d’un noeud de niveau i, ceci revient à poser pi faux si l’on descend à gauche, et
pi vrai si l’on descend à droite. Remarquons que :
1. chaque chemin infini partant de la racine correspond à une valuation de l’ensemble des pro-
positions ;
2. chaque noeud e à profondeur n correspond à une valuation ve des variables {p0 , . . . pn 1 }.

Nous appelons un noeud e de l’árbre noeud d’échec (par rapport à ) s’il existe une formule 'e 2
telle que Prop('e ) ✓ { p0 , . . . pn 1 } et ve ('e ) = 0, où n est la profondeur du noeud e.

On suppose que est inconsistante et on montre qu’il existe un sous-ensemble 0 ✓ fini et

inconsistant.
On commence par remarquer que chaque branche contient un noeud d’échec. En effet, si une
branche n’en contient pas, elle définit un modèle de , ce qui est contradictoire à l’hypothèse.
On peut donc faire la construction suivante : prenons le premier noeud d’échec de chaque
branche et étiquetons ce noeud par une formule de fausse sur ce noeud, puis coupons l’arbre
au niveau du noeud d’echec. (Plus formellement, si ⇡ est une branche de l’arbre sémantique,
dénotons par e(⇡) le premier noeud d’échec sur cette branche, et choisissons 'e(⇡) 2 tel que
ve(⇡) ('e(⇡) ) = 0 ; ensuite, coupons l’arbre de façon que les noeuds e(⇡) deviennent des feuilles de
l’arbre.)
L’arbre obtenu en tronquant ainsi toutes les branches est un arbre à branchement fini, ses
branches sont finies, et donc il est fini par le Lemme de König. Le sous-ensemble 0 = { 'e(⇡) |
⇡ une branche de l’arbre sémantique } des formules de étiquetant les feuilles de l’arbre est donc
fini. Or toutes les feuilles de l’arbre sont des noeuds d’échec et donc chacune des valuations rend
fausse au moins une des formules de 0 . (Si v 2 Val, alors v = v⇡ pour une branche ⇡ de l’arbre, et
donc v('e(⇡) ) = ve(⇡) ('e(⇡) ) = 0.) L’ensemble 0 ✓ est donc fini et inconsistant.

Exemple 2.41. Supposons que soit de la forme { p0 ^ ¬p1 , p0 ) p1 , . . . }. Alors le noeud e = 10

de l’arbre sémantique est un noeud d’échec par rapport à cet ensemble , car p0 ) p1 2 and
ve (p0 ) p1 ) = 0. (Le debut de) l’arbre sémantique, avec le noeud 10 étiqueté par la formule
témoignant son échec, est représenté en Figure 2.3.

Remarque 2.42. On peut donner une preuve plus simple du théorème de compacité en utilisant
les propriétés des systèmes de preuves. Nous la donnerons par la suite, lorsque nous aurons les
outils nécessaires.

Corollaire du théorème de compacité :

Corollaire 2.43. Une formule ' est conséquence d’un ensemble de formules si et seulement s’il
existe un sous-ensemble fini f ini de tel que f ini |= '.
2.3 Sémantique du calcul propositionnel 17

Démonstration.

|= ' ssi [ {¬'} est contradictoire par la Proposition 2.30

ssi il existe f ✓ [ {¬'} fini et contradictoire par le Théorème de compacité
ssi il existe f ✓ fini tel que f [ {¬'} est contradictoire
ssi il existe un sous-ensemble fini f ✓ tel que f |= ' .

2.3.3 Décidabilité du calcul propositionnel

Une logique est décidable s’il existe un algorithme (calcul réalisable sur un ordinateur qui
termine toujours pour toute donnée) qui permet de savoir pour chaque formule si elle est une
tautologie (i.e. si |= ') ou pas.
Théorème 2.44. Le calcul propositionnel est décidable.
Démonstration. Méthode des tables de vérité : calculer la table de vérité prenant en argument les
symboles propositionnels de ' et calculer pour chaque valuation possible la valeur de '.
Coût : O(2n ) avec n la taille de ' (nombre de propositions).

Nous verrons par la suite qu’il y a de meilleurs algorithmes, mais qu’il ont tous un coût ex-
ponentiel. La plupart de ces algorithmes débutent par une première phase de normalisation de la
formule, c’est à dire qu’on modifie la syntaxe de la formule de manière à la mettre sous une forme
normalisée, tout en conservant la sémantique de la formule, c’est-à-dire l’ensemble de ses modèles.
18 Chapitre 2. Calcul propositionnel

2.4 Equivalence entre formules

Il est courant de souhaiter modifier une formule, de façon à rendre son expression plus simple,
ou plus facile à manipuler, et ceci en gardant bien sûr la sémantique de la formule, c’est-à-dire,
sans modifier l’ensemble de ses modèles.

2.4.1 La substitution
La substitution d’une formule par une formule 0 dans une troisième formule ' (notée '[ 0])

consiste à remplacer chaque occurrence de dans ' par 0 .

Prenons par exemple ' = (¬p _ q) ^ (¬p _ ¬r), = ¬p et 0 = q ) p. Alors '[ 0 ] = ((q )

p) _ q) ^ ((q ) p) _ ¬r).
Plus formellement, la substitution est définie de la façon suivante :
Définition 2.45 (Substitution). Soient ', , et 0 trois formules du calcul propositionnel,
— si n’est pas une sous-formule de ', alors '[ 0] = '

— sinon si ' = alors '[ 0] =

0

— sinon
— si ' = ¬'0 alors '[ 0 ] = ¬('
0
[ 0])

— si ' = '1 '2 (où est un connecteurs ^, _, )) alors '[ 0 ] = '1

[ 0] '2 [ 0] .
Proposition 2.46. Soient ', , et 0
trois formules du calcul propositionnel, si ⌘ 0
alors
' ⌘ '[ 0].

Démonstration. Voir TD 3.
Attention, dans le cas général, la substitution ne conserve pas la sémantique de la formule. Par
exemple, p et q ^ ¬q ne sont pas équivalentes ; ainsi, les formules p et p[p q ^ ¬q] ne sont pas
équivalentes.

2.4.2 Equivalences classiques

Nous avons vu que remplacer une sous-formule d’une formule ' par une formule équivalente
0
donne une formule notée '[ 0
] équivalente à '. C’est-à-dire que cette substitution préserve
les modèles, i.e., mod(') = mod('[ 0
]).
Voici quelques règles d’équivalences courantes, qui permettent de telles substitutions.

'^ ⌘ ^' '_ ⌘ _' (Commutativité)

'^( 1 ^ 2) ⌘ (' ^ 1) ^ 2 '_( 1 _ 2) ⌘ (' _ 1) _ 2 (Associativité)
>^'⌘'^>⌘' ? _' ⌘ '_ ?⌘ ' (Élements neutres)
'^'⌘' '_'⌘' (Idempotence)
' ^ (' _ ) ⌘ ' ' _ (' ^ ) ⌘ ' (Absorption)
'^ ? ⌘? ^' ⌘? '_>⌘>_'⌘> (Elément absorbant)
'^( 1 _ 2) ⌘ (' ^ 1) _ (' ^ 2) '_( 1 ^ 2) ⌘ (' _ 1) ^ (' _ 2) (Distributivité)
' ^ ¬' ⌘ ¬' ^ ' ⌘? ' _ ¬' ⌘ ¬' _ ' ⌘ > (Complément)
¬¬' ⌘ ' (Involution)
¬(' ^ ) ⌘ ¬' _ ¬ ¬(' _ ) ⌘ ¬' ^ ¬ (Lois de De Morgan)
') ⌘ ¬' _ ⌘ ¬(' ^ ¬ ) (Implication matérielle)
') ⌘ ¬ ) ¬' (Contraposition)
'1 ) ('2 ) '3 ) ⌘ ('1 ^ '2 ) ) '3 (Curryfication)

Nous observons ici que la formule suivante :

[('1 ) '2 )^('2 ) '3 )] ) ['1 ) '3 ] (Transitivité)

est une tautologie, et que ' ⌘ > si et seulement si ' est une tautologie.
2.4 Equivalence entre formules 19

2.4.3 Formes normales

La mise sous forme normale transforme une formule en une formule équivalente (que l’on dit
« normalisée ») plus adaptée au traitement algorithmique.

Notations. Remarquons que, à cause des lois d’associativité et commutativité, toutes les pos-
sibles formules construites à partir des formules '1 , . . . , 'n via l’application du connecteur logique
^, sont équivalentes. Par exemple

(('1 ^ '2 ) ^ '3 ) ^ '4 , '1 ^ (('2 ^ '3 ) ^ '4 ) , '1 ^ ('2 ^ ('3 ^ '4 )) , ('2 ^ '4 ) ^ ('3 ^ '1 ) ,

sont des formules équivalentes. Une remarque analogue vaut pour le connecteur logique _.
Ainsi, si '1 , . . . , 'n sont des formules, nous pourrons utiliser les notations :
n
^ n
_
'i = ' 1 ^ . . . ^ 'n et 'i = '1 _ . . . _ ' n
i=1 i=1

pour dénoter un parenthésage arbitraire de '1 ^ . . . ^ 'n (resp. '1 _ . . . _ 'n ). Les choix de l’ordre
et du parenthésage ne sont donc pas significatifs, au moins du point de vue sémantique.
Nous pouvons même étendre nous considérations plus loin : si possède plus que deux occur-
rence dans la liste '1 , . . . , n , nous pouvons effacer les doublons de cette liste pour obtenir des
formules équivalentes. Par exemple, les formules

'1 ^ '2 ^ ' 1 ^ ' 3 , ' 1 ^ '2 ^ '3 ,

sont équivalents. Moralité : si ni l’ordre, ni le parenthésage, ni la multiplicité comptes, ce qui compte

dans une telle formule est sa structure d’ensemble.
Nous allons donc considérer des conjonctions et disjonctions de liste de formules (avec ou sans
répétions) ; n, la longuer de la liste pourra aussi prendre les valeurs 0 et 1, en posant :
0
^ 0
_
'i := > , 'i := ? , pour n = 0,
i=1 i=1
1
^ 1
_
'i := '1 , 'i := '1 , pour n = 1.
i=1 i=1

Définition 2.47 (Littéral). Un littéral est une formule atomique ou la négation d’une formule
atomique. Autrement dit, c’est une formule ` de la forme p ou ¬p, où p est un symbole proposi-
tionnel.
Wn
Définition 2.48 (Clause). Une clause disjonctive est une disjonction de littérauxV: i=1 `i où
n
les `i sont des littéraux. Une clause conjonctive est une conjonction de littéraux : i=1 `i où les
`i sont des littéraux.
Définition 2.49 (Forme normale conjonctive). Une formule conjonctive (ou formule sous forme
normale Vmconjonctive (FNC), ou sous forme clausale) est une V conjonction de clauses disjonc-
m W nj
tives : j=1 Cj où les Cj sont des clauses disjonctives, ou encore j=1 i=1 `ji où les `ji sont des
littéraux.
Exemple 2.50. La formule suivante est sous forme clausale :

(¬p _ q _ r) ^ (¬q _ p) ^ s

Définition 2.51 (Forme normale disjonctive). Une formule disjonctive (ouWmformule sous forme
normale disjonctive (FND)) est une disjonction de clauses conjonctives : j=1 Cj où les Cj sont
W m V nj j
des clauses, ou encore j=1 i=1 `i , où les `ji sont des littéraux.
Exemple 2.52. La formule suivante est sous forme normale disjonctive :

(¬p ^ q ^ r) _ (¬q ^ p) _ s
20 Chapitre 2. Calcul propositionnel

La forme normale conjonctive est en général la plus adaptée lorsqu’on cherche un modèle d’une
formule car il faut chercher une valuation satisfaisant chacune des clauses de la formule. Dans
l’exemple 2.50, on voit que si v est un modèle, alors forcément v(s) = 1 ; pour satisfaire la deuxième
clause, il faut que v(p) = 1 ou v(q) = 0, mais alors la seule façon de satisfaire la première clause
est r = 1. Il y a donc deux modèles.

2.4.3.1 Mise sous forme clausale, en préservant l’équivalence

L’algorithme est le suivant :
Etape 1 (élimination de l’implication). Appliquer, tant que possible, la substitution suivante :

') ¬' _ .

Etape 2 (pousser la négation vers les symboles propositionnels). Appliquer, tant que pos-
sible, les substitutions suivantes (en remplaçant le membre gauche par le membre droit) :

¬¬' ', ¬(' ^ ) ¬' _ ¬ , ¬(' _ ) ¬' ^ ¬ .

Etape 3 (pousser la disjonction vers les littéraux). Appliquer, tant que possible, les substi-
tutions suivantes (en remplaçant le membre gauche par le membre droit) :

'_( 1 ^ 2) (' _ 1) ^ (' _ 2) .

Exemple 2.53. Considérons ' = (¬(p ^ (¬q _ (r _ s)))) ^ (p _ q).

— Etape 1 : rien à faire
— Etape 2 :
' = (¬p _ ¬(¬q _ (r _ s))) ^ (p _ q)
' = (¬p _ (¬¬q ^ ¬(r _ s))) ^ (p _ q)
' = (¬p _ (q ^ ¬(r _ s))) ^ (p _ q)
' = (¬p _ (q ^ ¬r ^ ¬s)) ^ (p _ q)
— Etape 3 :
' = (¬p _ q) ^ (¬p _ ¬r) ^ (¬p _ ¬s) ^ (p _ q)

Proposition 2.54. Le calcul précédent termine et donne une formule en forme clausale équivalente
à la formule initiale.

Remarque 2.55. Il n’y a pas unicité de la forme clausale.

2.4.3.2 Mise sous forme clausale, en préservant la satisfaisabilité

Considérons un formule du calcul propositionnel ayant comme sous-formule : cette formule
sera donc de la forme '[p ], où on peut choisir p 62 Prop( ).

Proposition 2.56. Soit ', 2 Fcp and soit p 62 Prop( ) ; supposons que ' ne contient pas de
négations. On a alors que

mod('[p ]) 6= ? ssi mod(' ^ (p ) )) 6= ? .

c’est-à-dire, les deux formules sont equisatisfaisables.

Démonstration. Soit v d’abord une valuation telle que v('[p ]) = 1. On peut étendre cette
valuation à p, en définissant v(p) = v( ), et on aura alors v(' ^ (p ) )) = 1.
Par contre, considérons un modèle v de ' ^ p ) est un modèle de ' tel que v(p)  v( ). Par
induction sur ', en considérant que la négation n’apparaît pas dans ', on trouve que 1 = v(') 
v('[p ]).

Exercice 2.57. Montrez que l’hypothèse que la négation n’apparaît pas dans ' est nécessaire.

Exercice 2.58. Montrez que les deux formules '[p ] et ' ^ (p ) ) ne sont pas équivalentes.
2.5 Le problème SAT 21

Exemple 2.59. Considerez la formule

n
_
pi,0 ^ pi,1 . (2.1)
i=1

L’algorithme de mise en forme normale conjonctive construit la formule

^
p1,f (1) _ p2,f (2) _ . . . _ pn,f (n) .
f :[n]!2

Dans cet exemple le nombre de clauses produites a taille exponentielle par rapport au nombre de
clauses originaires.
La Proposition 2.56 montre que la formule (2.1) est equisatisfaisable avec la formule
n
^
(q1 _ . . . _ qn ) ^ (¬qi _ pi,0 ) ^ (¬qi _ pi,1 ) ,
i=1

une formule en FNC, avec un nombre de clauses de taille linéaire par rapport au nombre de clauses
originaires.
La Proposition 2.56 suggère donc une méthode de mise en forme clausale, préservant la sa-
tisfaisabilité, qui accélère le calcul de la forme clausale. La méthode s’applique si nous sommes
intéressés seulement à l’existence d’un modèle, et non pas à énumérer tous les modèles. Parmi les
défauts de la méthode, le fait qu’il introduit des nouveaux symboles propositionnels, ce qui alourdi
évidemment les calculs de recherche d’un modèle.

2.5 Le problème SAT

2.5.1 Définition du problème
Définition 2.60 (Problème SAT). Le problème SAT est le problème de décision qui consiste à
déterminer si ' 2 Fcp donnée en entrée admet, ou non, un modèle.
Le plus souvent, on suppose que la formule ' en entrée est en forme normale conjonctive.
La plupart des algorithmes de résolution de SAT ne se contentent pas de répondre par oui ou
par non, il peuvent fournir aussi un modèle, ou même l’ensemble des modèles.
Exemple 2.61. Donnée : Une formule booléenne mise sous forme FNC :

' = (¬x1 _ x2 _ x3 ) ^ (x1 _ x2 ) ^ (¬x2 _ x3 ) ^ (¬x3 _ ¬x1 ) .

Question : Est-ce que la formule ' admet au moins un modèle ?

Réponse : Pour cet exemple, la réponse est oui : la valuation v(x1 ) = 0, v(x2 ) = 1, v(x3 ) = 1
satisfait la formule ', c’est-à-dire v 2 mod(').

2.5.2 Un problème NP-complet

Théorème 2.62. Le problème SAT est décidable.
Démonstration. Algorithme : Etant donné une formule ' ayant n variables propositionnelles.
Calculer les 2n valuations possibles. Pour chacune d’entre-elles, calculer la valeur de vérité de '.
Si au moins une est vraie, alors ' est satisfaisable.
Il existe des algorithmes plus performants, mais ces améliorations ne changent pas fondamen-
talement la difficulté du problème. On est devant la situation suivante. Étant donnée une formule
', on se demande si ' admet un modèle ou non, i.e., s’il existe des valeurs de vérité attribuables
aux variables propositionnelles qui satisferait ' :
— une recherche exhaustive comme dans l’algorithme précédent peut demander jusqu’à 2n vé-
rifications si ' possède n variables propositionnelles. Cette démarche est dite déterministe,
mais son temps de calcul est exponentiel.
22 Chapitre 2. Calcul propositionnel

— d’un autre côté, si ' est satisfiable, il suffit d’une vérification à faire, à savoir tester précisé-
ment la configuration qui satisfait '. Cette vérification demande un simple calcul booléen,
qui se fait en temps polynomial (essentiellement linéaire en fait). Le temps de calcul cesse
donc d’être exponentiel, à condition de savoir quelle configuration tester. Celle-ci pourrait
par exemple être donnée par un être omniscient auquel on ne ferait pas totalement confiance.
Une telle démarche est dite non déterministe.
La question de la satisfiabilité de ', ainsi que tous les problèmes qui se résolvent suivant
la méthode que nous venons d’esquisser, sont dits NP (pour polynomial non déterministe). Par
exemple, tester si la formule ' est une tautologie équivaut, par des calculs très simples en temps
polynomial, à tester que sa négation n’est pas satisfaisable (par la Proposition 2.22).
Le problème SAT joue un rôle fondamental en théorie de la complexité, puisqu’on peut montrer
que la découverte d’un algorithme déterministe en temps polynomial pour ce problème permettrait
d’en déduire des algorithmes déterministes en temps polynomial pour tous les problèmes de type
NP (théorème de Cook). On dit que SAT (et donc également le problème de la non-démontrabilité
d’une proposition) est un problème NP-complet.
2.5 Le problème SAT 23

2.5.3 Modélisation - Réduction à SAT

Bien que le problème soit très difficile, nous verrons que nous disposons de logiciels très perfor-
mants permettant de résoudre le problème de satisfaction d’une formule. Il est donc important pour
tout informaticien de savoir profiter de ces outils. L’étape préalable est la suivante : étant donné
un problème qui peut-être apparemment complètement dissocié de la logique, réduire la résolution
de ce problème à la satisfaction d’une formule du calcul propositionnel. Il est bien sûr nécessaire
que la réduction elle-même soit réalisable en un temps raisonnable (en temps polynomial).

2.5.3.1 Comment modéliser

La plupart du temps, les problèmes sont énoncés en français (dans un fragment du français plus
ou moins ambigu). La première étape est d’identifier les propositions atomiques d’un énoncé,
il s’agit des plus petites briques de l’énoncé qui soient indécomposables et qui peuvent prendre la
valeur vraie ou faux.
Il faut ensuite construire une formule traduisant les énoncés à partir des propositions, en utili-
sant les connecteurs booléens. On utilise pour cela la table de correspondance suivante
et, mais ^
ou _
ne pas, non ¬
il n’est pas vrai que ¬
si p alors q, q seulement si p p ) q
p si et seulement si q p,q

Exemple 2.63 (suite).

Si et seulement si : Considérons l’énoncé

« Le triangle est équilatéral si, et seulement si, il a trois coté égaux. »

et posons :
— trois : le triangle a trois côtés égaux
— equi : le triangle est équilatéral
L’enoncé se traduit par trois , equi. En effet, décomposons l’énoncé :
— « Le triangle est équilatéral si il a trois coté égaux » se traduit par trois ) equi.
— « Le triangle est équilatéral seulement si il a trois coté égaux » signifie que si le triangle est
équilatéral, alors il a forcément trois cotés égaux et se traduit donc par equi ) trois.
On a donc trois ) equi ^ equi ) trois, ce qui est équivalent à equi , trois.

Implication versus équivalence Il est d’usage, lors de la définition de concepts mathématiques,

d’utiliser "si" à la place de "si et seulement si". Par exemple la définition du triangle équilatéral a
plus souvent la forme suivante :

« Un triangle est équilatéral s’il a trois coté égaux. »

Pourtant il faut entendre un "si et seulement si". Il s’agit d’une convention à laquelle vous devez
vous habituer.

Condition nécessaire et suffisante : Cette expression est une autre version du "si et seulement
si". Posons :
— note : avoir une bonne note
— travail : travailler
et considérons l’énoncé :

« Pour avoir une bonne note, il faut et il suffit de travailler »

ou de façon équivalente :

« Pour avoir une bonne note, il est nécessaire et suffisant de travailler »

24 Chapitre 2. Calcul propositionnel

Décomposons l’énoncé :
— P1 = « Pour avoir une bonne note il faut travailler » signifie qu’il faut nécessairement
travailler pour avoir une bonne note. On a donc la table suivante :
note travail P1
1 1 1
1 0 0
0 0 1
0 1 1
Donc P1 ⌘ note ) travail.
— P2 = « Pour avoir une bonne note, il suffit de travailler » signifie que si on travaille, on a
une bonne note :
note travail P1
1 1 1
1 0 1
0 0 1
0 1 0
Donc P2 ⌘ travail ) note.

2.5.3.2 Formalisation du problème du Sudoku pour la réduction à SAT

Une grille de Sudoku est composée de n = `2 cases, et cette grille est elle-même divisée en `
sous-grilles. Généralement, on prend n = 9 et ` = 3). Au départ certaines cases sont remplies par
des chiffres et d’autres sont vides. Le but du jeu est de remplir les cases vides en respectant les
règles suivantes :
— On ne doit pas avoir deux chiffres identiques sur une même ligne ;
— On ne doit pas avoir deux chiffres identiques sur une même colonne ;
— Il ne doit pas y avoir deux chiffres identiques dans l’une des sous-grilles de taille ` ⇤ `.

Pour être un Sudoku, la grille doit accepter une et une seule solution.

Formalisation. Pour représenter le problème sous forme de problème SAT, nous avons besoin
de beaucoup de variables propositionnelles. En effet il faut n3 variables Vxyz avec x, y et z in [1, n].
La variable Vxyz sera vraie si et seulement si la case (x, y) contient la valeur z. Par exemple, si V135
est vraie, alors la case (1, 3) contient 5. Si on prend n = 4, il faudra 64 variables, pour n = 9 il en
faut 729. Voici la formulation des règles de remplissage d’un Sudoku.

« Chaque case contient un et un seul chiffre » : pour tout i 2 [1, n], pour tout j 2 [1, n], il
existe k 2 [1, n] tel que la case (i, j) contient k et pour tout k 0 6= k dans [1, k] : la case (i, j)
ne contient pas k 0 .
^ ^ _ ^
A= ( Vijk ^ ¬Vi,j,k0 )
i2[1,n] j2[1,n] k2[1,n] 0
k 2 [1, k]
k0 6= k
2.5 Le problème SAT 25

« On ne doit pas avoir deux chiffres identiques sur une même colonne » : pour toute colonne
i 2 [1, n], pour toutes lignes j 6= j 0 dans [1, n], pour toute valeur k 2 [1, n] : si la case (i, j)
contient k, alors la case (i, j 0 ) ne contient pas k.
^ ^ ^ ^
B= (Vi,j,k ) ¬Vi,j 0 ,k )
i2[1,n] j2[1,n] j 0 2 [1, n] k2[1,n]
j 0 6= j

« On ne doit pas avoir deux chiffres identiques sur une même ligne » : pour toute ligne
j 2 [1, n], pour toutes colonnes i 6= i0 dans [1, n], pour toute valeur k 2 [1, n] : si la case (i, j)
contient k, alors la case (i0 , j) ne contient pas k.
^ ^ ^ ^
C= (Vi,j,k ) ¬Vi0 ,j,k )
j2[1,n] i2[1,n] i0 2 [1, n] k2[1,n]
i0 6= i

« On ne doit pas y avoir deux chiffres identiques dans l’une des sous-grilles de taille ` ⇤ ` » :
pour tous x, x0 2 [1, `],
^ ^ ^ ^
D= (Vi,j,k ) ¬Vi0 ,j 0 ,k )
x,y2[0,` 1] i, i0 2 [1 + `x, ` + `x] j, j 0 2 [1 + `y, ` + `y] k2[1,n]
i 6= i0 j 6= j 0

Pour assurer qu’une grille donnée est un Sudoku, il faut indiquer les chiffres déjà inscrits et
vérifier qu’il y a une et une seule solution au problème. Par exemple, pour la grille donnée en
exemple, on crée la formule :
E = V1,9,5 ^ V2,9,3 ^ V5,9,7 ^ . . .
On cherche alors les modèles de la formule A ^ B ^ C ^ D ^ E. Si il n’y a qu’un seul modèle, alors
la grille est un Sudoku dont la solution est donnée par ce modèle.

2.5.4 Algorithmes de résolution de SAT

De nombreux algorithmes ont été proposés pour résoudre SAT, nous en présentons quelques-
uns, en nous focalisant sur le cas où la formule dont il faut décider de la satisfaisabilité est déjà en
forme normale conjonctive.
Nous allons donc présenter ici quelques calculs sur les formules en FNC qui nous utiliserons
dans le cadres de ces algorithmes qui suivent.
Remarque 2.64 (Simplifications). Avant chercher un (ou plusieurs) modèle(s) d’une formule sous
forme clausale, nous pouvons optimiser les calculs qui suivront en appliquant les règles suivantes :
Tiers exclu : Les clauses comportant deux littéraux opposés (par ex. p _ q _ ¬r _ ¬q) sont valides
(par le tiers-exclu) et peuvent donc être supprimées.
Fusion : On peut supprimer les répétitions d’un littéral au sein d’une même clause (par ex. ¬p _
q _ ¬r _ ¬p équivaut à ¬p _ q _ ¬r).
Subsumption : Si, dans une formule clausale, une clause Ci est incluse dans une clause Cj (c’est-
à-dire, tout littéral apparaissant dans Ci apparaît aussi dans Cj , on dit alors que Ci subsume
Cj ), alors la clause Cj peut être supprimée, car la valeur de la conjonction des deux clauses ne
dépend que de la valeur de Ci . Par exemple Ci = p_q_r est incluse dans Cj = p_¬s_t_q_r,
de façon que l’on peut supprimer Ci d’une formule clausale de la forme C1 ^ . . . Ci ^ . . . Cj ^
. . . Cn .
Remarque 2.65 (Substitions simples). Comme la formule est sous forme clausale, le calcul de la
subtitution C[p '] avec ' 2 { ?, > } est donné par une procédure purement syntaxique :
C[p >] : pour substituer p par > dans une formule clausale, il suffit de supprimer toutes les
clauses contenant p et de supprimer ¬p de toutes les clauses contenant ¬p.
C[p ?] : de même, pour substituer p par ? dans une formule clausale, il suffit de supprimer
toutes les clauses contenant ¬p et de supprimer p de toutes les clauses contenant le littéral p.
26 Chapitre 2. Calcul propositionnel

Remarque 2.66. Nous pouvons identifier une formule en forme normale conjonctive ' avec l’en-
semble C des ses clauses. Par exemple, si

' = (¬x1 _ x2 ) ^ (¬x2 _ x3 ) ^ (¬x3 _ x4 ) ^ (¬x1 _ ¬x4 )

(donc ' est en FNC), alors son ensemble de clauses associé est

C' = { ¬x1 _ x2 , ¬x2 _ x3 , ¬x3 _ x4 , ¬x1 _ ¬x4 } .

2.5.4.1 Algorithme de Quine

Nous présentons d’abord la méthode de Quine dans le cas restreint de formules mises au préa-
lable sous forme normale conjonctive, assimilées donc à un ensemble de clauses. La discussion
de la méthode de Quine nous aidera à comprendre plus de près l’algorithme de Davis-Putnam-
Logemann-Loveland.
La méthode ne fait rien d’autre que parcourir l’arbre de toutes les solutions (l’arbre dont les
branches complètes sont les valuations, appelé arbre sémantique dans la preuve du Théorème 2.40).
Chaque fois qu’une variable est affectée à la valeur x 2 { 0, 1 }, le calcul se fait recursivement avec
C[p ?], si x = 0, et avec C[p >], sinon.

Algorithme de Quine
entrée : un ensemble de clauses C
sortie : vrai si C est satisfaisable ou f aux sinon
simplifier l’ensemble de clauses (cf. Remarque 2.64) ;
si C = ? retourner vrai
si C contient la clause ? retourner f aux
choisir le prochain p 2 Prop apparaissant dans une clause
si Quine(C[p ?]) = vrai alors retourner vrai
sinon retourner Quine(C[p >])
Exemple 2.67. Considerons { p1 _ p2 , ¬p1 _ p2 , p3 }. L’algorithme explore l’arbre de Herbrand
selon un parcours en profondeur gauche comme suit :

p1 _ p 2
¬p1 _ p2
p3

p2
p3

?
p3 p3
f aux

?
f aux vrai

Observons dans l’exemple précédent que nous sommes contraintes par l’algorithme de Quine à
essayer d’abord p1 , ensuite p2 , et puis p3 ; de façon similaire, l’algorithme demande d’évaluer un
symbole propositionnel d’abord à faux, et puis à vrai. Cette stratégie nous amène le plus souvent à
des calculs inutiles : par exemple, dans l’exemple précédent, nous construisons des noeuds suite aux
évaluations de p2 et p3 à faux, quand il est tout à fait évident que ces évaluations nous amènerons
à un échec.
2.5 Le problème SAT 27

En général, nous ne sommes pas contraint à suivre un ordre fixé au debut. Nous allons donc
chrecher d’améliorer l’algorithme de Quine pour trouver à la volée un ordre d’exploration des
symboles propositionnels, qui soit optimisé pour l’ensemble des clauses passé en entrée.

2.5.4.2 Algorithme de Davis-Putnam-Logemann-Loveland

L’algorithme DPLL est considéré à ce jour comme l’une des méthodes les plus efficaces parmi
celles permettant de résoudre le problème SAT. Il peut être vu comme un raffinement de la méthode
de Quine ; l’amélioration principale qu’elle apporte est l’utilisation d’heuristiques pour accélérer le
parcours des solutions.

Algorithme DP LL
entrée : un ensemble de clauses C
sortie : vrai si C est satisfaisable ou f aux sinon
simplifier l’ensemble de clauses (cf. Remarque 2.64) ;
si C = ? retourner vrai
si C contient la clause ? retourner f aux
si C contient la clause p retourner DP LL(C[p >])
si C contient la clause ¬p retourner DP LL(C[p ?])
choisir p depuis une clause et b 2 { >, ? },
avec la bonne heuristique !
si DP LL(C[p b]) = vrai alors retourner vrai
sinon retourner DP LL(C[p ¬b])

Heuristiques. Les heuristiques sont très importantes car elles permettent de réduire rapidement
la taille de l’arbre de recherche. Parmi les heuristiques possibles :

Littéraux purs. Choisir les littéraux qui n’apparaissent que positivement (resp. négativement),
et parmi ceux-ci ceux qui sont présents le plus souvent.

Fréquence des variables. Choisir les variables qui apparaissent le plus dans les clauses les plus
courtes.

Littéraux “courts”. Choisir les littéraux apparaissant dans les clauses les plus courtes.

Les heuristiques précédentes peuvent se formaliser en définissant des fonctions qui donnent une
pondération à chaque variable et ensuite à chaque littéral. Par exemple, si on pose

X 1 X 1
rank+ (p, C) = , rank (p, C) = ,
cardC cardC
p2C,C2C ¬p2C,C2C
+
rank(p, C) = rank (p, C) + rank (p, C) ,

nous pouvons choisir une variable qui maximise la fonction rank pour donner un sens à l’heuristique
exprimé en langue française : choisir une variable apparaissant le plus, dans les clauses les plus
courtes. Ensuite nous essayerons le littéral p si rank+ (p) < rank (p), et ¬p sinon.
28 Chapitre 2. Calcul propositionnel

Exemple Considérons l’ensemble de clauses C = {¬x1 _ x2 , ¬x2 _ x3 , ¬x3 _ x4 , ¬x1 _ ¬x4 }.

¬x1 _ x2
¬x2 _ x3
¬x3 _ x4
¬x1 _ ¬x4
x1 = 0 x1 = 1

¬x2 _ x3 x2
¬x3 _ x4 ¬x2 _ x3
heuristique : ¬x3 _ x4
x3 apparait le plus ¬x4
x3 = 0 x3 = 1

¬x2 x4 x2 = 1

x2 = 0 x4 = 1 x3
¬x3 _ x4
¬x4
VRAI VRAI
x3 = 1

x4
FAUX
¬x4

Les modèles de cette formule sont donc les suivants :

x1 x2 x3 x4
0 0 0 0
0 0 0 1
0 0 1 1
0 1 1 1
On remarque dans cet exemple que
— la propagation des clauses unitaires permet dans la branche de droite de ne suivre qu’un
seul chemin
— l’heuristique qui fait choisir x3 plutôt que x2 ou x4 réduit l’exploration
L’exécution est meilleure que si on avait fait une simple exploration de toutes les solutions (Algo-
rithme de Quine).
Par exemple, prenons l’ensemble de clauses
{{p, q, ¬r}, {q, s}, {¬p, q}, {¬r, s}, {p, ¬r}}.
Sans heuristique, on choisit les littéraux par ordre alphabétique.
— Choisir p : T ⇤p = {{q}, {¬r, s}}
— Choisir q : T ⇤p,q = {{¬r, s}}
— Choisir r : T ⇤p,q,r = {{s}}
— Choisir s : T ⇤p,q,r,s = ?
On a donc trouvé un modèle de l’ensemble initial, pour trouver tous les modèles, il faut continuer
le processus.
Si par contre on applique les heuristiques. Choisir q : T ⇤q = {{¬r, s}, {p, ¬r}} Choisir ¬r : T
q,¬r = ? On a donc trouver un modèle de l’ensemble initial, bien entendu si l’on cherche tous les
⇤

modèles le processus doit se poursuivre, mais le calcul demeure plus rapide.

2.5 Le problème SAT 29

2.5.4.3 Algorithmes incomplets

Il existe aussi des semi-algorithmes (ou algorithmes incomplets) très performants, ceux-ci ne
parcourent pas l’ensemble des solutions et peuvent donc ne pas répondre. En général, il ne répondent
pas à la question de l’insatisfaisabilité. Ils ont l’avantage de trouver souvent rapidement un modèle
lorsqu’il existe, mais il n’en trouvent pas toujours (même si la formule est satisfiable). Par contre,
si la formule est non-SAT, on n’obtient aucune réponse.

Algorithme de Hill Climbing (optimisation stochastique) : Au départ, on choisit une

valuation aléatoire et on dispose d’un critère de qualité (par exemple le nombre de clauses non
satisfaites). A chaque étape, on choisit une variable, on inverse la variable si cela améliore le
critère, sinon on l’inverse avec une probabilité faible (pour éviter les optimum locaux).

Algorithmes génétiques : Ces algorithmes sont inspirés de la sélection naturelle. Au départ,

on se donne aléatoirement un certain nombre de valuations qui forme la population initiale, puis
à chaque étape, on fait évoluer la population par brassage génétique en essayant de tendre vers
des modèles de la formule : par croisement des meilleurs individus, par mutation d’individus et
élimination des solutions les plus faibles.

2.5.4.4 Conclusion
Il existe donc de nombreux algorithmes, certains sont des améliorations de ceux présentés ci-
dessus, souvent par des heuristiques par exemple sur l’ordre d’utilisation des règles. Les meilleurs
complexités atteintes pour ces algorithmes oscillent entre O(1.5n ) et O(1.3n )

2.5.5 Sous-classes de SAT

2.5.5.1 2-SAT
Le problème 2-SAT est celui de la satisfaisabilité d’une formule sous forme clausale dont les
clauses sont d’ordre 2 (i.e., chaque clause est une disjonction d’au plus deux littéraux).
Exemple : ' = (p1 _ p2 ) ^ (¬p1 _ p3 ) ^ (¬p2 _ p1 ) ^ (¬p2 _ p3 ) ^ (¬p1 _ ¬p3 ) est sous forme
clausale d’ordre deux.

Problème 2-SAT
entrée : un ensemble de clauses C d’ordre 2
sortie : vrai si C est satisfaisable ou f aux sinon
Contrairement à SAT, ce problème est résolvable en temps polynomial.

Algorithme 2-SAT :
Une clause d’ordre deux `1 _ `2 est équivalente à (¬`1 ) `2 ) ^ (¬`2 ) `1 ). Pour résoudre SAT pour
une formule ' d’ordre 2, on construit le graphe orienté G(') = (S, A) dual (appelé graphe 2-SAT)
selon les deux règles suivantes :
— l’ensemble des sommets est S = {¬p | p 2 Prop(')} [ Prop(') (où Prop(') est l’ensemble
des variables propositionnelles de la formule ' ). C’est l’ensemble des littéraux sur Prop(')
— l’ensemble des arcs est A = {(`1 , `2 ) | ' contient une clause équivalente à `1 ) `2 }.
Chaque clause `1 _ `2 est donc associée à deux arcs (¬`1 , `2 ) et (¬`2 , `1 ).
Alors, la formule ' est insatisfaisable ssi il existe une variable p telle qu’il existe dans G(') un
chemin allant de p à ¬p et un chemin allant de ¬p à p. En effet, cela signifie alors que ' |= (p )
¬p) ^ (¬p ) p) ce qui est équivalent à ?.
Une autre formulation est la suivante : la formule ' est satisfaisable si et seulement si pour
chaque variable propositionnelle p, les sommets p et ¬p du graphe 2-SAT sont dans deux compo-
santes fortement connexes distinctes. (une composante fortement connexe d’un graphe orienté G
est un sous-graphe maximal de G tel que pour toute paire de sommets u et v dans ce sous-graphe,
il existe un chemin de u à v et un chemin de v à u.)
L’algorithme de Tarjan permet de calculer les composantes fortement connexes d’un graphe
orienté en O(|S| + |A|) , donc 2-SAT est bien polynomial.
30 Chapitre 2. Calcul propositionnel

Exemple 2.68. ' = (p1 _ p2 ) ^ (¬p1 _ p3 ) ^ (¬p2 _ p1 ) ^ (¬p2 _ p3 ) ^ (¬p1 _ ¬p3 )

On a :
— (p1 _ p2 ) ⌘ (¬p1 ) p2 ) ^ (¬p2 ) p1 )
— (¬p1 _ p3 ) ⌘ (p1 ) p3 ) ^ (¬p3 ) ¬p1 )
— (¬p2 _ p1 ) ⌘ (p2 ) p1 ) ^ (¬p1 ) ¬p2 )
— (¬p2 _ p3 ) ⌘ (p2 ) p3 ) ^ (¬p3 ) ¬p2 )
— (¬p1 _ ¬p3 ) ⌘ (p1 ) ¬p3 ) ^ (p3 ) ¬p1 )

On construit le graphe G(') = (S, A) :

p1 ¬p1

p2 ¬p2

p3 ¬p3
On remarque qu’il existe un cycle passant par p1 et ¬p1 , donc la formule est insatisfaisable.
Si on considère maintenant la formule '0 = (¬p1 _ p3 ) ^ (¬p2 _ p1 ) ^ (¬p2 _ p3 ) ^ (¬p1 _ ¬p3 ).
Le graphe est alors le suivant :

p1 ¬p1

p2 ¬p2

p3 ¬p3
On voit sur le graphe que '0 |= p1 ) ¬p1 , '0 |= p2 ) ¬p2 et '0 |= p3 ) ¬p3 . Il n’y a donc
qu’un seul modèle : v(p1 ) = v(p2 ) = v(p3 ) = 0.

2.5.5.2 3-SAT

Le problème 3-SAT est lui aussi NP-complet (c’est à dire qu’il est aussi difficile que le problème
SAT). Pour le démontrer, il suffit de prouver que le problème SAT est polynomialement réductible
à 3-SAT : cela signifie que répondre à la question SAT revient à répondre à 3-SAT et que le temps
nécessaire à transformer SAT en 3-SAT est polynomial.
Preuve : On remarque que toute clause 'n = `1 _ `2 _ . . . _ `n avec n 3 peut se mettre sous
la forme :
n = (`1 _ `2 _ q1 ) ^ (`3 _ ¬q1 _ q2 ) ^ . . . ^ (`n 2 _ ¬qn 4 _ qn 3 ) ^ (`n 1 _ `n _ ¬qn 3 ) où les
qi sont de nouveaux symboles propositionnels.
Donc le problème SAT est polynomialement réductible à 3-SAT. On conclut que 3-SAT est
NP-complet.
Tous les problèmes n-SAT avec n supérieur ou égal à 3 sont également des problèmes NP-
complets.
2.5 Le problème SAT 31

2.5.5.3 Horn-SAT
Une clause de Horn est une clause comportant au plus un littéral positif. C’est donc une
disjonction de la forme ¬p1 _ . . . _ ¬pn _ p, où les pi et p sont des variables propositionnelles. Selon
qu’elles comportent ou non un littéral positif (resp. négatif), les clauses de horn sont de l’une des
trois formes suivantes :
(a) ¬p1 _ . . . _ ¬pn _ p avec n > 0 ;
(b) ¬p1 _ . . . _ ¬pn avec n > 0 ;
(c) p ;
(d) ? ;
Le problème Horn-SAT s’énonce de la façon suivante :
Horn-SAT
Entrée : un ensemble C de clauses de Horn
Question : C est-il satisfiable ?
Ce problème est résolvable en temps polynomial.

Algorithme : Il convient d’abord de remarquer les équivalences suivantes :

— ¬p1 _ . . . _ ¬pn _ p ⌘ (p1 ^ p2 ^ . . . ^ pn ) ) p (avec n > 0) ;
— ¬p1 _ . . . _ ¬pn ⌘ (p1 ^ p2 ^ . . . ^ pn ) ) ? avec n > 0 ;
Si q est une variable propositionnelle, et C est une clause de Horn, on note C/q la clause de
Horn définie par
— C/q = (p2 ^ . . . ^ pn ) ) p si C = (p1 ^ p2 ^ . . . ^ pn ) ) p, p1 = q et n > 0 ;
— C/q = vrai si C = (p1 ^ p2 ^ . . . ^ pn ) ) p, p = q et n > 0 ;
— C/q = (p2 ^ . . . ^ pn ) si C = (p1 ^ p2 ^ . . . ^ pn ), p1 = q et n > 0 ;
— C/q = p si C = p et p 6= q
— C/q = > si C = q
— C/q = ? si C = ?
Les clauses réduites à une variable propositionnelle sont appelés faits.

Algorithme :
Données : Un ensemble C0 de clauses de Horn
Sortie : C0 est-il satisfaisable ?

C = C0
tant que faits(C) 6= ?
Choisir p 2 faits(C)
C = C/p ;
si ? 2 C alors Retourner "inconsistant"
sinon Retourner "satisfaisable" ;
En effet, tout ensemble de clauses ne contenant pas de faits ni la clause ? est satisfaisable : il
suffit de mettre à 0 toutes les variables apparaissant dans les clauses.

2.5.6 Les SAT-solvers

Puisque le problème SAT est présent dans de nombreux domaines de l’informatique, le déve-
loppement de SAT-solvers efficaces est un des défis majeur de l’informatique. De nouveaux solvers
sont constamment développés pour répondre à des besoins spécifiques. Des concours mondiaux de
SAT-solvers sont d’ailleurs organisés chaque année (voir http://www.satcompetition.org).
On peut citer parmis ces nombreux solvers : zChaff datant de 2001 qui utilise l’agorithme
de Chaff qui est une amélioration de DP, Siege en 2003, MiniSAT en 2005 logiciel open-source,
picoSAT dont les méthodes s’inspirent de l’algorithme de Chaff, SARzilla en 2009 qui a gagné de
nombreux prix.
Enfin remarquons que les solvers modernes exploitent les techniques les plus recentes de l’infor-
matique, comme l’apprentissage, la programmation parallèle exploitant l’architecture multicoeur
des processeurs récents, etc.
32 Chapitre 2. Calcul propositionnel

2.5.7 Applications
2.5.7.1 Vérification d’un circuit logique
On encode le circuit et les entrées/sorties désirées et on teste SAT

2.5.7.2 Satisfaction de contraintes

Les problèmes de satisfaction de contraintes (CSP) sont des problèmes mathématiques où l’on
cherche des états ou des objets satisfaisant un certain nombre de contraintes ou de critères. Ici on
sort un peu du contexte simple de la décidabilité, il ne suffit plus de dire qu’une formule est vraie,
il faut en exhiber un modèle.
Les problèmes d’emploi du temps, de coloration de graphe, ou les sudoku.

Emploi du temps Pour choisir un créneau horaire pour le cours de Logique, on doit respecter
les contraintes suivantes :
— Pas en même temps que les TP de RO du M1 informatique
— Pas avant 10h30 le matin
— Pas en même temps que les autres enseignements de L3 info
— Pas en même temps que les autres enseignements obligatoires de L3 math
— Pas en même temps que tout autre cours en amphi.

2.5.7.3 Diagnostic
Le diagnostic est une discipline de l’intelligence artificielle qui vise le développement d’algo-
rithmes permettant de déterminer si le comportement d’un système est conforme au comportement
espéré. Si il ne l’est pas, il faut être capable de trouver le dysfonctionnement.
Le diagnoser doit déterminer si un système a un comportement défectueux étant donnée l’ob-
servation des entrées et sorties du système et d’observation d’états internes. Le modèle du système
peut être traduit en un ensemble de contraintes (disjonctions) : pour chaque composant S du
système, une variable propositionnelle Ab(S) est créée qui est évaluée à vraie si le composant a
un comportement anormal (Abnormal). Les observations peuvent être également traduites par un
ensemble de disjonctions. L’assignation trouvée par l’algorithme de satisfaisabilité est un diagnostic.
On peut simplifier la modélisation par des formules comme les suivantes :
¬Ab(S) ) Int1 ^ Obs1
Ab(S) ) Int2 ^ Obs2
Les formules se lisent de la manière suivante : si le système n’a pas un comportement anormal,
alors il produira le comportement interne Int1 et le comportement observable Obs1. Dans le cas
d’un comportement anormal, il produira le comportement interne Int2 et les observations Obs2.
Étant données les observations Obs, il faut déterminer si le comportement du système est normal
ou non (¬Ab(S) ou Ab(S) )

2.5.7.4 Planification
La planification est une discipline de l’intelligence artificielle qui vise le développement d’algo-
rithmes pour produire des plans (en d’autre termes, une planification), typiquement pour l’exécu-
tion par un robot ou tout autre agent.
Un planificateur typique manipule trois entrées (toutes codées dans un langage formel qui utilise
des prédicats logiques) :
— une description de l’état initial d’un monde,
— une description d’un but à atteindre et
— un ensemble d’actions possibles (parfois appelés opérateurs)
Chaque action spécifie généralement des préconditions qui doivent être présentes dans l’état
actuel pour qu’elle puisse être appliquée, et des postconditions (effets sur l’état actuel). Le problème
de planification classique consiste à trouver une séquence d’actions menant d’un état du système à
un ensemble d’états. Par exemple, voici un problème de planification simple. On dispose de boites
sur une tables, dans une configuration initiale, et on souhaite obtenir une nouvelle configuration
2.5 Le problème SAT 33

(par exemple passer de conf 1 de la figure à a conf 2). La seule action possible est de déplacer une
boite non recouverte par une autre sur la table ou sur une autre boite.

A B

C B C

table table

configuration 1 configuration 2

2.5.7.5 Model checking

Le Model Checking désigne une famille de techniques de vérification automatique des systèmes
dynamiques (souvent d’origine informatique ou électronique). Il s’agit de vérifier algorithmiquement
si un modèle donné, le système lui-même ou une abstraction du système, satisfait une spécification,
souvent formulée en termes de logique temporelle.
Représentation formelle : M |=? '
— M : (modèle du) programme sous observation
— ' : propriété à vérifier
— pré-requis : sémantique (opérationnelle), langage de spécification
Exemple : voici la modélisation à partir d’une machine à état, d’une machine à café très sim-
plifiée.

cette machine est le modèle M, sur lequel on veut vérifier des propriétés ' (exprimées par des
formules de logique) telles que "on obtient un café seulement si on paie 2 euros".
Un exemple de model checker : POEM est un model checker développé au LIF par Peter Niebert
qui utilise un SAT-solver pour finaliser ses calculs.

2.5.7.6 Cryptographie
La complexité du problème SAT est une composante essentielle de la sécurité de tout système
de cryptographie.
Par exemple une fonction de hachage sécurisée constitue une boîte noire pouvant être formulée
en un temps et un espace fini sous la forme d’une conjonction de clauses normales, dont les variables
booléennes correspondent directement aux valeurs possibles des données d’entrée de la fonction de
hachage, et chacun des bits de résultat devra répondre à un test booléen d’égalité avec les bits de
données d’un bloc de données d’entrées quelconque. Les fonctions de hachages sécurisées servent
notamment dans des systèmes d’authentification (connaissance de données secrètes d’entrée ayant
servi à produire la valeur de hachage) et de signature (contre toute altération ou falsification "facile"
des données d’entrée, qui sont connues en même temps que la fonction de hachage elle-même et de
son résultat).
34 Chapitre 2. Calcul propositionnel

2.5.7.7 Bio-informatique
Certains problèmes de traitement du génome se modélisent par des formules propositionnellse
et sont résolus à l’aide de SAT-solvers.

2.5.8 Sur la modélisation

Tous les applications citées ci-dessus ont un point commun : partant d’un problème qui semble
complètement éloigné de la logique, on obtient une solution à ce problème en résolvant le problème
SAT. La phase important de ce travail est donc la modélisation, qui permet par abstraction d’un
objet concret d’obtenir un modèle représentant son fonctionnement et/ou ses propriétés. Dans le
cas cas qui nous intéresse, le modèle est une formule du calcul propositionnel.
Ce mécanisme est très puissant, il permet de résoudre des problèmes très concrets, d’ingénierie
par exemple, en utilisant des résultats théoriques existant sur des objets mathématiques.