Corrigé Mines-Ponts 2026 Informatique I MPI — Partie 5 (Q23 à Q30) : Réduction depuis SAT, des formules aux automates : décidabilité

Sujet officiel du concours Mines-Ponts, session 2026, épreuve Informatique I MPI. Corrigé rédigé par Ibrahim Alame.

Énoncé

Tautologie-Presburger : entrée, une formule de Presburger $φ$ sans variable libre ; sortie, sa valeur de vérité. Sat-Cnf : entrée, une formule propositionnelle (sans quantificateur) $φ$ sous forme normale conjonctive ; sortie, un booléen indiquant si $φ$ est satisfiable.

On reprend le type automate et les fonctions des parties 1 et 2. On note $0$ la lettre de $Σ_{n}$ dont toutes les lignes valent $0$ . Pour $L \subseteq Σ_{n}^{*}$ et $i \in [[1, n]]$ ,

$L_{\exists i} = {m \in Σ_{n}^{*} ∣ \exists w \in L, \forall k \in [[1, n]] ∖ {i}, π_{k} (m) = π_{k} (w)}$

(les mots de $L$ dont on a oublié la ligne $i$ ). On dispose de automate_somme n i j k, qui reconnaît $L_{i, j, k} = {m \in Σ_{n}^{*} ∣ v_{i} (m) + v_{j} (m) = v_{k} (m)}$ (pour $n ⩾ 3$ ), de automate_egalite n i j, qui reconnaît $L_{= i, j} = {m ∣ v_{i} (m) = v_{j} (m)}$ , et de sans_zero : automate -> automate, qui renvoie une copie de l'automate dont les états finaux sont les états menant à un état final par une suite de transitions étiquetées $0$ . Pour $φ$ sous forme simple sur $x_{1}, \dots, x_{n}$ , $a^{m}$ donne à chaque variable libre $x_{i}$ la valeur $v_{i} (m)$ , et $L_{φ} = {m \in Σ_{n}^{*} ∣ [[φ]]_{a^{m}} est vrai}$ . Types du sujet :


type terme = V of int | Plus of int*int

type formule =
    |Existe of int * formule
    |Et of formule * formule
    |Non of formule
    |Egale of terme * terme

Q23. Montrer que Sat-Cnf se réduit polynomialement à Tautologie-Presburger.
Q24. Pour $L = {ε, (011), (000) (111)}$ , donner $L_{\exists2}$ .
Q25. Écrire automate_existe : automate -> int -> automate reconnaissant $L (A)_{\exists i}$ .
Q26. Expliquer le principe d'un algorithme qui, pour $φ$ sous forme simple et l'indice $n$ de sa plus grande variable, renvoie un automate reconnaissant $L_{φ}$ .
Q27. Le faire tourner à la main, automates intermédiaires compris, sur $φ (x_{2}) := \neg\exists x_{1} .\neg (x_{1} = x_{2})$ .
Q28. Écrire automate_formule : formule -> int -> automate.
Q29. Démontrer la correction de cet algorithme.
Q30. En déduire est_vraie : formule -> int -> bool qui décide si une formule sous forme simple sans variable libre est vraie.

Corrigé

Q23. Il s'agit de construire, en temps polynomial, une fonction $f$ qui à toute formule $φ$ sous forme normale conjonctive associe une formule de Presburger close $f (φ)$ telle que $φ$ est satisfiable si et seulement si $f (φ)$ est vraie : c'est $S a t - C n f \leq_{p} T a u t o l o g i e - P r es b u r g er$ .

Construction. Soit $φ = C_{1} \land \dots \land C_{r}$ sur les variables propositionnelles $p_{1}, \dots, p_{k}$ . On choisit $k$ variables de Presburger distinctes $x_{1}, \dots, x_{k}$ et l'on remplace chaque variable propositionnelle par un atome de Presburger qui dit « $x_{i}$ est nul » (Q18) :

$p_{i} ⟼ Z (x_{i}) := (x_{i} = x_{i} + x_{i}), \neg p_{i} ⟼ \neg Z (x_{i}),$

les $\lor$ et $\land$ étant conservés. On obtient une formule $φ$ de variables libres $x_{1}, \dots, x_{k}$ , et l'on pose

$f (φ) := \exists x_{1} .\exists x_{2} . \dots \exists x_{k} . φ .$

C'est une formule de Presburger (chaque $x_{i}$ n'est quantifiée qu'une fois), et elle est close. Si la forme normale contient des constantes, on traduit $⊤$ par $\exists y . y = y$ et $⊥$ par $\neg\exists y . y = y$ ( $y$ nouvelle) ; une clause vide vaut $⊥$ et une conjonction vide $⊤$ .

Correction. À une assignation $a$ de $x_{1}, \dots, x_{k}$ , associons la valuation $v_{a}$ définie par $v_{a} (p_{i}) = V$ si et seulement si $a (x_{i}) = 0$ . Par induction sur $φ$ , $[[φ]]_{a} = [[φ]]_{v_{a}}$ : pour un atome, $[[x_{i} = x_{i} + x_{i}]]_{a}$ est vraie si et seulement si $a (x_{i}) = 2 a (x_{i})$ , c'est-à-dire $a (x_{i}) = 0$ , c'est-à-dire $v_{a} (p_{i}) = V$ ; les connecteurs $\neg, \lor, \land$ ont la même table des deux côtés.

Si $f (φ)$ est vraie, il existe $a$ avec $[[φ]]_{a}$ vraie, donc $v_{a}$ satisfait $φ$ .
Si une valuation $v$ satisfait $φ$ , on pose $a (x_{i}) = 0$ si $v (p_{i}) = V$ et $a (x_{i}) = 1$ sinon ; alors $v_{a} = v$ , $[[φ]]_{a}$ est vraie et $f (φ)$ est vraie.

Coût. $f$ se calcule en un parcours de $φ$ : chaque littéral devient un atome de taille constante, et l'on ajoute $k ⩽ ∣ φ ∣$ quantificateurs. La taille de $f (φ)$ et le temps de calcul sont en $O (∣ φ ∣)$ , donc polynomiaux : $S a t - C n f \leq_{p} T a u t o l o g i e - P r es b u r g er$ . (Remarque, hors question : Sat-Cnf étant $NP$ -complet, Tautologie-Presburger est $NP$ -difficile ; la suite du sujet montre qu'il est décidable.)

(Contrôle exécuté : sur $3000$ formes normales conjonctives tirées au hasard, de $1$ à $4$ variables, la satisfiabilité calculée par table de vérité coïncide avec la valeur de $f (φ)$ calculée par évaluation directe, quantificateurs parcourant ${0, 1, 2}$ , ce qui suffit puisque $φ$ ne dépend que des $x_{i}$ nuls ; et est_vraie de Q30, appliquée à la forme simple de $f (φ)$ , répond juste pour $p_{1}$ , $p_{1} \land \neg p_{1}$ et $\neg p_{1}$ .)

Ce que le correcteur attend : le bon sens de la réduction ( $S a t - C n f \leq_{p}$ , et non l'inverse), la traduction des variables propositionnelles en atomes de l'arithmétique (le jury précise que quantifier les variables d'une formule propositionnelle ne donne pas une formule de Presburger), la preuve de l'équivalence dans les deux sens et le caractère polynomial.

Q24. On garde les lignes 1 et 3 de chaque mot de $L$ et l'on laisse la ligne 2 libre, avec la même longueur. Le mot vide donne $ε$ ; la lettre $(011)$ donne deux mots ; le mot de longueur $2$ en donne $2 \times 2 = 4$ :

$L_{\exists2} = {ε, (001), (011), (000) (101), (000) (111), (010) (101), (010) (111)} .$

100 % gratuit

La suite du corrigé est sur Adloun

Le corrigé rédigé en entier, question par question, et le tuteur pour poser des questions sur ce sujet.

Voir le corrigé complet, gratuitement

Inscription gratuite en 30 secondes (e-mail, nom d'utilisateur, mot de passe, classe ou profil), sans carte bancaire : arrivée directe sur le corrigé.

Toutes les parties de l'épreuve

Corrigé complet gratuit →