| 摘要 |
<p>La présente invention concerne l'amélioration des algorithmes de satisfaisabilité existants par modification de la représentation du problème qui exploite la structure des problèmes naturels. On considère plus particulièrement les algorithmes communs de satisfaisabilité, et notamment les WSAT et RELSAT. Chacun de ces algorithmes implique l'exécution, au moins une fois, d'un calcul spécifique, ou 'sous-recherche', dans lequel l'algorithme recherche, dans la théorie originale, des clauses fondamentales satisfaisant l'une quelconque des propriétés numériques. Dans le cas des problèmes réalistes, l'invention fait que le temps passé en sous-recherche constitue une quantité négligeable par rapport à l'investissement représenté par le calcul de l'algorithme. De fait, l'invention représente la sous-recherche en termes de S(C,P,us), auquel cas les réalisations fondamentales de C présentent des littéraux u non valorisés par P pour des littéraux s vérifiés pour les valeurs attribuées à P. Cette représentation permet l'exécution d'une recherche intelligente pour résoudre les problèmes de sous-recherche posés en termes de S(C,P,u,s). La sous-recherche intelligente procède par attribution de valeurs de vérité, à des atomes, de façon à éliminer des ensembles de liaisons avec des variables universellement quantifiées dans les limites d'une contrainte clausale quantifiée. Ces liaisons s'éliminent d'ailleurs d'elles-mêmes du fait qu'elles ne peuvent pas satisfaire à une proposition spécifique. De plus, il reste possible de faire une remontée à partir des choix pauvres à l'occasion d'une recherche de liaisons aboutissant à des variables dans les limites des clauses quantifiées. D'une façon générale, la sous-recherche intelligente permet de réduire le temps de vérification des problèmes de O(D?U) à O(DαU¿) pour tout α∫1.</p> |
