Rappel logique propositionnelle
-------------------------------

  http://liris.cnrs.fr/ecoquery/dokuwiki/lib/exe/fetch.php?media=enseignement:logique:logique-memo1.pdf
  
  - formule
  - interprétation
  - sémantique des formules
  - formules SAT et TAUT
  - def du problème (de décision) SAT
  
Sucre syntaxique et jeux de conncteurs fonctionnellement complets.
  
Formes normales
---------------

CNF et DNF : définition

Transformation (exponentielle)
 . supprimer les connecteurs superflus
 . descendre les négations sur les feuilles
 . distribuer le OU sur le ET (ou l'inverse pour DNF)
  
Transformation de Tseitin
  http://liris.cnrs.fr/ecoquery/dokuwiki/lib/exe/fetch.php?media=enseignement:logique:logique-td3-enonce.pdf
  
Dicussion sur SAT trivial pour DNF VS algo naif exponentiel VS tseitin "lineaire"
  
Le problème SAT
---------------
  http://liris.cnrs.fr/ecoquery/dokuwiki/lib/exe/fetch.php?media=enseignement:logique:logique-memo-sat.pdf
  
Idée de NP difficulté/complétude (sans preuves)

  NP Complétude de SAT
  NP Complétude de k-SAT (k >= 3)
  Polynomialité de 2-SAT

  
Les algorithmes pour résoudre SAT
  - algo naif : critère d'exponentialité
  - dpll
  - propag unitaire