Abstract FR:

Dans la première partie nous formalisons l'idée qu'une conjonction de clauses S qui n'est pas Horn-renommable peut tout de même l'être partiellement. Pour toute formule S nous montrons qu'il existe un sous-ensemble B de variables de S, maximal et unique, tel que S soit Horn renommable relativement à B. Cet ensemble est appelé base de Horn de S. Le reste de S est obtenu à partir de S par suppression de toutes les clauses contenant au moins un littéral sur B. Nous montrons que si S est sans clause unitaire, alors S est satisfaisable si et seulement si le reste de S est satisfaisable. Nous montrons ensuite que ce processus de simplification peut être répété jusqu'à l'obtention d'une formule ayant une base de Horn vide ; on appelle reste itéré de S la formule obtenue en fin de compte. Nous définissons ensuite une nouvelle famille de classes polynomiales pour le probleme SAT. La notion de base de Horn permet en outre de caractériser simplement les formules q-Horn. Nous montrons que la base de Horn ainsi que le reste de S peuvent être calculés en temps linéaire, et que le reste itéré peut être obtenu en temps quadratique. Les algorithmes que nous décrivons s'appuient sur le graphe d'implication exprimant les contraintes du Horn-renommage. La deuxième partie est consacrée à l'étude des données SAT aléatoires, relativement aux littéraux purs. Nous avons tout d'abord réalisé une étude expérimentale sur des données 3-SAT aléatoires afin de détecter quelles formules contiennent des littéraux purs. Nous observons ainsi un phénomène de seuil. Nous prouvons ensuite analytiquement l'existence de ce seuil, en termes identiques pour les trois modèles probabilistes les plus couramment utilisés. Finalement, nous présentons des résultats expérimentaux surprenants qui montrent que les données 2-SAT aléatoires ont, pour la monotonie, des propriétés très particulières