Problème — La transformation de Tseitin : une fnc linéaire — exercice corrigé d'informatique (MP2I/MPI) (chapitre 20)

1. Les trois traductions. On décompose l'équivalence en deux implications, puis on décompose chaque implication.

$t \leftrightarrow (a \land b) t \leftrightarrow (a \lor b) t \leftrightarrow \neg a t \leftrightarrow (a \to b) (\neg t \lor a) \land (\neg t \lor b) \land (t \lor \neg a \lor \neg b) (\neg t \lor a \lor b) \land (t \lor \neg a) \land (t \lor \neg b) (\neg t \lor \neg a) \land (t \lor a) (\neg t \lor \neg a \lor b) \land (t \lor a) \land (t \lor \neg b)$

Comment on les retrouve sans les apprendre : pour $t \leftrightarrow (a \land b)$ , le sens $t \to (a \land b)$ donne $\neg t \lor (a \land b)$ , qu'on distribue en deux clauses ; le sens $(a \land b) \to t$ donne $\neg (a \land b) \lor t = \neg a \lor \neg b \lor t$ . Trois clauses, chacune de longueur au plus $3$ . La distribution reste ici sans danger parce qu'elle porte sur deux littéraux, jamais sur des formules.

2. La construction. On parcourt l'arbre de $φ$ de bas en haut ; à chaque nœud interne on crée une variable fraîche et l'on émet ses trois clauses ; à la fin, on ajoute la clause unitaire $(t_{φ})$ , qui force la racine à être vraie.


Entrée  : une formule phi.
Sortie  : une FNC.
Pour chaque nœud interne de l'arbre de phi, dans un parcours postfixe :
    creer une variable fraiche t
    emettre les 2 ou 3 clauses de t <-> (operation sur les fils)
Emettre la clause unitaire (t_racine).

Le compte. Un nœud interne engendre au plus $3$ clauses de longueur au plus $3$ , et une variable. Si $φ$ a $k$ nœuds internes, on obtient au plus $3 k + 1$ clauses et $k$ variables auxiliaires : la fnc est de taille linéaire en $∣ φ ∣$ . Mesuré sur $φ_{n}$ : $6 n - 2$ clauses et $2 n - 1$ variables auxiliaires.

3. Non, elle n'est pas équivalente — et elle ne peut pas l'être : elle parle de variables que $φ$ ne connaît pas. Ce qu'on garde est plus faible et parfaitement suffisant :

◆Théorème 20.1Équisatisfiabilité

Notons $T (φ)$ la fnc de Tseitin. Alors $φ$ est satisfiable si et seulement si $T (φ)$ l'est. De plus, tout modèle de $T (φ)$ , restreint aux variables de $φ$ , est un modèle de $φ$ .

Démonstration

( $\Rightarrow$ ) Soit $v$ un modèle de $φ$ . Étendons $v$ en posant $t_{ψ} := [[ψ]]_{v}$ pour chaque sous-formule $ψ$ . Chaque groupe de clauses traduit exactement $t_{ψ} \leftrightarrow ψ$ , donc est satisfait par construction ; et la clause unitaire $(t_{φ})$ l'est puisque $[[φ]]_{v} = V$ .

( $\Leftarrow$ ) Soit $w$ un modèle de $T (φ)$ . Une récurrence sur la hauteur de $ψ$ montre que $w (t_{ψ}) = [[ψ]]_{w}$ : c'est vrai pour les feuilles, et les clauses du nœud $ψ$ imposent précisément l'équivalence. En particulier $w (t_{φ}) = [[φ]]_{w}$ , et la clause unitaire donne $w (t_{φ}) = V$ : la restriction de $w$ est un modèle de $φ$ .

L'équisatisfiabilité suffit, et c'est le point de méthode à retenir : on ne demande jamais à un solveur sat de préserver le sens, seulement de préserver la réponse. Vérifié à la mesure sur $400$ formules tirées au hasard sur trois variables : $φ$ et $T (φ)$ ont toujours le même statut, et la restriction d'un modèle de $T (φ)$ satisfait toujours $φ$ .

4. La comparaison, mesurée sur $φ_{n} = (p_{1} \land q_{1}) \lor \dots \lor (p_{n} \land q_{n})$ :

$n$	taille de $φ_{n}$	fnc par distribution	fnc de Tseitin	variables ajoutées
$1$	$3$	$2$	$4$	$1$
$3$	$11$	$8$	$16$	$5$
$5$	$19$	$32$	$28$	$9$
$7$	$27$	$128$	$40$	$13$
$10$	$39$	$1024$	$58$	$19$

La distribution est meilleure jusqu'à $n = 4$ , puis Tseitin l'emporte définitivement : $2^{n}$ contre $6 n - 2$ . Le croisement à $n = 5$ mérite d'être noté — une transformation asymptotiquement meilleure peut être plus coûteuse sur les petites instances, et c'est pour cela qu'un solveur regarde la taille avant de choisir.

Problème — La transformation de Tseitin : une fnc linéaire

Énoncé

Corrigé

Exercices semblables