2SAT est décidable en temps linéaire

De AgregmathKL
Révision de 30 novembre 2011 à 22:32 par Basile (discuter | contributions) (Page créée avec « Ce développement montre que pour toute formule sous forme normale conjonctive dont les clauses sont à deux littéraux, on peut décider en temps linéaire vis à vis de la ... »)

(diff) ← Version précédente | Voir la version courante (diff) | Version suivante → (diff)
Aller à : navigation, rechercher

Ce développement montre que pour toute formule sous forme normale conjonctive dont les clauses sont à deux littéraux, on peut décider en temps linéaire vis à vis de la taille de la formule si celle-ci est satisfiable.

Le développement

pdf : ici

Recasements

  • 925 - Graphes : représentation et algorithmes.
  • 916 - Formules du calcul propositionnel : représentation, formes normales, satisfiabilité. Applications.


  • (920 - Réécriture et formes normales. Exemples.)
  • (914 - Décidabilité et indécidabilité. Exemples.)


Remarques

Knuth est assez élusif sur la démonstration du résultat principal. On peut s'en tenir à ce qu'il écrit et passer du temps sur un exemple ou détailler un peu plus sa preuve, voire présenter carrément l'algorithme dérivé de Tarjan.

Références

  • Knuth : TAoCP tome 4A partie 1, page 60 à 62
Récupérée de « https://minerve.ens-rennes.fr/index.php?title=2SAT_est_décidable_en_temps_linéaire&oldid=399 »