Informatique et mathématiques de l'ingénieur

Une machine ne raisonne pas, elle cherche. Poser une question à un solveur SAT consiste à la traduire en une formule de variables valant vrai ou faux, puis à demander : « existe-t-il une façon de les régler qui rende tout vrai à la fois ? » Cette question a l'air pauvre, et elle est en réalité l'une des plus riches de l'informatique : planifier un emploi du temps, vérifier un circuit, casser un protocole, colorer une carte s'y ramènent tous. Ce chapitre pose le langage, la sémantique, et le problème lui-même.

Des variables qui valent vrai ou faux

Variable propositionnelle

Une variable propositionnelle est un symbole qui ne peut prendre que deux valeurs : vrai, noté $1$ , ou faux, noté $0$ .

Elle représente une affirmation indivisible, dont on ne cherche pas à analyser le contenu : « la machine A est allumée », « la tâche 3 est planifiée le lundi », « le fil 7 porte un signal haut ».

C'est une restriction sévère, et c'est elle qui rend tout le reste possible. On ne peut pas écrire « pour tout serveur $s$  », ni « le nombre de tâches est inférieur à 5 » : la logique propositionnelle ne connaît ni quantificateur, ni entier, ni fonction. Elle ne connaît que des interrupteurs.

Nommer les variables avant de les écrire

La faute qui coûte le plus cher n'est pas dans la formule, elle est en amont : une variable dont le sens n'a pas été fixé en français. Avant de poser quoi que ce soit, écrire une ligne de la forme « 

x_{i,j}

vaut 1 si et seulement si la tâche

i

est affectée à la machine

j

 ».
Sans cette ligne, une formule juste et une formule fausse se ressemblent, et rien ne permet de trancher.

Les connecteurs

Les cinq connecteurs

Nom	Notation	Se lit	Vaut 1 quand
négation	$\neg x$	non $x$	$x$ vaut 0
conjonction	$x \wedge y$	$x$ et $y$	les deux valent 1
disjonction	$x \vee y$	$x$ ou $y$	au moins un des deux vaut 1
implication	$x \rightarrow y$	si $x$ alors $y$	$x$ vaut 0, ou $y$ vaut 1
équivalence	$x \leftrightarrow y$	$x$ si et seulement si $y$	les deux ont la même valeur

Le « ou » de la logique n'est pas celui du français

« Fromage ou dessert » exclut d'en prendre deux. Le

\vee

de la logique, lui, est inclusif :

1 \vee 1 = 1

. Il correspond au « et/ou » administratif.
Le ou exclusif existe, il se note

\oplus

et vaut 1 quand exactement un des deux opérandes vaut 1. Il s'écrit

(x \vee y) \wedge \neg(x \wedge y)

, et il faudra s'en souvenir : c'est lui qui rend les formules issues de la cryptographie si difficiles à résoudre.

L'implication est vraie quand la prémisse est fausse

0 \rightarrow 1

0 \rightarrow 0

valent toutes les deux 1. « Si la machine tombe en panne, alors l'alarme sonne » n'est violée que dans un seul cas : la machine tombe en panne et l'alarme ne sonne pas.
Une implication dont la prémisse ne se produit jamais est donc vraie, et sans intérêt. C'est ce qu'on appelle une implication vide, et c'est une source classique de contraintes qui ne contraignent rien.

La règle à retenir sans hésiter, parce que tout le chapitre 2 en dépend :

$x \rightarrow y \quad \text{équivaut à} \quad \neg x \vee y$

Priorité et parenthèses

Du plus fort au plus faible : $\neg$ , puis $\wedge$ , puis $\vee$ , puis $\rightarrow$ , puis $\leftrightarrow$ .

Une formule est en réalité un arbre, et les parenthèses ne servent qu'à dire de quel arbre il s'agit. La chaîne $\neg x \vee y \wedge z$ en désigne un seul, celui-ci.

Graphe orienté5 sommets, 4 arêtes

L'arbre de ¬x ∨ y ∧ z, avec les priorités usuelles. Le ∧ étant plus fort que le ∨, il se noue plus bas dans l'arbre : la formule se lit (¬x) ∨ (y ∧ z).

Voici l'autre lecture, celle que beaucoup font spontanément, et qui exige des parenthèses pour être écrite.

Graphe orienté5 sommets, 4 arêtes

L'arbre de (¬x ∨ y) ∧ z. La chaîne de symboles est presque la même, l'arbre ne l'est pas, et les deux formules n'ont pas les mêmes modèles : avec x = 1, y = 0, z = 0, la première vaut 0 et la seconde vaut 0 aussi ; mais avec x = 0, y = 0, z = 0, la première vaut 1 et la seconde 0.

Parenthéser plutôt que compter sur la priorité

Les conventions de priorité varient d'un ouvrage et d'un solveur à l'autre, en particulier pour l'implication, qui est parfois associative à droite et parfois interdite sans parenthèses. Une formule ambiguë est une formule fausse la moitié du temps.
Dans le doute, parenthéser. Cela n'a jamais coûté un point à personne.

Évaluer une formule

Affectation et satisfaction

Une affectation attribue une valeur, 0 ou 1, à chaque variable. Une affectation partielle n'en fixe qu'une partie.

L'affectation satisfait la formule si celle-ci vaut 1 sous cette affectation. On dit alors que l'affectation est un modèle de la formule.

Évaluer

(x \vee \neg y) \wedge (\neg x \vee z)

sous

x = 1, y = 1, z = 0

Première clause. $x$ vaut 1, donc $x \vee \neg y$ vaut 1. La valeur de $y$ ne change plus rien : dès qu'un membre d'une disjonction est vrai, le reste est sans effet.
Seconde clause. $\neg x$ vaut 0 et $z$ vaut 0, donc $\neg x \vee z$ vaut 0.
La conjonction. $1 \wedge 0 = 0$ . L'affectation ne satisfait pas la formule.

Une seule clause fausse suffit à tout faire tomber : c'est la propriété qui rend la conjonction si commode à vérifier, et si difficile à satisfaire.

Le bloc ci-dessous permet de manipuler cette formule directement. Chaque variable a trois positions : 0, 1, et ? tant qu'elle n'est pas décidée.

2 clausesen attente

c1(x∨¬y)
c2(¬x∨z)

xyz

vert = décidé, orange = déduit par propagation.

Aucune variable n'est affectée : toutes les clauses attendent.

La formule (x ∨ ¬y) ∧ (¬x ∨ z), sous une affectation qu'on peut changer. Une clause devient verte dès qu'un de ses littéraux est vrai, et rouge quand ils sont tous faux.

Deux observations à faire sur la figure

Poser

x = 1

suffit à satisfaire la première clause, et la valeur de

y

n'y change plus rien : une clause satisfaite est éteinte, le solveur n'a plus à s'en occuper.
Poser

x = 1

et laisser

z

en position ? rend la seconde clause orange : il ne lui reste qu'un littéral non décidé, donc ce littéral n'a plus le choix. C'est la propagation unitaire, le mécanisme le plus rentable de tout le domaine, et elle occupera un chapitre entier.
Le bouton propager applique cette déduction. La valeur obtenue s'affiche en orange et non en vert, parce qu'elle n'a pas été choisie : elle a été calculée.

Table de vérité

Une table de vérité énumère les $2^n$ affectations possibles de $n$ variables et donne la valeur de la formule pour chacune.

La table de

(x \rightarrow y) \wedge (y \rightarrow z)

$x$	$y$	$z$	$x \rightarrow y$	$y \rightarrow z$	formule
0	0	0	1	1	1
0	0	1	1	1	1
0	1	0	1	0	0
0	1	1	1	1	1
1	0	0	0	1	0
1	0	1	0	1	0
1	1	0	1	0	0
1	1	1	1	1	1

Quatre modèles sur huit affectations. Noter la ligne $x = 1, y = 0$  : la première implication est violée, et il devient inutile de regarder $z$ .

Pourquoi la table de vérité n'est pas une méthode

Elle est parfaitement correcte et parfaitement inutilisable. Le tableau ci-dessous suppose une machine qui traiterait un milliard de lignes par seconde, ce qu'aucune ne fait.
Tout le domaine consiste à répondre à la question que pose la table, sans jamais la construire. C'est le programme des chapitres suivants.

variables	lignes de la table	temps à un milliard de lignes par seconde
20	1 million	instantané
40	$10^{12}$	18 minutes
60	$10^{18}$	36 ans
80	$10^{24}$	38 millions d'années
300	$10^{90}$	plus que l'âge de l'univers, par un facteur inconcevable

L'ordre de grandeur à garder

Chaque variable ajoutée double le travail. Vingt variables de plus multiplient donc le temps par un million.
Une instance industrielle en compte des centaines de milliers. Aucune énumération, aussi rapide soit-elle, n'en viendra jamais à bout : ce n'est pas une question de matériel, et il n'y aura pas de machine assez grande.

Satisfiable, valide, insatisfiable

Les trois statuts d'une formule

Une formule est satisfiable s'il existe au moins une affectation qui la rend vraie.

Elle est valide, ou tautologie, si toutes les affectations la rendent vraie.

Elle est insatisfiable, ou contradictoire, si aucune ne la rend vraie.

Ces trois notions ne sont pas indépendantes, et le lien entre elles est le fondement de toute la vérification par SAT.

Les deux cas extrêmes valent la peine d'être manipulés une fois. La formule de gauche est satisfaite quoi qu'on fasse ; celle de droite ne l'est jamais.

1 clauseen attente

c1(x∨¬x)

vert = décidé, orange = déduit par propagation.

Aucune variable n'est affectée : toutes les clauses attendent.

La formule (x ∨ ¬x), une tautologie. Elle reste verte dans les deux positions de x, et n'est jamais unitaire : elle ne contraint rien, et un solveur peut la supprimer sans rien changer.

2 clausesunitaire

c1(x)⇒ x = 1
c2(¬x)⇒ x = 0

vert = décidé, orange = déduit par propagation.

Deux clauses unitaires réclament des valeurs opposées pour x. Le conflit est déjà là, la prochaine propagation le révélera.

La formule (x) ∧ (¬x), insatisfiable. Les deux clauses sont unitaires et réclament des valeurs opposées : le conflit est annoncé avant même qu'on ait décidé quoi que ce soit.

Le passage par la négation

F

est valide si et seulement si

\neg F

est insatisfiable.
En effet, dire que

F

est vraie partout, c'est dire que

\neg F

n'est vraie nulle part. Les deux phrases décrivent la même situation.
Conséquence pratique, et elle est considérable : un outil qui sait seulement répondre « satisfiable ou non » sait aussi démontrer des théorèmes. Pour prouver que

F

est toujours vraie, il suffit de lui soumettre

\neg F

et d'obtenir « insatisfiable ».

Prouver une équivalence avec un outil qui ne sait rien prouver

Vérifier que $x \rightarrow y$ et $\neg y \rightarrow \neg x$ sont équivalentes, c'est-à-dire que la formule

$(x \rightarrow y) \leftrightarrow (\neg y \rightarrow \neg x)$

est valide. On soumet donc sa négation au solveur. Celui-ci répond insatisfiable : aucune affectation ne distingue les deux formules, donc elles sont équivalentes. Aucune table n'a été construite, et le raisonnement vaudrait à l'identique pour deux circuits de dix mille portes.

C'est exactement ainsi que l'industrie vérifie qu'une optimisation de circuit n'a rien changé au comportement : on demande au solveur de trouver une entrée où l'ancien et le nouveau diffèrent. S'il n'en trouve pas, ils sont identiques.

Conséquence logique

C'est la question que l'on pose réellement à un solveur dans l'industrie, et elle mérite son nom.

Conséquence logique

$G$ est conséquence logique de $F$ , noté $F \models G$ , si tout modèle de $F$ est aussi un modèle de $G$ .

Autrement dit : dès que $F$ est vraie, $G$ l'est nécessairement.

Ce que cela recouvre concrètement

$F$ décrit un système : les règles d'un protocole, le câblage d'un circuit, les contraintes d'un ordonnanceur.

$G$ décrit une propriété qu'on voudrait garantie : « deux processus ne sont jamais en section critique en même temps », « la sortie du circuit optimisé vaut celle du circuit d'origine », « aucune tâche ne démarre avant sa dépendance ».

Demander $F \models G$ , c'est demander : le système garantit-il la propriété. C'est la question de la vérification, et c'est celle qu'un solveur SAT sait traiter.

Comment un solveur y répond

Il n'existe pas de bouton « conséquence logique ». On la ramène à une insatisfiabilité, exactement comme la validité.

F \models G

si et seulement si

F \wedge \neg G

est insatisfiable.
La raison tient en une phrase : un modèle de

F \wedge \neg G

serait un cas où le système fonctionne et où la propriété est violée, c'est-à-dire un contre-exemple. S'il n'en existe aucun, la propriété est garantie.

Le solveur ne dit pas seulement oui ou non

C'est ce qui rend la méthode utilisable en pratique. Si le solveur répond insatisfiable, la propriété est démontrée pour toutes les entrées possibles, et il n'y en avait pas besoin d'énumérer une seule.
S'il répond satisfiable, il rend un modèle, et ce modèle est le contre-exemple : les valeurs exactes des entrées qui font échouer le système. Un ingénieur reçoit donc, au lieu d'un verdict, le scénario à corriger.
C'est la différence entre « ce circuit a un bug » et « avec ces douze entrées à ces valeurs, il sort 0 au lieu de 1 ».

Vérifier la transitivité de l'implication

Question : de $(x \rightarrow y)$ et $(y \rightarrow z)$ , peut-on conclure $(x \rightarrow z)$  ?

Écrire la négation de ce qu'on veut prouver. $\neg(x \rightarrow z)$ vaut $x \wedge \neg z$ , ce qui donne deux clauses unitaires.

Rassembler le tout : $(\neg x \vee y) \wedge (\neg y \vee z) \wedge (x) \wedge (\neg z)$ .

Laisser la propagation faire le travail, sur la figure ci-dessous. La clause $(x)$ force $x = 1$ , ce qui rend $(\neg x \vee y)$ unitaire et force $y = 1$ , ce qui rend $(\neg y \vee z)$ unitaire et force $z = 1$ . Mais la clause $(\neg z)$ exigeait $z = 0$ .

Conflit, donc insatisfiable, donc la conséquence est démontrée. Et remarquer qu'aucune énumération n'a eu lieu : trois propagations ont suffi.

4 clausesunitaireen attente

c1(¬x∨y)
c2(¬y∨z)
c3(x)⇒ x = 1
c4(¬z)⇒ z = 0

xyz

vert = décidé, orange = déduit par propagation.

Propagation unitaire : x = 1, z = 0. Ces valeurs ne sont pas des choix, elles sont imposées.

La négation de « (x → y) et (y → z) entraînent (x → z) ». Propager jusqu'au bout mène à un conflit : aucun contre-exemple n'existe, donc l'implication est bien transitive. C'est une démonstration, faite par un outil qui ne sait que chercher.

Le problème SAT

SAT

Donnée : une formule propositionnelle $F$ .

Question : $F$ est-elle satisfiable ?

Un solveur moderne ne se contente pas de répondre par oui ou par non, et c'est cette double sortie qui le rend utilisable :

s'il répond SAT, il fournit un modèle, une affectation complète que l'on peut vérifier soi-même en temps linéaire ;
s'il répond UNSAT, il peut fournir une preuve de réfutation : un fichier texte contenant une suite de déductions, chacune tirée des précédentes, qui aboutit à une contradiction manifeste. Un programme indépendant, de quelques centaines de lignes, relit cette suite et confirme que chaque pas est licite. C'est ce qui permet de faire confiance au verdict d'un solveur de cent mille lignes sans avoir à lui faire confiance.

Vérifier est facile, chercher ne l'est pas

Étant donné une affectation, contrôler qu'elle satisfait une formule de

m

clauses demande de parcourir la formule une fois : c'est immédiat, même sur des millions de clauses.
Trouver cette affectation, en revanche, n'a aucune méthode connue qui échappe à une explosion dans le pire cas. Cet écart entre vérifier et trouver est précisément ce que formalise la classe NP, et SAT en est le représentant historique. Le chapitre 4 y revient.

Traduire une contrainte

C'est le geste qui décide de tout, et il s'apprend en le faisant. Trois traductions à connaître par cœur, parce qu'elles reviennent dans toutes les modélisations.

Trois patrons de traduction

Au moins un parmi $x_1, \ldots, x_n$  : une seule clause, $x_1 \vee x_2 \vee \cdots \vee x_n$ .

Au plus un parmi $x_1, \ldots, x_n$  : toutes les paires s'excluent, soit $\neg x_i \vee \neg x_j$ pour chaque paire $i < j$ .

Sur quatre variables $a, b, c, d$ , cela donne six clauses, une par paire :

$(\neg a \vee \neg b)$ , $(\neg a \vee \neg c)$ , $(\neg a \vee \neg d)$ , $(\neg b \vee \neg c)$ , $(\neg b \vee \neg d)$ , $(\neg c \vee \neg d)$ .

En général il y a $\frac{n(n-1)}{2}$ paires, donc autant de clauses.

Exactement un : les deux ensembles de clauses précédents, réunis.

Trois créneaux, une réunion

Une réunion doit se tenir à exactement un des trois créneaux $A$ , $B$ , $C$ . Trois variables, $a$ , $b$ , $c$ , valant 1 si le créneau est retenu.

Au moins un : $(a \vee b \vee c)$ .
Au plus un : $(\neg a \vee \neg b) \wedge (\neg a \vee \neg c) \wedge (\neg b \vee \neg c)$ .

Voici les quatre clauses ensemble. Choisir un seul créneau satisfait tout ; en choisir deux fait apparaître une clause rouge.

4 clausessatisfaiteunitaireen attente

c1(a∨b∨c)
c2(¬a∨¬b)⇒ b = 0
c3(¬a∨¬c)⇒ c = 0
c4(¬b∨¬c)

abc

vert = décidé, orange = déduit par propagation.

Propagation unitaire : b = 0, c = 0. Ces valeurs ne sont pas des choix, elles sont imposées.

« Exactement un créneau parmi trois ». Poser a = 1 satisfait la première clause et rend les deux suivantes unitaires : elles imposent b = 0 et c = 0, sans qu'aucun choix supplémentaire soit nécessaire.

Toujours vérifier une traduction sur deux cas

Un cas qui doit passer, et un cas qui doit échouer. Ici :

a = 1, b = 0, c = 0

doit satisfaire la formule, et

a = 1, b = 1, c = 0

doit la violer.
Une traduction qui oublie la moitié « au plus un » laisse passer les deux, et le solveur rendra une solution parfaitement valide pour la formule et parfaitement absurde pour le problème. Le solveur ne se trompe jamais ; la traduction, si.

Équivalence et équisatisfiabilité

Deux relations qu'il ne faut pas confondre

$F$ et $G$ sont équivalentes si elles ont exactement les mêmes modèles. On note $F \equiv G$ .

Elles sont équisatisfiables si elles sont satisfiables toutes les deux, ou insatisfiables toutes les deux. Rien de plus.

L'équivalence est beaucoup plus forte. Deux formules équisatisfiables peuvent porter sur des variables différentes et n'avoir aucun modèle en commun.

Voici une formule dont il vaut la peine de parcourir les quatre affectations, l'une après l'autre.

2 clausesen attente

c1(a∨b)
c2(¬a∨¬b)

vert = décidé, orange = déduit par propagation.

Aucune variable n'est affectée : toutes les clauses attendent.

La formule (a ∨ b) ∧ (¬a ∨ ¬b). Deux affectations sur quatre la satisfont, celles où a et b diffèrent : c'est une écriture du ou exclusif. Poser les deux à 1, ou les deux à 0, fait apparaître une clause rouge.

Pourquoi cette distinction va servir immédiatement

Le chapitre suivant transforme n'importe quelle formule en forme normale conjonctive. La transformation naïve préserve l'équivalence, mais peut faire exploser la taille de la formule.
Celle qu'on emploie en pratique introduit des variables nouvelles, qui nomment des morceaux de la formule de départ. Elle ne peut donc pas préserver l'équivalence : les deux formules ne portent même plus sur les mêmes variables. Elle préserve seulement l'équisatisfiabilité.
Et cela suffit, parce que la question posée est « existe-t-il un modèle », pas « lesquels ». Confondre les deux notions revient à croire que cette transformation est fausse. Elle ne l'est pas ; elle répond à une question un peu plus modeste, qui se trouve être exactement la bonne.

Vérification rapideon peut se reprendre

1.« Le menu comprend un café ou un thé » se traduit par la clause (c ∨ t). Qu'autorise cette clause ?

2.La formule (x → y) est-elle satisfaite quand x = 0 et y = 0 ?

3.Un solveur répond SAT sur la modélisation d'un emploi du temps, et la solution rendue place deux cours dans la même salle au même créneau. Que conclure ?

Exercices type

Combien de modèles a la formule

(x \vee y) \wedge (\neg x \vee \neg y)

La première clause exige au moins un vrai, la seconde au plus un vrai. Ensemble : exactement un des deux.

Les modèles sont donc $x = 1, y = 0$ et $x = 0, y = 1$  : deux modèles sur quatre affectations.

Cette formule est d'ailleurs une écriture du ou exclusif : elle vaut exactement $x \oplus y$ .

La formule

(x \rightarrow y) \wedge x \wedge \neg y

est-elle satisfiable ?

Non. La deuxième clause impose $x = 1$ , la troisième impose $y = 0$ . Sous ces deux valeurs, $x \rightarrow y$ vaut $1 \rightarrow 0$ , c'est-à-dire 0.

Aucune des quatre affectations restantes n'a besoin d'être testée : les deux clauses unitaires ont déjà tout décidé, et la première est alors violée. C'est un raisonnement de propagation unitaire, mené à la main.

Traduire : « si le serveur A est actif, alors B ou C doit l'être aussi »

Trois variables : $a$ , $b$ , $c$ , valant 1 si le serveur correspondant est actif.

La phrase s'écrit $a \rightarrow (b \vee c)$ , soit après élimination de l'implication :

$\neg a \vee b \vee c$

Une seule clause. Vérification sur deux cas : avec $a = 1, b = 0, c = 0$ la clause vaut 0, ce qui est bien le cas interdit ; avec $a = 0$ la clause vaut 1 quelles que soient les autres valeurs, ce qui traduit correctement le fait que la contrainte ne dit rien quand A est éteint.

Montrer que

\neg(x \wedge y)

\neg x \vee \neg y

sont équivalentes

C'est l'une des deux lois de De Morgan. Table de vérité :

$x$	$y$	$x \wedge y$	$\neg(x \wedge y)$	$\neg x \vee \neg y$
0	0	0	1	1
0	1	0	1	1
1	0	0	1	1
1	1	1	0	0

Les deux dernières colonnes coïncident sur les quatre lignes, donc les formules sont équivalentes.

L'autre loi s'obtient en échangeant les rôles : $\neg(x \vee y) \equiv \neg x \wedge \neg y$ . Les deux serviront à chaque transformation en forme normale.

Une formule valide peut-elle être insatisfiable ?

Non, à une exception près qui n'existe pas ici : une formule valide est vraie sous toute affectation, et il existe toujours au moins une affectation, puisqu'une formule porte sur un nombre fini de variables. Une formule valide est donc toujours satisfiable.

La réciproque est fausse : $x$ est satisfiable, par $x = 1$ , sans être valide, puisque $x = 0$ la falsifie. Les trois statuts se rangent ainsi : valide implique satisfiable, et insatisfiable est le contraire de satisfiable.

La méthode

Écrire d'abord ce que signifie chaque variable, en français, avant toute formule.
Traduire chaque contrainte de l'énoncé séparément, puis les relier par des $\wedge$ .
Éliminer les implications dès que possible, par $x \rightarrow y \equiv \neg x \vee y$ .
Parenthéser plutôt que se fier à la priorité des connecteurs.
Vérifier la traduction sur deux cas, un qui doit passer et un qui doit échouer.
Passer par la négation pour prouver qu'une formule est valide.
Ne jamais construire une table de vérité au-delà de quatre ou cinq variables : elle sert à comprendre, pas à calculer.

Synthèse

Une variable propositionnelle vaut 1 ou 0, et ne représente rien d'autre qu'une affirmation indivisible.
$x \rightarrow y$ équivaut à $\neg x \vee y$  : c'est la réécriture la plus utilisée du domaine.
Une affectation qui rend la formule vraie est un modèle.
Satisfiable : au moins un modèle. Valide : tous. Insatisfiable : aucun.
$F$ est valide si et seulement si $\neg F$ est insatisfiable : un solveur SAT sait donc démontrer.
$F \models G$ si et seulement si $F \wedge \neg G$ est insatisfiable : un modèle est alors un contre-exemple.
Une formule est un arbre ; les parenthèses disent lequel.
SAT demande si une formule est satisfiable ; le solveur rend un modèle, ou une preuve d'impossibilité.
Vérifier un modèle est immédiat, le trouver n'a aucune méthode connue efficace dans tous les cas.
« Au moins un » est une clause ; « au plus un » est une clause par paire.
Équivalentes : mêmes modèles. Équisatisfiables : même réponse à la question SAT, et rien de plus.

Logique propositionnelle et satisfiabilité

Ce que ce chapitre apporte

Des variables qui valent vrai ou faux

Les connecteurs

Priorité et parenthèses

Évaluer une formule

Table de vérité

Satisfiable, valide, insatisfiable

Conséquence logique

Le problème SAT

Traduire une contrainte

Équivalence et équisatisfiabilité

Exercices type

La méthode

Synthèse