Séminaire du 20 janvier 2003, Vincent Puyhaubert, Projet Algorithmes, Inria, Rocquencourt

Combinatoire analytique appliquée à la satisfaisabilité des formules 3-SAT

Le problème 3-SAT consiste à déterminer si une formule booléenne à trois littéraux par clause est satisfaisable. Lorsque le rapport entre nombre de clauses et nombre de variable augmente, on constate empiriquement la présence d'un phénomène de seuil~: pour une certaine valeur, on passe abruptement de la satisfaisabilité à la contradiction. Bien que ceci ait été mis en évidence pour les formules 2-SAT ou pour le problème voisin 3-XORSAT, il n'existe toujours pas de preuve du phénomène pour le problème 3-SAT.

Les travaux récents ne donnent à ce jour que des bornes supérieures ou inférieures à l'éventuelle valeur de seuil. On présente un aperçu général des méthodes donnant des bornes supérieures. On s'intéressera particulièrement à des méthodes combinatoires usant de séries génératrices, lesquelles permettent de retrouver plusieurs bornes classiques par une méthode simple et uniforme.