Probleme – La transformation de Tseitin : une \textsc{fnc} linéaire

Exercice · niveau 3 (difficile) · informatique (MP2I/MPI), chapitre 20 — Logique propositionnelle

Énoncé

Le cours annonce que « les solveurs réels emploient des transformations qui ajoutent des variables au lieu de distribuer ». On construit ici cette transformation.

À chaque sous-formule $ψ$ de $φ$ , on associe une variable fraîche $t_{ψ}$ , et l'on écrit des clauses exprimant $t_{ψ} \leftrightarrow ψ$ localement.

Donner les clauses traduisant $t \leftrightarrow (a \land b)$ , puis $t \leftrightarrow (a \lor b)$ , puis $t \leftrightarrow \neg a$ .
En déduire la construction, et compter les clauses.
La fnc obtenue est-elle équivalente à $φ$ ? Que garde-t-on ?
Comparer, sur $φ_{n}$ du cours, avec la mise en fnc par distribution.

Corrigé

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 $φ$ .

<details class="group my-6 border border-gray-300 rounded-2xl bg-black/[0.03] overflow-hidden transition-all duration-300"><summary style="color:#1e3a8a" class="flex items-center justify-between p-4 cursor-pointer text-xs font-bold select-none"><div class="flex items-center"><i class="fa-solid fa-graduation-cap mr-2"></i>Démonstration</div><span class="transition-transform group-open:rotate-180"><i class="fa-solid fa-chevron-down"></i></span></summary><div style="color:#1d4ed8" class="force-blue p-4 pt-0 border-t border-gray-200 bg-black/[0.02] leading-relaxed font-sans text-xs select-text"> ( $\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.

Les autres exercices de ce chapitre Le cours du chapitre

Un blocage sur cet exercice ? Le tuteur d'Adloun guide par questions, sans donner la réponse.