Mines Informatique MP 2010

Thème de l'épreuve Le problème de la satisfiabilité logique
Principaux outils utilisés logique propositionnelle, programmation impérative
Mots clefs logique, satisfiabilité, forme normale conjonctive

Corrigé

(c'est payant, sauf le début): - - - - - - - - - - - - - - - - - - - - - - - - - - -

Extrait gratuit du corrigé

(télécharger le PDF)
           

Énoncé complet

(télécharger le PDF)
                                

Rapport du jury

(télécharger le PDF)
     

Énoncé obtenu par reconnaissance optique des caractères


Épreuve d'informatique 2010
A 2010 INFO. MP
ÉCOLE NATIONALE DES PONTS ET CHAUSSÉES,
ÉCOLES NATIONALES SUPÉRIEURES DE L'AÉRONAUTIQUE ET DE L'ESPACE,
DE TECHNIQUES AVANCÉES, DES TÉLÉCOMMUNICATIONS,
DES MINES DE PARIS, DES MINES DE SAINT-ÉTIENNE, DES MINES DE NANCY,
DES TÉLÉCOMMUNICATIONS DE BRETAGNE,
ÉCOLE POLYTECHNIQUE (FILIÈRE TSI)
CONCOURS D'ADMISSION 2010
ÉPREUVE D'INFORMATIQUE
Filière MP
Durée de l'épreuve : 3 heures.
L'usage de calculettes est autorisé. L'utilisation d'un ordinateur est 
interdite.
Sujet mis à disposition des concours : ENSAE ParisTech, TELECOM SudParis (ex 
INT), TPE-EIVP

L'énoncé de cette épreuve comporte 11 pages.

Les candidats sont priés de mentionner de façon apparente sur la première page 
de la copie :
INFORMATIQUE - MP

Recommandations aux candidats
· Si, au cours de l'épreuve, un candidat repère ce qui lui semble être une 
erreur
d'énoncé, il le signale sur sa copie et poursuit sa composition en expliquant 
les
raisons des initiatives qu'il est amené à prendre.
· Tout résultat fourni dans l'énoncé peut être utilisé pour les questions 
ultérieures
même s'il n'a pas été démontré.
· Il ne faut pas hésiter à formuler les commentaires qui semblent pertinents 
même
lorsque l'énoncé ne le demande pas explicitement.

Composition de l'épreuve
L'épreuve comporte un seul problème

Page 1 sur 11

Épreuve d'informatique 2010

Le problème de la satisfiabilité logique
Préliminaire concernant la programmation : il faudra écrire des fonctions ou des
procédures à l'aide d'un langage de programmation qui pourra être soit Caml, 
soit Pascal,
tout autre langage étant exclu. Indiquer en début de problème le langage de
programmation choisi ; il est interdit de modifier ce choix au cours de 
l'épreuve.
Certaines questions du problème sont formulées différemment selon le langage de
programmation ; cela est indiqué chaque fois que nécessaire. Par ailleurs, pour 
écrire une
fonction ou une procédure en langage de programmation, le candidat pourra 
définir des
fonctions ou des procédures auxiliaires qu'il explicitera ou faire appel à 
d'autres fonctions ou
procédures définies dans les questions précédentes.
Dans l'énoncé du problème, un même identificateur écrit dans deux polices de
caractères différentes désigne la même entité, mais du point de vue 
mathématique pour la
police écrite en italique (par exemple : F) et du point de vue informatique 
pour celle écrite en
romain (par exemple : F).
On appelle variable booléenne une variable qui ne peut prendre que les valeurs 0
(synonyme de faux) ou 1 (synonyme de vrai). Si x est une variable booléenne, on 
appelle
complémenté de x et on note x la négation de x : x vaut 1 si x vaut 0 et x vaut 
0 si x vaut 1.
On appelle littéral une variable booléenne ou son complémenté. Pour un littéral
 = x , où x est une variable booléenne, on définit le complémenté  de  comme 
étant égal
à x. On a ainsi défini le complémenté de tout littéral.
On représente la disjonction (« ou » logique ) par le symbole  et la conjonction
(« et » logique) par le symbole .
On appelle clause une disjonction de littéraux et longueur d'une clause le 
nombre des
littéraux qui composent cette clause. La longueur d'une clause doit être 
toujours au moins
égale à 1.
On appelle formule logique sous forme normale conjonctive une conjonction de
clauses ; chacune de ces clauses est dite appartenir à la formule logique. Dans 
tout le
problème, quand on utilisera l'expression formule logique, il s'agira d'une 
formule
logique sous forme normale conjonctive. On ne suppose pas que toutes les 
clauses d'une
formule logique sont distinctes.
Dans tout le problème, les littéraux d'une même clause sont différents et une 
clause
ne contient pas à la fois une variable et le complémenté de celle-ci : si une 
clause contient
le littéral , elle ne contient pas une deuxième fois  et elle ne contient pas  
. Dans les
algorithmes qui seront à écrire, on fera en sorte que cette propriété soit 
toujours vérifiée. En
conséquence, la longueur d'une clause d'une formule logique n'est jamais 
supérieure au
nombre total de variables de la formule logique considérée.
On appelle valuation des variables d'une formule logique une application de
l'ensemble de ces variables dans l'ensemble {0, 1}. Une clause vaut 1 si au 
moins un de ses
littéraux vaut 1 et 0 sinon. Une clause est dite satisfaite par une valuation 
des variables si elle
vaut 1 pour cette valuation. Une formule logique vaut 1 si toutes ses clauses 
valent 1 et 0
sinon. Une formule logique est dite satisfaite par une valuation des variables 
si elle vaut 1
pour cette valuation. Une formule logique est dite satisfiable s'il existe une 
valuation de ses
variables qui la satisfait. Si une formule logique est satisfiable, on appelle 
alors solution de
cette formule logique toute valuation des variables qui la satisfait. Par 
exemple, la formule
logique :
(x  y  z)  ( x  z)  ( y  z )
est satisfiable et elle est satisfaite par la solution x = 1, y = 0 et z = 1.
Page 2 sur 11

Épreuve d'informatique 2010
Comme pour une variable booléenne, la valeur 0 est synonyme de faux et la 
valeur 1
est synonyme de vrai pour un littéral, une clause ou une formule logique.
Une formule logique qui n'aurait aucune clause est dite vide et considérée comme
toujours satisfaite.
Étant donnée une formule logique F, on note dans ce problème max(F) le nombre
maximum de clauses de F pouvant être satisfaites par une même valuation ; en 
notant m le
nombre de clauses de F, on remarque que F est satisfiable si et seulement si 
max(F) = m.

Première partie : introduction
Pour les deux premières questions de ce problème, on considère trois personnes
nommées X, Y et Z et on s'intéresse au fait qu'elles portent ou non un chapeau. 
On considère
les propositions suivantes :
a) au moins une des personnes porte un chapeau ;
b) au moins une des personnes ne porte pas de chapeau ;
c) si X porte un chapeau, ni Y ni Z n'en portent ;
d) si Y porte un chapeau, au moins une personne parmi X ou Z en porte un.
On définit des variables booléennes x, y et z qui valent 1 si, respectivement, 
X, Y et Z
portent un chapeau et 0 sinon.
 1 ­ Exprimer chacune des propositions a), b), c) et d) comme une formule 
logique
(on rappelle que l'expression « formule logique » signifie « formule logique 
sous
forme normale conjonctive ») exprimée avec les variables x, y et z.
 2 ­ Écrire une formule logique exprimant le fait que les propositions a), b), 
c) et d)
doivent être satisfaites simultanément. Indiquer si cette formule logique est 
satisfiable
ou non et, si elle est satisfiable, donner l'ensemble des solutions pour cette 
formule
logique. On prouvera la réponse.
On considère maintenant la formule logique F1 dépendant de quatre variables x, 
y, z et t :
F1 = (x  y  z)  ( x  z  t )  (x  y  z ) 
(x  y  t )  ( x  z  t )  ( x  t)  (x  y  z).
 3 ­ Indiquer si F1 est satisfiable ou non et, si elle est satisfiable, donner 
l'ensemble
des solutions de F1. On prouvera la réponse.
On considère une formule logique F définie sur n variables booléennes et dont 
toutes
les clauses sont de longueur 3 ; on dit alors qu'il s'agit d'une instance de 
3-SAT ; on note m
le nombre de clauses dont F est la conjonction.
 4 ­ Déterminer une instance F2 de 3-SAT non satisfiable et possédant exactement
8 clauses ; indiquer max(F2) en justifiant la réponse.
On considère une instance F de 3-SAT définie sur n variables booléennes. On 
note V
l'ensemble des 2n valuations des variables de F. Soit val une valuation des n 
variables ; si C
Page 3 sur 11

Épreuve d'informatique 2010
est une clause, on note  (C , val ) la valeur de C pour la valuation val ; on 
note  ( F , val ) le
nombre de clauses de F qui valent 1 pour la valuation val. On a :  ( F , val ) =

 (C , val )
C , clause de F

et max(F) = max  (F , val ) .
val V

 5 ­ On considère une clause C de F ; indiquer en fonction de n la valeur de la
somme :   (C , val ) .
valV

 6 ­ En considérant la somme

 (C , val ) , indiquer en fonction de m un

C , clause de F val V

minorant de max(F).

 7 ­ Donner le nombre minimum de clauses d'une instance de 3-SAT non
satisfiable.
Indications pour la programmation, à lire avec attention
On va désormais numéroter à partir de 1 les variables booléennes d'une formule 
logique.
Ainsi, si les variables sont x, y et z, on associe à x le numéro 1, à y le 
numéro 2 et à z le
numéro 3. Par ailleurs, on numérote le complémenté d'une variable avec l'opposé 
du numéro
associé à celle-ci ; ainsi, avec l'exemple ci-dessus, au littéral x , on 
associe le numéro ­1, au
littéral y , on associe le numéro ­2, au littéral z , on associe le numéro ­3. 
Pour alléger les
explications, on identifie désormais un littéral avec son numéro.
Le mot tableau utilisé plus bas est synonyme de ce qu'on appelle vecteur en 
Caml.
Pour coder une valuation d'un ensemble de n variables booléennes, on utilise un 
tableau d'au
moins n + 1 entiers indicé à partir de 0 ; pour i compris entre 1 et n, la case 
d'indice i donne la
valeur de la variable de numéro i (valeur qui vaut soit 0, soit 1, ou 
éventuellement une valeur
quelconque si la valeur de la variable correspondante n'est pas spécifiée). La 
case d'indice 0
n'est pour l'instant pas utilisée.
Pour coder une clause de longueur p, on utilise un tableau d'au moins p + 1 
entiers indicé à
partir de 0 ; pour i compris entre 1 et p, la case d'indice i contient le 
numéro du littéral qui se
trouve en position i dans la clause. La case d'indice 0 de ce tableau indique 
la longueur de la
clause. Ainsi, si les variables sont x, y, z et t, numérotées respectivement 
par 1, 2, 3 et 4, la
clause (x  t  y) est codé par un tableau représenté ci-dessous :
Indice
Numéro

0
3

1
1

2
­4

3
2

Pour coder une formule logique, on utilise un tableau de tableaux d'entiers 
indicés par (i, j) où
les indices i et j sont supérieurs ou égaux à 0 ; pour i supérieur ou égal à 1, 
la ligne d'indice i
décrit la ie clause de la formule logique. On utilise deux cases de la ligne 
d'indice 0 : la case
d'indice (0, 0) contient le nombre de clauses de la formule logique et la case 
d'indice
(0, 1) contient le nombre total de variables. Ainsi, la formule logique :
F3 = (x  y  z  t)  ( x  z )  (x  t  y)
est codée par le tableau ci-dessous. Dans ce tableau, les cases contenant des 
pointillés existent
ou non ; si elles existent, leurs valeurs n'ont pas d'importance :

Page 4 sur 11

Épreuve d'informatique 2010
j

i
0
1
2
3

0

1

2

3

4

3
4
2
3

4
1
­1
1

...
­2
­3
­4

...
3
...
2

...
4
...
...

Indications pour Caml
En Caml, la formule logique F3 peut être définie comme ci-dessous par le 
vecteur de vecteurs
F3 :
let F3 = [|[|3;4|];[|4;1;-2;3;4|];[|2;-1;-3|];[|3;1;-4;2|]|];;
Soit F un vecteur de vecteurs définissant une formule logique F et soient i et 
j deux entiers
compris entre 1 et F.(0).(0) ; le vecteur F.(i)définit la ie clause de F ; dans 
un calcul
de complexité, on considérera l'instruction F.(i) <- F.(j) comme une seule 
opération
élémentaire.
Fin des indications pour Caml

Indications pour Pascal
On définit les constantes et les types ci-dessous :
CONST
MAX_VAR = 10;
MAX_CLAUSES = 100;
type Valuation = array [0 .. MAX_VAR] of Integer;
type Clause =

array [0 .. MAX_VAR] of Integer;

type Formule = array [0 .. MAX_CLAUSES] of Clause;
La constante MAX_VAR indique le nombre maximum de variables d'une formule 
logique. La
constante MAX_CLAUSES indique le nombre maximum de clauses d'une formule 
logique. Dans ce
problème, on ne se préoccupera pas d'un éventuel débordement de ces tableaux.
La formule logique F3 peut être codée avec une variable F3 de type Formule par :
F3[0][0]:=3; F3[0][1]:=4;
F3[1][0]:=4; F3[1][1]:=1; F3[1][2]:=-2; F3[1][3]:=3; F3[1][4]:=4;
F3[2][0]:=2; F3[2][1]:=-1; F3[2][2]:=-3;
F3[3][0]:=3; F3[3][1]:=1; F3[3][2]:=-4; F3[3][3]:=2;
Soit F un tableau de type Formule définissant une formule logique F et soient i 
et j deux
entiers compris entre 1 et F[0][0] ; le tableau F[i] définit la ie clause de F 
; dans un
calcul de complexité, on considérera l'instruction F[i] := F[j] comme une seule
opération élémentaire.
Fin des indications pour Pascal

Page 5 sur 11

Épreuve d'informatique 2010

Deuxième partie : satisfiabilité, méthode exacte
 8 ­ La fonction valeur_clause.
Caml : Écrire en Caml une fonction valeur_clause telle que, si C est un vecteur
d'entiers codant une clause C et si val est un vecteur codant une valuation val 
d'un
ensemble de variables contenant les variables de C, alors
valeur_clause C val
donne la valeur de C (c'est-à-dire 0 ou 1) pour la valuation val.
Indiquer la complexité de la fonction valeur_clause.
Pascal : Écrire en Pascal une fonction valeur_clause telle que, si C, de type
Clause, code une clause C et si val, de type Valuation, code une valuation val
d'un ensemble de variables contenant les variables de C, alors
valeur_clause(C, val)
donne la valeur de la clause C (c'est-à-dire 0 ou 1) pour la valuation val.
Indiquer la complexité de la fonction valeur_clause.
 9 ­ La fonction satisfait_formule.
Caml : Écrire en Caml une fonction satisfait_formule telle que, si F est un
vecteur de vecteurs d'entiers codant une formule logique F et si val est un 
vecteur
codant une valuation val de l'ensemble des variables de F, alors
satisfait_formule F val
vaut true si val satisfait F et false sinon.
Indiquer la complexité de la fonction satisfait_formule.
Pascal : Écrire en Pascal une fonction satisfait_formule telle que, si F, de 
type
Formule, code une formule logique F et si val, de type Valuation, code une
valuation val de l'ensemble des variables de F, alors
satisfait_formule(F, val)
vaut true si val satisfait F et false sinon.
Indiquer la complexité de la fonction satisfait_formule.
 10 ­ La fonction resoudre_rec.
On considère une formule logique F et un nombre k compris entre 0 et le nombre 
total
de variables de F. Pour i compris entre 1 et k, on fixe une valeur vi égale à 0 
ou 1 pour
la variable i (si k vaut 0, aucune variable n'a une valeur fixée). La fonction
resoudre_rec détermine s'il existe une valuation val des variables telle que
· pour i compris entre 1 et k, la valeur dans val de la variable i est vi,
· val satisfait F.
De plus, la fonction resoudre_rec dispose d'un tableau d'entiers destiné à coder
une valuation des variables ; dans le cas où la valuation cherchée existe, la 
fonction
modifie ce tableau pour qu'il code une telle valuation et elle renvoie alors la 
valeur 1 ;
si la valuation cherchée n'existe pas, la fonction renvoie la valeur 0 sans 
avoir modifié
les cases d'indices compris entre 1 et k.
Caml : Écrire en Caml une fonction récursive resoudre_rec telle que,
· si F est un vecteur de vecteurs d'entiers codant une formule logique F,
· si val est un vecteur d'entiers servant à coder une valuation,
· si k est un entier compris entre 0 et le nombre de variables de F,
Page 6 sur 11

Épreuve d'informatique 2010
· si le vecteur val contient soit 0, soit 1 dans les cases d'indices 1, 2, ..., 
k,
alors resoudre_rec F val k modifie le vecteur val comme indiqué ci-dessus,
en considérant que les valeurs des cases d'indices 1, 2, ..., k de ce vecteur 
sont les
valeurs fixées v1, v2, ..., vk des variables 1, 2, ..., k ; la fonction renvoie 
true si la
valuation cherchée existe et false sinon.
Pascal : Écrire en Pascal une fonction récursive resoudre_rec telle que,
· si F, de type Formule, code une formule logique F,
· si val est de type Valuation,
· si k est un entier compris entre 0 et le nombre de variables de F,
· si le tableau val contient soit 0, soit 1 dans les cases d'indices 1, 2, ..., 
k,
alors resoudre_rec(F, val, k) modifie le tableau val comme indiqué cidessus, en 
considérant que les valeurs des cases d'indices 1, 2, ..., k de ce tableau sont
les valeurs fixées v1, v2, ..., vk des variables 1, 2, ..., k ; la fonction 
renvoie true si la
valuation cherchée existe et false sinon.
 11 ­ La fonction resoudre.
La fonction resoudre prend en argument une formule logique F et renvoie un 
tableau
d'entiers pouvant coder une valuation des variables de F. Si F est satisfiable, 
le tableau
renvoyé code une solution de F et contient la valeur 1 dans la case d'indice 0 
; si F
n'est pas satisfiable, le tableau contient la valeur 0 dans la case d'indice 0.
Caml : Écrire en Caml une fonction resoudre telle que, si F est un vecteur de
vecteurs d'entiers codant une formule logique F, alors resoudre F renvoie un
vecteur d'entiers correspondant au résultat de la fonction resoudre décrite 
ci-dessus.
Pascal : Écrire en Pascal une fonction resoudre telle que, si F, de type 
Formule,
code une formule logique F, alors resoudre(F) renvoie un tableau de type
Valuation correspondant au résultat de la fonction resoudre décrite ci-dessus.
 12 ­ Évaluer la complexité de la fonction resoudre appliquée à une formule 
logique
F en fonction du nombre n de variables de F et de la somme des longueurs des 
clauses
de F.

Troisième partie : MAX-SAT
Dans cette partie, on ne s'intéresse plus à savoir si une formule logique est 
satisfiable mais au
calcul, pour une formule logique F, de max(F). On va définir une heuristique, 
c'est-à-dire une
méthode qui ne donne pas nécessairement la valeur de max(F) mais une valeur 
approchée,
qu'on souhaite proche de l'optimum : on calcule une valuation en choisissant 
une à une les
variables et leurs valeurs. Plus précisément, soit F une formule logique ; 
étant donnée une
variable  de F, on note diff(F, ) le nombre de fois où  figure dans F diminué 
du nombre
de fois où  figure dans F ; l'heuristique utilise la transformation suivante :
Page 7 sur 11

Épreuve d'informatique 2010
a) On calcule pour chaque variable  de F le nombre diff(F, ).
b) Si p est un entier relatif, on note abs(p) la valeur absolue de p. On 
détermine une
variable 0 de F telle que, pour toute variable  de F, on ait :
abs(diff(F, 0))  abs(diff(F, )).
c) On pose 0 = 1 si on a diff(F, 0) > 0 et 0 = 0 sinon.
d) On supprime la variable 0 de F en tenant compte de la valeur choisie de 
façon à ne
conserver que les clauses qui restent à satisfaire après le choix de la valeur 
de 0 ; on
comptabilise le nombre de clauses satisfaites. On obtient ainsi une formule 
logique
notée F qui est la formule transformée à partir de F.
Pour exécuter l'heuristique, on transforme la formule F comme décrit ci-dessus, 
puis on
transforme de même la formule F, puis on transforme la formule transformée à 
partir de F et
ainsi de suite jusqu'à obtenir une formule vide. On somme au fur et à mesure 
les nombres de
clauses satisfaites comptabilisés pendant chaque transformation ; le résultat 
de l'heuristique
est constitué de cette somme et d'une valuation correspondant aux choix 
effectués pendant les
transformations successives pour les valeurs des variables.
 13 ­ Appliquer l'heuristique à la formule F1 définie avant la question  3 ;
détailler les différentes étapes.
De façon à écrire l'heuristique en langage de programmation, on définit cinq 
fonctions
ou procédures dans les cinq questions suivantes.
 14 ­ La fonction place.
Caml : Écrire en Caml une fonction place telle que, si C est un vecteur codant 
une
clause C et si litt est un littéral, place C litt renvoie
· 0 si litt ne figure pas dans C,
· la position de litt dans C si litt figure dans C (valeur comprise entre 1 et 
le
nombre de littéraux de C).
Évaluer la complexité de la fonction place.
Pascal : Écrire en Pascal une fonction place telle que, si C, de type Clause, 
code
une clause C et si litt est un littéral, place(C, litt) renvoie
· 0 si litt ne figure pas dans C,
· la position de litt dans C si litt figure dans C (valeur comprise entre 1 et 
le
nombre de littéraux de C).
Évaluer la complexité de la fonction place.
 15 ­ La fonction ou procédure supprimer_variable.
Caml : Écrire en Caml une fonction supprimer_variable telle que, si C est un
vecteur codant une clause C et si i est un entier compris entre 1 et le nombre 
de
littéraux de C, alors supprimer_variable C i modifie C pour que C code la
clause obtenue en supprimant de la clause C le littéral d'indice i. La 
complexité de
cette fonction doit être de l'ordre d'une constante, et donc ne pas dépendre du 
nombre
de littéraux de la clause C ni de la valeur de i.
Pascal : Écrire en Pascal une procédure supprimer_variable telle que, si C, de
type Clause, code une clause C et si i est un entier compris entre 1 et le 
nombre de
littéraux de C, alors supprimer_variable(C, i) modifie C pour que C code la
Page 8 sur 11

Épreuve d'informatique 2010
clause obtenue en supprimant de la clause C le littéral d'indice i. La 
complexité de
cette fonction doit être de l'ordre d'une constante, et donc ne pas dépendre du 
nombre
de littéraux de la clause C ni de la valeur de i.
 16 ­ La fonction ou procédure supprimer_clause.
Caml : Écrire en Caml une fonction supprimer_clause telle que, si F est un
vecteur de vecteurs d'entiers codant une formule logique F et si i est un entier
compris entre 1 et le nombre de clauses de F, alors supprimer_clause F i
modifie F pour que F code la formule logique obtenue en supprimant la clause
d'indice i. La complexité de cette fonction doit être de l'ordre d'une 
constante, et
donc ne pas dépendre du nombre de clauses de la formule logique ni de la valeur 
de i.
Pascal : Écrire en Pascal une procédure supprimer_clause telle que, si F, de 
type
Formule, code une formule logique F et si i est un entier compris entre 1 et le
nombre de clauses de F, alors supprimer_clause(F, i) modifie F pour que F
code la formule logique obtenue en supprimant la clause d'indice i. La 
complexité de
cette fonction doit être de l'ordre d'une constante, et donc ne pas dépendre du 
nombre
de clauses de la formule logique ni de la valeur de i.
 17 ­ La fonction calculer_diff.
Caml : Écrire en Caml une fonction calculer_diff telle que, si F est un vecteur
de vecteurs d'entiers codant une formule logique F, alors calculer_diff F
renvoie un vecteur d'entiers donnant pour chaque variable  de F la valeur de
diff(F, ) décrite au-dessus de la question  13. En supposant que toutes les 
variables
(dont le nombre figure dans la case d'indice 1 de la ligne d'indice 0 de F) 
figurent
effectivement dans F directement ou par son complémenté, cette fonction doit 
avoir
une complexité de l'ordre de la somme des longueurs des clauses de F.
Pascal : Écrire en Pascal une fonction calculer_diff telle que, si F, de type
Formule, code une formule logique F, alors calculer_diff(F) renvoie un
tableau de type Valuation donnant pour chaque variable  de F la valeur de
diff(F, ) décrite au-dessus de la question  13. En supposant que toutes les 
variables
(dont le nombre figure dans la case d'indice 1 de la ligne d'indice 0 de F) 
figurent
effectivement dans F directement ou par son complémenté, cette fonction doit 
avoir
une complexité de l'ordre de la somme des longueurs des clauses de F.
 18 ­ La fonction simplifier.
On s'intéresse dans cette question à une transformation automatique d'une 
formule
logique F lorsqu'on pose qu'une variable  prend la valeur v. Cette 
transformation est
effectuée à l'aide d'une fonction nommée simplifier prenant F,  et v comme
arguments. Si v vaut 1, on note litt le littéral  et sinon on note litt le 
littéral  . Quand
 prend la valeur v, litt prend la valeur 1 et le complémenté de litt prend la 
valeur 0.
Les clauses contenant litt, prenant la valeur 1, sont supprimées de F. Pour 
chaque
clause contenant le complémenté de litt, on retire ce complémenté ; si une 
clause était
réduite au complémenté de litt, on supprime une telle clause. Les clauses qui ne
contiennent ni litt ni le complémenté de litt sont inchangées. La fonction 
simplifier
compte le nombre de clauses qui contenaient litt avant simplification et 
renvoie ce
nombre.
Page 9 sur 11

Épreuve d'informatique 2010
Caml : Écrire en Caml la fonction simplifier telle que, si F est un vecteur de
vecteurs d'entiers codant une formule logique F, si alpha est un entier 
représentant
une variable  de F et si v vaut 0 ou 1, alors
simplifier F alpha v
transforme F pour que F code la formule logique obtenue à partir de F par la 
fonction
simplifier et renvoie le nombre de clauses de la formule logique F initiale qui
contenaient litt défini ci-dessus.
Évaluer la complexité de la fonction simplifier.
Pascal : Écrire en Pascal la fonction simplifier telle que, si F, de type 
Formule,
code une formule logique F, si alpha est un entier représentant une variable  
de F
et si v vaut 0 ou 1, alors
simplifier(F, alpha, v)
transforme F pour que F code la formule logique obtenue à partir de F par la 
fonction
simplifier et renvoie le nombre de clauses de la formule logique F initiale qui
contenaient litt défini ci-dessus.
Évaluer la complexité de la fonction simplifier.
 19 ­ La fonction heuristique.
Caml : Écrire en Caml une fonction heuristique telle que, si F est un vecteur de
vecteurs d'entiers codant une formule logique F, alors heuristique F renvoie un
vecteur d'entiers codant la valuation des variables résultant de l'heuristique 
décrite au
début de cette partie ; la case d'indice 0 de ce même vecteur devra contenir le 
nombre
de clauses satisfaites par la valuation déterminée par l'heuristique.
Évaluer la complexité de la fonction heuristique.
Pascal : Écrire en Pascal une fonction heuristique telle que, si F, de type
Formule, code une formule logique F, alors heuristique(F) renvoie un tableau
de type Valuation codant la valuation des variables résultant de l'heuristique
décrite au début de cette partie ; la case d'indice 0 de ce même tableau devra 
contenir
le nombre de clauses satisfaites par la valuation déterminée par l'heuristique.
Évaluer la complexité de la fonction heuristique.

Quatrième partie : étude d'un cas particulier
On revient au problème de la satisfiabilité. On s'intéresse dans cette partie à 
une formule
logique dans laquelle chaque littéral apparaît au plus une fois et dans 
laquelle toutes les
clauses sont de longueur au moins 2. On appelle dans ce problème formule 
logique 1-occ
une telle formule logique. Par exemple, la formule logique F4 ci-dessous, ayant 
six variables
x, y, z, t, u, v, est une formule logique 1-occ :
F4 = (x  y  z)  ( x  z  t)  ( y  v )  (u  v)  ( t  u )
On cherche à déterminer une solution d'une formule logique 1-occ.

Page 10 sur 11

Épreuve d'informatique 2010
 20 ­ On considère une formule logique 1-occ qui s'écrit :
F = (x  l1  l2 ...  lk)  ( x  lk + 1  lk + 2  ...  lk + h)  G
avec k  1, h  1, où x est une variable, où l1, ... , lk + h sont des littéraux 
et où G est
une formule logique 1-occ éventuellement vide.
a) Montrer que si {l1, l2, ..., lk, lk + 1, lk + 2, ..., lk + h} contient à la 
fois une variable et
son complémenté, alors F est satisfiable si et seulement si G est satisfiable ; 
on dira
dans ce cas que F réduite par rapport à x donne la formule logique G.
b) On suppose que {l1, l2, ..., lk, lk + 1, lk + 2, ..., lk + h} ne contient 
jamais à la fois une
variable et son complémenté. Indiquer une formule logique 1-occ F ne contenant 
ni x
ni x telle que F est satisfiable si et seulement si F est satisfiable. On dira 
dans ce cas
que F réduite par rapport à x donne la formule logique F.
Remarque : on rappelle que, par définition dans ce problème, une clause ne 
contient
pas à la fois une variable et son complémenté et qu'une formule logique vide est
considérée comme toujours satisfaite.
 21 ­ Exemples de réduction
a) On considère la formule logique (x  y  z)  ( x  z  t)  ( y  t ) ; indiquer la
formule logique obtenue en réduisant celle-ci par rapport à x.
b) On considère la formule logique ( x  z  t)  ( t  u )  (z  u) ; indiquer la
formule logique obtenue en réduisant celle-ci par rapport à t.
 22 ­ Montrer que toute formule logique 1-occ est satisfiable.
 23 ­ Décrire sans utiliser le langage de programmation une fonction (ou une
procédure) récursive calculer_solution
· qui prend en paramètre une formule logique 1-occ F et un tableau val
permettant de coder une valuation des variables ;
· qui transforme le tableau val pour que, après exécution de la fonction (ou de 
la
procédure), val contienne une solution de F.
 24 ­ Appliquer la fonction (ou la procédure) calculer_solution décrite dans la
question précédente à la formule F4. Détailler chaque appel récursif.

Page 11 sur 11

Extrait du corrigé obtenu par reconnaissance optique des caractères



Mines Informatique MP 2010 -- Corrigé
Ce corrigé est proposé par Benjamin Monmege (ENS Cachan), il a été relu par
Vincent Danjean (Enseignant-chercheur en école d'ingénieur) et Guillaume Batog
(ENS Cachan).

Ce sujet d'informatique consiste en un unique problème abordant des questions
de logique propositionnelle. Il se déroule en quatre parties.
· La première partie, très générale, débute par l'étude classique d'un exemple
de modélisation d'une situation de la vie courante via une formule de logique
propositionnelle, qui est ensuite résolue. Le sujet introduit alors le problème
3-SAT et familiarise le candidat avec cette nouvelle notion.
· La deuxième partie propose d'implémenter une méthode exacte de résolution
du problème de satisfiabilité d'une formule logique.
· La troisième partie aborde le problème MAX-SAT et propose de programmer
une heuristique permettant de calculer une solution approchée.
· Finalement, la quatrième partie propose l'étude d'un cas particulier dans 
lequel
il existe un algorithme beaucoup plus simple pour résoudre la satisfiabilité.
Une bonne connaissance du programme de logique propositionnelle est nécessaire
pour aborder ce sujet convenablement. En outre, les fonctions et procédures 
attendues
demandent de bien savoir manipuler les structures impératives (tableaux, 
boucles).
Tout au long du sujet, de nombreuses questions abordent la complexité 
algorithmique
des programmes écrits : il faut donc également savoir compter les boucles et 
évaluer
la quantité d'opérations élémentaires dans une boucle.

Les conseils du jury
Malgré un bon niveau dans l'ensemble, le rapport du jury mentionne deux
erreurs récurrentes au niveau des questions de programmation. Tout d'abord,
« beaucoup de candidats omettent l'indentation de leurs programmes ; cela a
pour conséquence de rendre la lecture de ces programmes difficile ». Ensuite,
le jury constate « une utilisation abusive des exceptions et de la construction
try ». Dans les sujets de concours, il est souvent inutile, et toujours à 
éviter, de faire usage d'exceptions : préférez-y les constructions récursives 
ou les
boucles for et while.

Indications
Partie I
1 Il peut être plus facile d'exprimer dans un premier temps les propositions c)
et d) à l'aide de l'opérateur d'implication =, puis de trouver une formule
équivalente sous forme normale conjonctive.
2, 3 Utiliser une table de vérité pour trouver l'ensemble des solutions.
4 Remarquer qu'il y a exactement 8 valuations sur un ensemble à 3 variables :
pour chaque valuation, construire une clause qui s'évalue à 0 sur celle-ci.
5 Décrire, puis compter l'ensemble des valuations qui assignent la valeur 0 à la
clause C.
P
P
6 Inverser l'ordre de sommation et majorer
(C, val).
C clause de F valV

7 Remarquer que si F est une formule non satisfiable, alors max(F) 6 m - 1 et
utiliser le résultat de la question 6.
Partie II
8 Il peut être utile d'écrire une fonction auxiliaire qui prend en entrée une 
clause C,
une valuation val et l'indice i de l'un des littéraux de C, et renvoie un 
booléen
exprimant si la valeur donnée par val de ce littéral est 0 ou 1.
9 Calculer la complexité de satisfait_formule en fonction de la somme des
longueurs des clauses de la formule.
12 On pourra définir une suite (uk (F, val))06k6n qui compte le nombre 
d'opérations élémentaires exécutées lors de l'appel à resoudre_rec F val (n-k).
Partie III
15 L'ordre des littéraux dans chaque clause n'a aucune importance.
16 L'ordre des clauses dans une formule n'a, ici encore, aucune importance.
17 Initialiser un tableau pour contenir les valeurs diff (F, ), puis le mettre 
à jour
lors du parcours de toutes les clauses de F. On utilisera un entier, qu'on 
pourra
noter MIN_INT, inférieur à toute valeur réelle apparaissant dans diff (F, ), 
pour
signifier qu'un littéral  n'apparaît pas dans la formule F.
18 La fonction simplifier doit parcourir l'ensemble des littéraux d'une formule,
c'est-à-dire les cases significatives du tableau à double entrée qui représente
cette formule. Réfléchir à l'utilisation d'une boucle for ou while étant donnée
l'utilisation des fonctions supprimer_clause et supprimer_litteral.
Partie IV
20.a Raisonner par double implication.
20.b Considérer F = (1  2  . . .  k  k+1  k+2  . . .  k+h )  G.
22 Démontrer le résultat par récurrence sur le nombre de variables qui 
apparaissent
en même temps que leur complémenté dans la formule F.
23 Appliquer le principe de récurrence mis en oeuvre pour répondre à la 
question 22
afin d'en déduire une fonction récursive, puis utiliser les réductions définies
dans les questions 20.a et 20.b.

Pour définir la logique propositionnelle, on introduit traditionnellement
deux notions : la syntaxe et la sémantique. La première décrit l'ensemble des
règles d'écriture pour construire une formule. La seconde donne une 
signification à une formule, c'est-à-dire renvoie une valeur booléenne étant 
donnée une
valuation des variables de la formule. Il est à noter que le sujet est 
légèrement
flou sur cette distinction entre syntaxe et sémantique.
Un théorème fondamental en logique propositionnelle est l'existence de
formes normales. Par exemple, on peut définir un fragment F constitué de
l'ensemble des formules sous la forme C1  · · ·  Cm où, pour j  [[ 1 ; m ]],
la formule Cj s'écrit (x1  · · ·  xp  ¬xp+1  · · ·  ¬xq ), avec x1 , . . . , xq
des variables. On démontre alors que pour toute formule F de la logique
propositionnelle, il existe une formule G  F équivalente à F, c'est-à-dire
prenant la même valeur pour toutes les valuations possibles. On dit que G
est mise en forme normale conjonctive. Le sujet considère uniquement les
formules du fragment F .

I. Introduction
1 La proposition a), exprimant qu'au moins une des personnes X, Y et Z porte
un chapeau, s'énonce grâce la formule Fa = x  y  z : il s'agit d'une unique 
clause
(disjonction de littéraux). De même, la proposition b) s'exprime par Fb = x  y  
z.
Les propositions c) et d) s'expriment comme des implications  =  : comme
les formules doivent être exprimées en forme normale conjonctive, on remarque 
que
l'implication précédente est équivalente à   .
Ainsi, la proposition c), qu'on peut exprimer avec une implication logique sous 
la
forme x = (y  z), ou de manière équivalente x  (y  z), est décrite par la 
formule
Fc = (x  y)  (x  z) par distributivité de la disjonction sur la conjonction. De 
la
même manière, la proposition d) peut être décrite par la formule Fd = y  x  z.
Fa = x  y  z

Fb = x  y  z

Fc = (x  y)  (x  z)

Fd = x  y  z

2 On traduit par une conjonction logique le fait que les quatre propositions 
précédentes doivent être satisfaites simultanément, c'est-à-dire par la formule 
suivante :
F = (x  y  z)  (x  y  z)  (x  y)  (x  z)  (x  y  z)
Pour décider si cette formule est satisfiable ou pas, on construit sa table de 
vérité :
x
0
0
0
0
1
1
1
1

y
0
0
1
1
0
0
1
1

z
0
1
0
1
0
1
0
1

xyz
0
1
1
1
1
1
1
1

xyz
1
1
1
1
1
1
1
0

xy
1
1
1
1
1
1
0
0

xz
1
1
1
1
1
0
1
0

xyz
1
1
0
1
1
1
1
1

F
0
1
0
1
1
0
0
0

La formule F est satisfiable et l'ensemble de ses solutions est
(x = 0, y = 0, z = 1), (x = 0, y = 1, z = 1) et (x = 1, y = 0, z = 0).

On aurait pu commencer par réécrire la formule F en une formule plus simple
et équivalente. En factorisant d'une part la formule x  z, on obtient que
la formule (x  y  z)  (x  y  z) est équivalente à (x  z)  (y  y), puis
à xz puisque y y est une formule valant 0 sur tout valuation. D'autre part,
on remarque que les deux formules (xy z)(xy)(xz) et (xy)(xz)
sont équivalentes en raisonnant sur les valuations de (x  y)  (x  z). Ainsi,
la formule F est équivalente à F = (x  z)  (x  y)  (x  z), pour laquelle
on peut construire une table de vérité plus simple que la précédente.
3 Construisons à nouveau la table de vérité de la formule F1 . Pour simplifier,
on numérote les clauses de la formule F1 de gauche à droite du numéro 1 au 
numéro 7.
x y z t C1 C2 C3 C4 C5 C6 C7 F1
0 0 0 0
0
1
1
1
1
1
1
0
0 0 0 1
0
1
1
0
1
1
1
0
0 0 1 0
1
1
1
1
1
1
1
1
0 0 1 1
1
1
1
0
1
1
1
0
0 1 0 0
1
1
1
1
1
1
0
0
0 1 0 1
1
1
1
1
1
1
0
0
0 1 1 0
1
1
0
1
1
1
1
0
0 1 1 1
1
1
0
1
1
1
1
0
1 0 0 0
1
1
1
1
1
0
1
0
1 0 0 1
1
0
1
1
1
1
1
0
1 0 1 0
1
1
1
1
1
0
1
0
1 0 1 1
1
1
1
1
0
1
1
0
1 1 0 0
1
1
1
1
1
0
1
0
1 1 0 1
1
0
1
1
1
1
1
0
1 1 1 0
1
1
1
1
1
0
1
0
1 1 1 1
1
1
1
1
0
1
1
0
F1 est satisfiable et possède pour une unique solution (x = 0, y = 0, z = 1, t 
= 0).
4 On définit la formule F2 par
F2

= (x  y  z)  (x  y  z)  (x  y  z)  (x  y  z) 
(x  y  z)  (x  y  z)  (x  y  z)  (x  y  z)

Par définition, F2 est une instance de 3-SAT possédant exactement 8 clauses. 
Elle est
non satisfiable puisque pour les 8 valuations possibles sur les variables {x, 
y, z},
au moins une des 8 formules est invalidée : en effet, si v est une valuation, 
la clause
Cv = x  y  z telle que x vaut x si v(x) = 0 et x sinon (de même pour y et z),
s'évalue en 0 sur v, et fait partie des clauses de F2 .
Puisque la formule F2 est non satisfiable, on sait que max(F2 ) est strictement
inférieur à 8. Par ailleurs, la valuation v donnée par (x = 0, y = 0, z = 0) 
satisfait
l'ensemble des clauses de F2 privé de la clause x  y  z. Ainsi,
max(F2 ) = 7
5 La clause C possède trois littéraux x , y et z , respectivement sur les trois
variables (distinctes) x, y et z. Observons que n > 3, sinon la seule instance F
de 3-SAT est la formule vide. Soit VC l'ensemble des valuations val  V 
falsifiant