Abstract FR:

Nous nous sommes interesses a l'etude des classes de formules cnf propositionnelles pour lesquelles il est possible de generer tous les modeles de facon efficace (i. E. Avec un delai polynomial entre chaque modele genere). Nous proposons un algorithme generique permettant de generer tous les modeles d'une formule quelconque. Nous prouvons que pour les principales classes de formules pour lesquelles on sait resoudre le probleme sat efficacement, notre algorithme genere les solutions avec un delai polynomial. Cette etude nous pousse a etudier ensuite plus en detail les classes de formules pour lesquelles la resolution unitaire est le seul outil utilise pour la generation. C'est pourquoi nous nous interessons aux formules horn etendues introduites par chandru et hooker. Malheureusement, il n'existe pas encore d'algorithme polynomial permettant de tester si une formule appartient a cette classe. Nous etudions donc la classe des formules horn etendues simples qui est une restriction de la classe pecedente pour laquelle swaminathan et wagner ont propose un algorithme de reconnaissance quadratique. Une etude de la structure de ces formules nous permet de proposer un algorithme de reconnaissance lineaire. Le resultat de plus original de ce travail est la presentation de la classe des formules ordonnees. Cette classe etend de facon naturelle celle des formules de horn, en preservant les proprietes relatives a la resolution unitaire (sat, generation de modeles). De plus, nous proposons un algorithme quadratique permettant de determiner si une formule est ordonnee-renommable. En outre nous presentons la classe des formules presque ordonnees qui englobe les formules ordonnees-renommables. Ces formules peuvent etre reconnues en temps polynomial et on peut aussi generer leurs modeles en n'utilisant que la resolution unitaire, a condition de disposer d'un ordre convenable sur les variables.