Informatique et mathématiques de l'ingénieur

Un solveur SAT ne lit pas les formules du chapitre précédent. Il ne connaît qu'une seule forme : une conjonction de clauses, chaque clause étant une disjonction de littéraux. Cette uniformité n'est pas une coquetterie de notation, c'est ce qui rend le solveur possible. Reste à y amener n'importe quelle formule, et la méthode évidente, la distributivité, fait exploser la taille. Ce chapitre montre l'explosion, puis la façon dont Tseitin l'évite en payant un prix qui semble d'abord inacceptable : changer de formule.

Le vocabulaire, en trois lignes

Littéral, clause, forme normale conjonctive

Un littéral est une variable ou sa négation : $x$ et $\neg x$ sont deux littéraux, dits opposés.

Une clause est une disjonction de littéraux : $(x \vee \neg y \vee z)$ .

Une formule est en forme normale conjonctive, en abrégé CNF, si elle est une conjonction de clauses.

Deux cas limites qu'il faut avoir vus une fois, parce qu'ils apparaissent au milieu d'un calcul et déroutent :

la clause vide, sans aucun littéral, est fausse. Ce n'est pas une convention arbitraire : une clause exige qu'au moins un de ses littéraux soit vrai, et s'il n'y en a aucun à l'intérieur, il est impossible d'en trouver un. La condition ne peut jamais être remplie. On la note $\square$ ou $\bot$ , et la dériver est exactement ce que cherche une preuve d'insatisfiabilité ;
la formule vide, sans aucune clause, est vraie : rien ne s'oppose à elle.

Littéral pur

Un littéral est pur dans une formule si son opposé n'y apparaît nulle part.

Si $x$ est pur, aucune clause ne contient $\neg x$  : poser $x = 1$ satisfait toutes les clauses où $x$ figure, et n'en gêne aucune autre. On peut donc le faire sans risque, et sans avoir à revenir dessus.

Une seule règle de lecture

Dans une CNF, il faut satisfaire toutes les clauses, et pour chacune il suffit d'un littéral. « Tout » à l'extérieur, « au moins un » à l'intérieur.
D'où l'asymétrie qui gouverne tout le domaine : une seule clause falsifiée condamne l'affectation entière, alors qu'il faut passer en revue toutes les clauses pour se déclarer satisfait. Trouver l'échec est rapide, confirmer le succès est long.

Pourquoi cette forme, et pas une autre

Trois raisons, et la troisième est la vraie.

Elle est uniforme. Une clause est une liste de littéraux ; une formule est une liste de clauses. Aucune structure arborescente à parcourir, aucun cas particulier. Un solveur manipule des tableaux d'entiers.

Elle rend l'échec local. Une clause dont tous les littéraux sont faux suffit à condamner l'affectation, sans regarder le reste.

Elle rend la déduction locale. Une clause dont tous les littéraux sauf un sont faux force ce dernier. C'est la propagation unitaire, et c'est de loin l'opération la plus rentable d'un solveur : elle décide des variables sans jamais parier.

3 clausessatisfaiteunitaire

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

xyz

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

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

Trois clauses. Poser x = 1 rend c2 unitaire, qui impose y = 1 ; c3 est unitaire depuis le début et impose z = 0. Aucune de ces deux valeurs n'est un choix : elles sont déduites.

La propagation ne parie pas

Il faut bien séparer deux gestes que le vocabulaire courant confond.
Décider, c'est choisir une valeur sans y être forcé. C'est un pari, et il faudra peut-être le défaire.
Propager, c'est constater qu'une clause ne laisse plus qu'une possibilité. Ce n'est pas un pari : si l'affectation courante mène à un modèle, cette valeur en fait partie.
Un solveur moderne passe l'essentiel de son temps à propager. Le chapitre 7 chiffrera à quel point.

Ce qu'un solveur jette avant de commencer

Trois situations rendent une clause inutile, et tout solveur les élimine à la lecture du fichier, avant la moindre décision. Les connaître évite d'écrire des clauses qui ne servent à rien, et explique pourquoi le nombre de clauses annoncé par un solveur diffère parfois de celui du fichier.

Les trois simplifications de lecture

Littéral répété. $(x \vee y \vee x)$ vaut $(x \vee y)$ . Une clause est un ensemble de littéraux, pas une liste.

Clause tautologique. Une clause qui contient à la fois $x$ et $\neg x$ est toujours satisfaite : l'un des deux est vrai quoi qu'il arrive. Elle ne contraint rien et se supprime.

Subsomption. Si toute la clause $C$ est contenue dans la clause $D$ , alors $D$ est subsumée : satisfaire $C$ satisfait $D$ automatiquement. On garde la plus courte et l'on jette l'autre.

3 clausesunitaireen attente

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

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

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

Trois clauses dont deux sont inutiles. La première contient x et ¬x : elle reste verte quelle que soit la valeur de x, donc elle ne contraint rien. La deuxième est subsumée par la troisième, plus courte : dès que c3 est satisfaite, c2 l'est aussi. Il ne reste réellement que (x).

Le sens de la subsomption, à ne pas inverser

C'est la clause la plus courte qui est la plus forte, et c'est elle qu'on garde.

(x)

exige davantage que

(x \vee y)

, puisqu'elle interdit plus d'affectations.
Le réflexe contraire est fréquent, parce qu'on associe spontanément « plus long » à « plus contraignant ». En logique propositionnelle c'est l'inverse : ajouter un littéral à une clause l'affaiblit, en lui donnant une façon de plus d'être satisfaite.

La subsomption entre toutes les paires coûte cher

Vérifier que

C

subsume

D

est immédiat ; le faire pour toutes les paires de clauses d'une formule d'un million d'entrées ne l'est pas, puisque cela ferait

10^{12}

comparaisons.
Les solveurs ne cherchent donc pas toutes les subsomptions. Ils en attrapent une partie à la lecture, et d'autres pendant la recherche sur les clauses qu'ils apprennent eux-mêmes. Le chapitre 9 y revient : le prétraitement est un compromis, pas une simplification exhaustive.

Mise en forme normale négative

Première étape de toute transformation : faire descendre les négations jusqu'aux variables.

Les quatre réécritures

$x \rightarrow y \ \equiv\ \neg x \vee y$

$x \leftrightarrow y \ \equiv\ (\neg x \vee y) \wedge (x \vee \neg y)$

$\neg (x \wedge y) \ \equiv\ \neg x \vee \neg y$ et $\neg (x \vee y) \ \equiv\ \neg x \wedge \neg y$ (De Morgan)

$\neg \neg x \ \equiv\ x$

Une formule où toute négation porte directement sur une variable est dite en forme normale négative. Elle n'est pas encore une CNF, mais elle n'a plus que des $\wedge$ et des $\vee$ à réorganiser.

Mettre

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

en forme normale négative

Éliminer l'implication. $(x \wedge y) \rightarrow z$ devient $\neg(x \wedge y) \vee z$ , donc la formule est $\neg\big(\neg(x \wedge y) \vee z\big)$ .

De Morgan sur le $\vee$ . $\neg(A \vee B) \equiv \neg A \wedge \neg B$ , d'où $\neg\neg(x \wedge y) \wedge \neg z$ .

Double négation. $(x \wedge y) \wedge \neg z$ .

Résultat : $x \wedge y \wedge \neg z$ , qui se lit «  $x$ et $y$ sont vrais, et $z$ est faux ». C'est bien la seule façon de violer l'implication de départ, ce qui est un bon contrôle du calcul.

L'équivalence coûte deux fois

Chaque

\leftrightarrow

éliminé duplique la formule, puisqu'il s'écrit comme une conjonction de deux implications portant chacune sur les deux membres.
Sur

A \leftrightarrow (B \leftrightarrow C)

, l'élimination du

\leftrightarrow

extérieur écrit deux fois le morceau

B \leftrightarrow C

, une fois dans chaque implication. Il faudra ensuite éliminer chacune de ces deux copies, et chacune se dédoublera à son tour. Une formule qui empile

k

équivalences en produit ainsi

2^k

copies après réécriture naïve.
C'est la première explosion du chapitre, et Tseitin la traitera comme les autres.

La distributivité, et son explosion

La règle qui transforme une forme normale négative en CNF tient en une ligne :

$A \vee (B \wedge C) \ \equiv\ (A \vee B) \wedge (A \vee C)$

Elle est correcte, et elle préserve l'équivalence. Sur de petites formules, elle est même la bonne méthode.

Un cas où elle fonctionne très bien

$(x \wedge y) \vee z$ devient $(x \vee z) \wedge (y \vee z)$  : deux clauses, aucune variable nouvelle. Il n'y a rien de mieux à faire.

Et un cas où elle est catastrophique

Considérons la formule

$(x_1 \wedge y_1) \vee (x_2 \wedge y_2) \vee \cdots \vee (x_n \wedge y_n)$

Elle compte $2n$ variables et s'écrit en une ligne. Distribuer revient à choisir, dans chaque conjonction, lequel des deux littéraux on garde : il y a $2^n$ façons de choisir, donc $2^n$ clauses, chacune de $n$ littéraux.
Pour $n = 20$ , cela fait $1\,048\,576$ clauses de 20 littéraux, soit une vingtaine de millions de littéraux, pour une formule de départ qui en comptait 40. Pour $n = 40$ , aucune machine ne l'écrit.

f(x) = 2^xg(x) = 4*x + 1

Le coût des deux méthodes sur la formule ci-dessus. La distributivité, en 2ⁿ, quitte le cadre avant n = 10 ; Tseitin, en 4n + 1, reste une droite. Les deux courbes répondent pourtant à la même question.

Ce que l'explosion signifie vraiment

Elle ne dit pas que le problème est difficile : la formule de départ est trivialement satisfiable, il suffit de poser

x_1 = y_1 = 1

.
Elle dit que la traduction est mauvaise. Un solveur ne verra jamais cette formule facile, parce qu'il aura fallu écrire un million de clauses avant de le lancer. Le coût est entièrement dans la mise en forme, et c'est exactement ce que Tseitin supprime.

La transformation de Tseitin

L'idée tient en une phrase : nommer chaque sous-formule par une variable nouvelle, et écrire ce que ce nom veut dire.

Principe

À chaque sous-formule $\varphi$ de $F$ , on associe une variable fraîche $t_\varphi$ , et l'on écrit les clauses qui traduisent $t_\varphi \leftrightarrow \varphi$ en ne regardant que les fils immédiats de $\varphi$ .

La formule finale est la conjonction de toutes ces clauses de définition, plus la clause unitaire $(t_F)$ qui impose que la racine soit vraie.

Ces clauses ne s'apprennent pas, elles se retrouvent. Un $\leftrightarrow$ est une double implication, et il suffit d'écrire les deux sens séparément.

Prenons $t \leftrightarrow (a \wedge b)$ .

Premier sens, $t \rightarrow (a \wedge b)$ . Si le nom est vrai, la sous-formule l'est, donc $a$ est vrai et $b$ aussi. Cela fait deux implications, $t \rightarrow a$ et $t \rightarrow b$ , qui s'écrivent $(\neg t \vee a)$ et $(\neg t \vee b)$ .

Second sens, $(a \wedge b) \rightarrow t$ . Si la sous-formule est vraie, le nom l'est. En éliminant l'implication : $\neg(a \wedge b) \vee t$ , et De Morgan donne $(\neg a \vee \neg b \vee t)$ .

Trois clauses, et aucune n'a été mémorisée. Le même raisonnement, avec les rôles du et et du ou échangés, donne les autres lignes du tableau.

Les clauses de définition

Ce qu'on définit	Clauses
$t \leftrightarrow \neg a$	$(\neg t \vee \neg a)$ , $(t \vee a)$
$t \leftrightarrow (a \wedge b)$	$(\neg t \vee a)$ , $(\neg t \vee b)$ , $(t \vee \neg a \vee \neg b)$
$t \leftrightarrow (a \vee b)$	$(\neg t \vee a \vee b)$ , $(t \vee \neg a)$ , $(t \vee \neg b)$
$t \leftrightarrow (a \rightarrow b)$	$(\neg t \vee \neg a \vee b)$ , $(t \vee a)$ , $(t \vee \neg b)$

Voici la formule $(x \wedge y) \vee (\neg x \wedge z)$ vue comme un arbre. Chaque nœud interne va recevoir un nom.

Graphe orienté7 sommets, 6 arêtes

L'arbre de la formule. La racine t3 est le ou, t1 et t2 sont les deux et. Tseitin n'écrit des clauses que pour ces trois nœuds, en ne regardant chaque fois que les deux enfants immédiats : c'est de là que vient le coût linéaire, puisqu'on ne descend jamais dans les sous-arbres.

Tseitin sur

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

Nommer les sous-formules. $t_1$ pour $x \wedge y$ , $t_2$ pour $\neg x \wedge z$ , $t_3$ pour $t_1 \vee t_2$ .

Écrire les définitions.

$t_1 \leftrightarrow x \wedge y$ donne $(\neg t_1 \vee x)$ , $(\neg t_1 \vee y)$ , $(t_1 \vee \neg x \vee \neg y)$ .

$t_2 \leftrightarrow \neg x \wedge z$ donne $(\neg t_2 \vee \neg x)$ , $(\neg t_2 \vee z)$ , $(t_2 \vee x \vee \neg z)$ .

$t_3 \leftrightarrow t_1 \vee t_2$ donne $(\neg t_3 \vee t_1 \vee t_2)$ , $(t_3 \vee \neg t_1)$ , $(t_3 \vee \neg t_2)$ .

Imposer la racine. La clause unitaire $(t_3)$ .

Dix clauses, six variables. La figure ci-dessous les montre sous l'affectation $x = 1$ , $y = 1$  : la propagation reconstitue toute seule $t_1 = 1$ puis $t_3 = 1$ , ce qui est bien le comportement attendu d'une définition.

10 clausessatisfaiteunitaireen attente

c1(¬t1∨x)
c2(¬t1∨y)
c3(t1∨¬x∨¬y)⇒ t1 = 1
c4(¬t2∨¬x)⇒ t2 = 0
c5(¬t2∨z)
c6(t2∨x∨¬z)
c7(¬t3∨t1∨t2)
c8(t3∨¬t1)
c9(t3∨¬t2)
c10(t3)⇒ t3 = 1

t1xyt2zt3

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

Propagation unitaire : t1 = 1, t2 = 0, t3 = 1. Ces valeurs ne sont pas des choix, elles sont imposées.

La formule (x ∧ y) ∨ (¬x ∧ z) après Tseitin. Les variables t1, t2, t3 n'existaient pas dans le problème : elles nomment des sous-formules, et la clause unitaire c10 impose que la racine soit vraie.

Trois propriétés, et elles vont ensemble

La taille reste linéaire. Chaque connecteur de la formule de départ produit au plus trois clauses d'au plus trois littéraux. Une formule de

k

connecteurs donne au plus

3k + 1

clauses, quelle que soit son imbrication.
L'équivalence est perdue. La formule obtenue parle de variables que la formule de départ ne connaît pas. Elles ne peuvent pas avoir les mêmes modèles, ne serait-ce que parce qu'elles ne portent pas sur le même ensemble de variables.
L'équisatisfiabilité est conservée. Tout modèle de la formule de départ s'étend en un modèle de la formule transformée, en donnant à chaque

t_\varphi

la valeur de sa sous-formule. Réciproquement, tout modèle de la transformée, restreint aux variables d'origine, est un modèle de la formule de départ.

Le fichier, en entier

Numérotons dans l'ordre où les variables apparaissent : $x = 1$ , $y = 2$ , $t_1 = 3$ , $z = 4$ , $t_2 = 5$ , $t_3 = 6$ . Voici ce qui part vraiment au solveur.

Format DIMACS CNF6 variables, 10 clauses

1	c (x et y) ou (non x et z), apres Tseitin
2	c x=1 y=2 t1=3 z=4 t2=5 t3=6
3	p cnf 6 10
4	-3 10
5	-3 20
6	3 -1 -20
7	-5 -10
8	-5 40
9	5 1 -40
10	-6 3 50
11	6 -30
12	6 -50
13	60

Les dix clauses de l'exemple précédent, au format d'échange. Les trois dernières lignes définissent la racine, et la toute dernière, réduite à « 6 », est la clause unitaire qui impose que la formule soit vraie.

Le faire écrire par un programme

Personne n'applique Tseitin à la main sur une formule réelle. Trente lignes suffisent, et elles montrent que la transformation est purement mécanique.

main.py

Sortie

>_ Prêt à exécuter…

Deux choses que ce code apprend

La négation ne coûte rien. Le tableau des définitions donne des clauses pour

t \leftrightarrow \neg a

, et pourtant le code ne les écrit jamais : il renvoie simplement l'opposé du littéral. C'est ce que font tous les encodeurs réels, et cela divise le nombre de variables.
La taille reste linéaire, quelle que soit l'imbrication. La dernière boucle empile dix niveaux de « ou » et de « et » les uns dans les autres, et produit une soixantaine de clauses. La distributivité, sur la même formule, aurait explosé. C'est la propriété centrale de Tseitin, mesurée plutôt qu'affirmée.

Lire la solution d'un solveur après Tseitin

Le solveur rend un modèle sur toutes les variables, celles de Tseitin comprises. Il faut donc oublier les variables fraîches et ne garder que les variables d'origine : ce sont les seules qui ont un sens dans le problème posé.
Un solveur bien employé sait d'ailleurs le faire seul, et les formats de modélisation modernes conservent la correspondance pour ne pas rendre à l'utilisateur des noms qu'il n'a jamais écrits.

Ne définir que dans un sens : la variante de Plaisted-Greenbaum

Sur une formule en forme normale négative, la moitié des clauses de définition ne sert à rien : il suffit d'écrire

t \rightarrow \varphi

pour les sous-formules qui apparaissent positivement, et

\varphi \rightarrow t

pour celles qui apparaissent négativement.
On obtient environ deux fois moins de clauses, et l'équisatisfiabilité tient toujours. Le prix se paie ailleurs :

t

n'est plus égal à sa sous-formule, seulement lié à elle, ce qui interdit la transformation pour le comptage de modèles du chapitre 10. Une optimisation correcte pour une question, fausse pour une autre.

Le format DIMACS

C'est le format d'échange universel, compris par tous les solveurs depuis trente ans. Il est volontairement stupide.

Les règles, en entier

Les variables sont des entiers strictement positifs. Un littéral négatif s'écrit avec un signe moins.

Une ligne d'en-tête p cnf <variables> <clauses> annonce les tailles.

Chaque clause tient sur une ligne et se termine par un zéro.

Une ligne commençant par c est un commentaire.

Format DIMACS CNF3 variables, 3 clauses

1	c la formule (x1 ∨ ¬x2) ∧ (¬x1 ∨ x3) ∧ (x2 ∨ ¬x3)
2	p cnf 3 3
3	1 -20
4	-1 30
5	2 -30

Le même exemple en DIMACS. La variable x1 devient 1, ¬x2 devient −2, et le zéro ferme la clause.

Le zéro final n'est pas décoratif

Il permet à une clause de s'étendre sur plusieurs lignes, ce qui arrive constamment sur les instances industrielles où une clause peut compter des milliers de littéraux. Un analyseur DIMACS ne lit donc pas des lignes : il lit un flot d'entiers, et découpe aux zéros.
Oublier le zéro de la dernière clause est la faute d'écriture la plus fréquente, et elle se manifeste par une clause silencieusement fusionnée avec la suivante.

Vérification rapideon peut se reprendre

1.Une clause DIMACS s'écrit « 1 -2 3 ». Que manque-t-il ?

2.Après une transformation de Tseitin, le solveur rend un modèle où t1 = 1. Que faut-il en faire ?

3.Pourquoi préférer Tseitin à la distributivité ?

Exercices type

Mettre

(x \rightarrow y) \rightarrow z

en forme normale conjonctive, par distributivité

Éliminer les implications, de l'extérieur vers l'intérieur :

$(x \rightarrow y) \rightarrow z \ \equiv\ \neg(x \rightarrow y) \vee z \ \equiv\ \neg(\neg x \vee y) \vee z$

De Morgan : $\neg(\neg x \vee y) \equiv x \wedge \neg y$ , d'où $(x \wedge \neg y) \vee z$ .

Distribuer : $(x \vee z) \wedge (\neg y \vee z)$ .

Deux clauses. Contrôle rapide : avec $z = 1$ les deux clauses sont satisfaites, ce qui est correct puisqu'une implication de conclusion vraie est vraie.

Combien de clauses produit Tseitin sur

(x_1 \wedge y_1) \vee \cdots \vee (x_{20} \wedge y_{20})

Vingt conjonctions, chacune définie par 3 clauses : 60 clauses.

Les vingt noms obtenus sont réunis par un ou. En binarisant, dix-neuf disjonctions à 3 clauses chacune : 57 clauses. En traitant le ou comme une seule disjonction de vingt arguments, ce que font les implémentations réelles : une clause $(\neg t \vee t_1 \vee \cdots \vee t_{20})$ et vingt clauses $(t \vee \neg t_i)$ , soit 21 clauses.

Plus la clause unitaire de la racine. Soit 82 clauses dans la seconde variante, contre $2^{20} = 1\,048\,576$ par distributivité.

Le rapport est de l'ordre de treize mille, et il double à chaque conjonction ajoutée.

Écrire les clauses de

t \leftrightarrow (a \oplus b)

, le ou exclusif

Quatre clauses, une par ligne de la table de vérité qu'il faut interdire :

$(\neg t \vee a \vee b)$  : si $t$ est vrai, $a$ et $b$ ne peuvent pas être faux tous les deux.

$(\neg t \vee \neg a \vee \neg b)$  : ni vrais tous les deux.

$(t \vee \neg a \vee b)$  : si $a$ est vrai et $b$ faux, alors $t$ doit être vrai.

$(t \vee a \vee \neg b)$  : symétriquement.

Le ou exclusif coûte donc quatre clauses là où le et et le ou en coûtent trois, et surtout ses clauses comptent trois littéraux au lieu de deux. Ce détail explique en partie pourquoi les instances issues de la cryptographie, saturées de ou exclusifs, résistent si bien aux solveurs.

Deux formules équisatisfiables sont-elles toujours équivalentes ?

Non, et un contre-exemple d'une ligne suffit.

$x$ et $y$ sont toutes deux satisfiables, donc équisatisfiables. Elles ne sont pas équivalentes : l'affectation $x = 1, y = 0$ satisfait la première et pas la seconde.

De même, $x \wedge \neg x$ et $y \wedge \neg y$ sont équisatisfiables, toutes deux insatisfiables, sans partager la moindre variable.

L'équisatisfiabilité ne compare que la réponse à la question SAT. C'est une relation beaucoup plus grossière que l'équivalence, et c'est précisément ce qui la rend utile.

Écrire en DIMACS la formule

(a \vee \neg b) \wedge (\neg a) \wedge (b \vee c)

Numéroter d'abord les variables : $a = 1$ , $b = 2$ , $c = 3$ .

Format DIMACS CNF3 variables, 3 clauses

1	c (a ∨ ¬b) ∧ (¬a) ∧ (b ∨ c)
2	p cnf 3 3
3	1 -20
4	-10
5	2 30

Un fichier DIMACS. Les littéraux négatifs sont en orange, et le zéro qui ferme chaque clause en gris : c'est lui, et non la fin de ligne, qui la termine.

L'en-tête annonce 3 variables et 3 clauses. Noter la deuxième clause, réduite à un seul littéral : c'est une clause unitaire, et elle impose $a = 0$ avant même que le solveur ait commencé à chercher.

La méthode

Éliminer les équivalences, puis les implications, dans cet ordre.
Faire descendre les négations jusqu'aux variables par De Morgan.
Compter les $\vee$ au-dessus des $\wedge$ avant de distribuer : c'est ce qui décide de l'explosion.
Distribuer seulement si la formule est petite et peu imbriquée.
Appliquer Tseitin dans tous les autres cas, en nommant chaque connecteur.
Ne jamais oublier la clause unitaire de la racine : sans elle, la formule est trivialement satisfiable.
Restreindre le modèle rendu aux variables d'origine avant de le lire.

Synthèse

Un littéral est une variable ou sa négation ; une clause est une disjonction de littéraux.
Une CNF est une conjonction de clauses : tout à l'extérieur, au moins un à l'intérieur.
La clause vide est fausse, la formule vide est vraie.
La CNF est la forme d'entrée des solveurs parce qu'elle rend l'échec et la déduction locaux.
Une clause dont tous les littéraux sauf un sont faux force ce dernier : c'est la propagation unitaire.
$x \rightarrow y \equiv \neg x \vee y$ , et les lois de De Morgan font descendre les négations.
La distributivité préserve l'équivalence, et peut produire $2^n$ clauses.
Tseitin nomme chaque sous-formule et produit au plus $3k + 1$ clauses pour $k$ connecteurs.
Tseitin préserve l'équisatisfiabilité, pas l'équivalence : les variables fraîches l'interdisent.
Une clause qui contient $x$ et $\neg x$ est tautologique et se supprime ; une clause subsumée par une plus courte aussi.
Ajouter un littéral à une clause l'affaiblit : la plus courte est la plus forte.
DIMACS : variables entières positives, littéral négatif signé, clause terminée par un zéro.

Forme normale conjonctive et transformation de Tseitin

Ce que ce chapitre apporte

Le vocabulaire, en trois lignes

Pourquoi cette forme, et pas une autre

Ce qu'un solveur jette avant de commencer

Mise en forme normale négative

La distributivité, et son explosion

La transformation de Tseitin

Le fichier, en entier

Le faire écrire par un programme

Le format DIMACS

Exercices type

La méthode

Synthèse