\'Evolution de la satisfiabilit\'e et de la difficult\'e de formules bool\'eennes al\'eatoires. Applications pour la r\'esolution.

Les formules bool\'eennes sous forme CNF (conjonctive Normal Form) ont jou\'e un role central dans la compr\'ehension de la complexit\'e caculatoire. Derni\`erement il y a eu un int\'er\^et accru pour l'analyse du comportement de formules bool\'eennes al\'eatoires. Elles sont actuellement \'etudi\'ees intensivement tant du point de vue th\'eorique qu'exp\'erimental. Ces r\'ecentes \'etudes ont r\'evel\'e de mani\`ere experimentale l'existence de ph\'enomenes de seuil de satisfiabilit\'e qu'on cherche aujourd'hui activement \`a d\'emontrer. Elles ont par ailleurs conduit sur le plan pratique \`a d\'evelopper des algorithmes de r\'esolution beaucoup plus efficaces. Nous montrerons comment par une analyse de l'espace des solutions nous avons pu progresser sensiblement sur ces deux points. Travail en collaboration avec Yacine Boufkhad.