La résolution étendue étroite

Overview & Synopsis

La résolution étendue (ER) (c'est-à-dire, la résolution incorporant la règle d'extension) est un système de preuve plus puissant que la résolution standard (Res) car elle permet de résoudre en temps polynômial certaines classes d'instances que Res ne peut traiter qu'en temps exponentiel. Cependant, elle est très difficile à mettre en pratique car la règle d'extension accroit considérablement la taille de l'espace de recherche de la preuve. On dit qu'une résolution est étroite si l'application de la règle de résolution produit une résolvante contenant au maximum trois littéraux. Dans cet article nous présentons deux variantes de ER : la résolution étendue étroite (ER3) et la résolution à refragmentation. Ces deux systèmes de preuves p-simulent ER : toute preuve de l'une n'est que polynômialement plus longue que celle de l'autre. ER3 consiste simplement à n'autoriser que des résolutions étroites dans ER. Ceci permet une diminution exponentielle de l'espace de recherche d'une preuve dans ER. La résolution à refragmentation est une variante de ER3 qui permet une intégration facile de la résolution étendue dans n'importe quel solveur appliquant la résolution.