Les problèmes SAT... et les graphes.

[@happylife9397]

Merci monsieur.

[@Faxbable]

Super vidéo, très claire ! Mais il y a un truc de base que je n'arrive pas à bien comprendre : pour mesurer la complexité algorithmique en temps d'un algo, le nombre d'opérations du pire des cas doit être exprimé en O(fonction(n)) où n est la taille des données. Normal. Or la donnée d'une instance (formule) a pour taille son nb de littéraux N (donc essentiellement son nombre de clauses), et pas juste le nb de variables n, non ? Et pour le coup, le nb d'opération NOp à effectuer en fonction de N (qui peut lui valoir jusqu'à n2^n pour la plus longue des formules) pourrait être polynomial en N, d'où l'intérêt d'exprimer NOp en fonction de n et pas en fonction de N, sinon la théorie n'a pas d'intérêt, ça je le comprends bien... mais pourquoi dire alors que la taille des données est le nb de variables ? Sinon autre question, je n'ai pas réussi à trouver sur le net : pour n variables, quel est le nombre maximal de n-clauses qu'une formule puisse avoir pour être satisfaisable ? Je disais qu'en théorie une formule peut avoir jusqu'à 2^n n-clauses. Mais en fait, quel est le nombre maximal de clauses qui rend une formule intéressante (au-delà de quoi elle ne sera pas satisfaisable) et du même coup, permettra de gagner en temps de calcul pour un algo "pas stupide" ?

[@emileduvernois6680]

Je ne comprends pas du tout... vous avez choisi des trois-clauses pour simplifier, et les questions vraiment complexes concernent des (grands) systèmes de n-clauses, avec n très grand ? D'autre part, dans tout ce que vous avez exposé, une information m'a échappé : parmi tout cela, qu'est-ce qu'on appelle un problème SAT ?

[@a_la_decouverte_des_graphes]

Comme dit dans la vidéo : le problème 3-SAT (avec des clauses à seulement 3 littéraux) est un problème difficile (il est NP-complet de savoir s'il existe une affectation permettant de rendre toutes les clauses Vrai). Le problème SAT général, est la donnée de clauses (avec un nombre quelconque de littéraux) et de savoir s'il existe une affectation permettant de rendre vrai toutes les clauses. Le problème 3-SAT est donc un cas particulier (mais qui reste difficile) du problème SAT général. J'ai choisi de présenter plutôt 3-SAT dans cette vidéo car c'est un problème très connu et sa description me semblait plus simple à illustrer.

[@emileduvernois6680]

@@a_la_decouverte_des_graphes : D'accord, merci. Pour m'assurer que j'ai bien compris : pour des clauses à trois littéraux, on n'a bien que huit clauses possibles, c'est bien ça? Ça représente 256 systèmes de clauses possibles, non? Des problèmes 3-SAT, il n'en existe que 256, et leur résolution, toute NP complète qu'elle soit, n'est pas bien difficile, par exploration systématique... APRÈS COUP : Ah non, pardon ! Je crois que je viens de comprendre qu'on n'est pas limité à trois variables booléennes différentes. On peut avoir une équation qui fait intervenir trois variables, une deuxième équation qui fait intervenir deux de ces trois variables et une quatrième, etc... Il y a trois variables par équation, mais pas trois variables en tout.

[@a_la_decouverte_des_graphes]

Émile Duvernois. Les variables peuvent être nombreuses comme vous le notez. Cela fait la combinatoire des 3 clauses possibles très grande et les systèmes d’équation très important. Une exploration exhaustive est hors d’atteinte.

[@amaldaagi5450]

donne moi un algorithme approché de problème de satisfiabilité et merci

[@a_la_decouverte_des_graphes]

Tirer une affectation au hasard (comme décrit dans la vidéo) permet d'approcher, de manière probabiliste, le nombre max. de 3-clauses satisfaites. Regardez les détails sous wikipédia (version anglaise) par exemple.

[@amaldaagi5450]

donne moi un algorithme approché de problème de satisfiabilité et merci