[go: up one dir, main page]
Scribd
Importer
6 vues2 pages

(' A Rendre Sous Forme D'un Rapport Le Jeudi 13 Octobre 23h59.) Minisat Dimacs

Transféré par

Fanigue

Droits d'auteur :

© All Rights Reserved
Téléchargez comme PDF, TXT ou lisez en ligne sur Scribd
Télécharger au format pdf ou txt

(' A Rendre Sous Forme D'un Rapport Le Jeudi 13 Octobre 23h59.) Minisat Dimacs

Transféré par

Fanigue
6 vues2 pages

Titre original

SAT_

Copyright

© © All Rights Reserved

Formats disponibles

PDF, TXT ou lisez en ligne sur Scribd

Avez-vous trouvé ce document utile ?

Ce contenu est-il inapproprié ?

Droits d'auteur :

© All Rights Reserved
Téléchargez comme PDF, TXT ou lisez en ligne sur Scribd
Télécharger au format pdf ou txt
6 vues2 pages

(' A Rendre Sous Forme D'un Rapport Le Jeudi 13 Octobre 23h59.) Minisat Dimacs

Transféré par

Fanigue

Droits d'auteur :

© All Rights Reserved
Téléchargez comme PDF, TXT ou lisez en ligne sur Scribd
Télécharger au format pdf ou txt
Vous êtes sur la page 1/ 2

M1 Informatique - Luminy Complexité - 2016 / 2017

N. Creignou, G. Di Molfetta, F. Olive, et K. Perrot

TP no 2
Le solveur Minisat
(À rendre sous forme d’un rapport le jeudi 13 octobre 23h59.)

L’objectif du TP est de se familiariser avec le solveur Minisat, qui permet de décider la satisfai-
sabilité de formules en forme normale conjonctive. De tels solveurs partagent le même format de
représentation des formules en CNF, le format Dimacs.

Travail demandé

Exercice 1. Première utilisation de Minisat

(a) Écrire un fichier texte qui contient la formule (a ∨ b ∨ ¬c ∨ d) ∧ (¬b ∨ c) ∧ (¬a ∨ ¬d) au format
Dimacs (http://people.sc.fsu.edu/˜jburkardt/data/cnf/cnf.html).
(b) Tester la satisfaisabilité de cette formule en utilisant le solveur Minisat (http://minisat.
se/) en vous aidant du guide d’utilisation ci-dessous. La commande est minisat.
(http://www.dwheeler.com/essays/minisat-user-guide.html).
(c) On considère les la formule :
   
ϕ = (¬t → ¬s) → (b ∨ t) → s ∧ (r ∧ m) → (b ∨ a) ∧¬r

i) Mettre ϕ sous forme normale conjonctive.


ii) Écrire la formule CNF obtenue dans un fichier texte sous format Dimacs
iii) Utiliser le solveur Minisat pour décider si ϕ est satisfaisable. Si oui, décider si elle admet
au moins deux valuations satisfaisantes.
(d) Proposer une procédure qui permettrait de décider si une formule est une tautologie.
(e) Le principe des tiroirs affirme que n tiroirs ne peuvent contenir n + 1 chaussettes si on impose
qu’il n’y ait qu’une seule chaussette par tiroir.
i) Écrire une formule propositionnelle ϕn en forme normale conjonctive, qui exprime le fait
que l’on désire ranger (n + 1) objets dans n tiroirs de telle sorte qu’un tiroir ne contienne
qu’au plus un objet. À cet effet on pourra introduire n(n + 1) variables propositionnelles
ci, j , avec 1 ≤ i ≤ n + 1 et 1 ≤ j ≤ n, qui codent le fait que l’objet i se trouve dans le tiroir
j. Ainsi par exemple la clause (c1,1 ∨ c1,2 . . . ∨ c1,n ) traduira le fait que l’objet numéro 1 est
rangé dans un des n tiroirs.
ii) Conformément au principe des tiroirs, la formule ϕn ainsi obtenue est insatisfaisable. Le
vérifier en utilisant le solveur Minisat pour de petites valeurs de n.
iii) Que se passe-t-il quand on fait croı̂tre n ?

Exercice 2. Réduction de 3-C OLOR à S AT


Le problème 3-C OLOR consiste à décider si un graphe est 3-coloriable.

1
3-C OLOR
Instance : Un graphe non-orienté G = (V, E)
Question : G admet-il une 3-coloration valide ?
1. Proposer une réduction en temps polynomial de 3-C OLOR au problème S AT.
Un graphe est représenté par une suite de nombres de la façon suivante. Le premier entier indique le
nombre de sommets n, le second le nombre d’arêtes p. Viennent ensuite 2 p entiers compris entre 1 et
n, chacun des p couple décrivant les extrémités d’une arête. Ainsi,

4 5 1 2 2 3 3 4 1 3 2 4

représente le graphe à 4 sommets et 5 arêtes suivant.

1 3

2. Dessiner le graphe représenté par la séquence

10 15 1 2 2 3 3 4 4 5 5 1 1 6 2 7 3 8 4 9 5 10 6 8 7 9 8 10 9 6 10 7.

3. Implémenter une procédure qui, étant donné un graphe passé en argument selon le format décrit
ci-dessus, produit la formule (au format Dimacs) obtenue en appliquant votre réduction de la
première question.
4. Utiliser cette procédure pour décider si un graphe donné est 3-coloriable, en utilisant le solveur
Minisat.
5. Améliorer le programme précédent de telle sorte que si le graphe est 3-coloriable alors un 3-
coloriage est obtenu. Ce programme doit indiquer la couleur de chaque sommet.
6. Tester votre algorithme sur des exemples simples et sur des graphes aléatoires. Que se passe-t-il
quand on fait grossir la taille des graphes ?

Vous aimerez peut-être aussi