2SAT est décidable en temps linéaire : Différence entre versions
De AgregmathKL
(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 ... ») |
|||
| Ligne 19 : | Ligne 19 : | ||
== Références == | == Références == | ||
* Knuth : TAoCP tome 4A partie 1, page 60 à 62 | * Knuth : TAoCP tome 4A partie 1, page 60 à 62 | ||
| + | |||
| + | [Category: Développement de la leçon 925] | ||
| + | [Category: Développement de la leçon 916] | ||
Version du 26 février 2015 à 21:10
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
[Category: Développement de la leçon 925] [Category: Développement de la leçon 916]
