Bonjour, je suis à la recherche d'une solution pour les questions 2 et 3 s'il vous plait.

Question 2. Ecrire la méthode grapheDimplication qui a partir d’une instance 2-SAT construit

le graphe d’implication.

On admettra la proposition suivante :

Proposition. Une formule F est satisfaisable si et seulement si pour toute variable p de F,

p et ¬p ne sont pas dans la même composante connexe de GF . Autrement dit, F est satisfaisable

si et seulement si on n’a pas `a la fois un chemin de p vers ¬p et un chemin de ¬p vers p.

Question 3. Ecrire une méthode estSatisfaisable qui d´etermine si une formule F , instance

2-SAT est ou non satisfaisable.

(Ne pas hésiter `a utiliser la méthode strongly connected components de la classe DiGraph

définie dans networkX.). Et voici comment je fais le graphe en image.