Programmation logique de contraintes - Constraint logic programming

La programmation logique par contraintes est une forme de programmation par contraintes , dans laquelle la programmation logique est étendue pour inclure des concepts de satisfaction de contraintes . Un programme logique de contraintes est un programme logique qui contient des contraintes dans le corps des clauses. Un exemple de clause incluant une contrainte est . Dans cette clause, est une contrainte ; , , et sont des littéraux comme dans la programmation logique normale. Cette clause énonce une condition sous laquelle l'instruction est vérifiée : est supérieur à zéro et les deux et sont vrais. A(X,Y) :- X+Y>0, B(X), C(Y)X+Y>0A(X,Y)B(X)C(Y)A(X,Y)X+YB(X)C(Y)

Comme dans la programmation logique normale, les programmes sont interrogés sur la prouvabilité d'un objectif, qui peut contenir des contraintes en plus des littéraux. Une preuve pour un but est composée de clauses dont les corps sont des contraintes satisfiables et des littéraux qui peuvent à leur tour être prouvés en utilisant d'autres clauses. L'exécution est effectuée par un interpréteur, qui part du but et parcourt récursivement les clauses essayant de prouver le but. Les contraintes rencontrées lors de cette analyse sont placées dans un ensemble appelé magasin de contraintes . S'il s'avère que cet ensemble n'est pas satisfaisant, l'interprète revient en arrière , en essayant d'utiliser d'autres clauses pour prouver le but. En pratique, la satisfiabilité du magasin de contraintes peut être vérifiée à l'aide d'un algorithme incomplet, qui ne détecte pas toujours l'incohérence.

Aperçu

Formellement, les programmes logiques de contraintes sont comme les programmes logiques normaux, mais le corps des clauses peut contenir des contraintes, en plus des littéraux de programmation logique normaux. À titre d'exemple, X>0est une contrainte et est incluse dans la dernière clause du programme logique de contrainte suivant.

B(X,1):- X<0.
B(X,Y):- X=1, Y>0.
A(X,Y):- X>0, B(X,Y).

Comme dans la programmation logique normale, l'évaluation d'un objectif tel que A(X,1)nécessite d'évaluer le corps de la dernière clause avec Y=1. Comme dans la programmation logique normale, cela nécessite à son tour de prouver l'objectif B(X,1). Contrairement à la programmation régulière logique, cela nécessite aussi une contrainte à être satisfaite: X>0la contrainte dans le corps de la dernière clause (dans la programmation régulière logique, X> 0 ne peut pas être prouvé , sauf si X est lié à un entièrement terme terre et l' exécution du le programme échouera si ce n'est pas le cas).

Il n'est pas toujours possible de déterminer si une contrainte est satisfaite lorsque la contrainte est rencontrée. Dans ce cas, par exemple, la valeur de Xn'est pas déterminée lors de l'évaluation de la dernière clause. En conséquence, la contrainte X>0n'est pas satisfaite ni violée à ce stade. Plutôt que de procéder à l'évaluation de B(X,1)puis de vérifier si la valeur résultante de Xest positive par la suite, l'interpréteur stocke la contrainte X>0puis procède à l'évaluation de B(X,1); de cette façon, l'interpréteur peut détecter une violation de la contrainte X>0lors de l'évaluation de B(X,1), et revenir immédiatement en arrière si c'est le cas, plutôt que d'attendre que l'évaluation de B(X,1)se termine.

En général, l'évaluation d'un programme logique de contraintes se déroule comme un programme logique ordinaire. Cependant, les contraintes rencontrées lors de l'évaluation sont placées dans un ensemble appelé magasin de contraintes. A titre d'exemple, l'évaluation du but A(X,1)procède en évaluant le corps de la première clause avec Y=1; cette évaluation s'ajoute X>0à la réserve de contraintes et nécessite que l'objectif B(X,1)soit prouvé. En essayant de prouver cet objectif, la première clause est appliquée mais son évaluation s'ajoute X<0au magasin de contraintes. Cet ajout rend le magasin de contraintes insatisfiable. L'interpréteur revient alors en arrière, supprimant le dernier ajout du magasin de contraintes. L'évaluation de la deuxième clause ajoute X=1et Y>0au magasin de contraintes. Puisque le magasin de contraintes est satisfiable et qu'aucun autre littéral n'est laissé à prouver, l'interpréteur s'arrête avec la solution X=1, Y=1.

Sémantique

La sémantique des programmes logiques de contraintes peut être définie en termes d'interpréteur virtuel qui maintient une paire pendant l'exécution. Le premier élément de cette paire est appelé objectif courant ; le deuxième élément est appelé magasin de contraintes. Le goal actuel contient les littéraux que l'interpréteur essaie de prouver et peut également contenir certaines contraintes qu'il essaie de satisfaire ; le magasin de contraintes contient toutes les contraintes que l'interpréteur a supposées satisfaisables jusqu'à présent. ${\displaystyle \langle G,S\rangle }$

Initialement, l'objectif actuel est l'objectif et le magasin de contraintes est vide. L'interpréteur procède en supprimant le premier élément de l'objectif courant et en l'analysant. Les détails de cette analyse sont expliqués ci-dessous, mais à la fin, cette analyse peut aboutir à une résiliation réussie ou à un échec. Cette analyse peut impliquer des appels récursifs et l'ajout de nouveaux littéraux à l'objectif actuel et de nouvelles contraintes au magasin de contraintes. L'interpréteur revient en arrière si un échec est généré. Une terminaison réussie est générée lorsque le but actuel est vide et que le magasin de contraintes est satisfiable.

Les détails de l'analyse d'un littéral retiré du but sont les suivants. Après avoir retiré ce littéral du début du but, on vérifie s'il s'agit d'une contrainte ou d'un littéral. S'il s'agit d'une contrainte, elle est ajoutée au magasin de contraintes. S'il s'agit d'un littéral, une proposition dont la tête a le même prédicat du littéral est choisie ; la clause est réécrite en remplaçant ses variables par de nouvelles variables (variables n'apparaissant pas dans le but) : le résultat est appelé une nouvelle variante de la clause ; le corps de la nouvelle variante de la clause est alors placé devant le but ; l'égalité de chaque argument du littéral avec celui correspondant de la nouvelle variante head est également placée devant le but.

Certaines vérifications sont effectuées lors de ces opérations. En particulier, la cohérence du magasin de contraintes est vérifiée à chaque fois qu'une nouvelle contrainte lui est ajoutée. En principe, chaque fois que le magasin de contraintes est insatisfiable, l'algorithme peut revenir en arrière. Cependant, vérifier l'insatisfiabilité à chaque étape serait inefficace. Pour cette raison, un vérificateur de satisfiabilité incomplet peut être utilisé à la place. En pratique, la satisfiabilité est vérifiée à l'aide de méthodes qui simplifient le magasin de contraintes, c'est-à-dire le réécrivent sous une forme équivalente mais plus simple à résoudre. Ces méthodes peuvent parfois, mais pas toujours, prouver l'insatisfiabilité d'un magasin de contraintes insatisfiables.

L'interpréteur a prouvé le but lorsque le but courant est vide et que le magasin de contraintes n'est pas détecté insatisfiable. Le résultat de l'exécution est l'ensemble courant de contraintes (simplifiées). Cet ensemble peut inclure des contraintes telles que celles qui forcent les variables à une valeur spécifique, mais peut également inclure des contraintes telles que celles liées uniquement aux variables sans leur donner une valeur spécifique. ${\style d'affichage X=2}$${\displaystyle X>2}$

Formellement, la sémantique de la programmation logique par contraintes est définie en termes de dérivations . Une transition est une paire de paires but/magasin, notée . Un tel couple énonce la possibilité de passer d'un état à l'autre . Une telle transition est possible dans trois cas possibles : ${\displaystyle \langle G,S\rangle \rightarrow \langle G',S'\rangle }$${\displaystyle \langle G,S\rangle }$${\displaystyle \langle G',S'\rangle }$

• un élément de G est une contrainte C , et ; en d'autres termes, une contrainte peut être déplacée du but vers le magasin de contraintes${\displaystyle G'=G\barre oblique inverse \{C\}}$${\displaystyle S'=S\cup \{C\}}$
• un élément de G est un littéral , il existe une clause qui, réécrite à l'aide de nouvelles variables, est , est G avec remplacé par , et ; en d'autres termes, un littéral peut être remplacé par le corps d'une nouvelle variante d'une proposition ayant le même prédicat dans la tête, ajoutant le corps de la nouvelle variante et les égalités de termes ci-dessus au but${\displaystyle L(t_{1},\ldots ,t_{n})}$${\displaystyle L(t_{1}',\ldots ,t_{n}'):-B}$${\style d'affichage G'}$${\displaystyle L(t_{1},\ldots ,t_{n})}$${\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B}$${\style d'affichage S'=S}$
• S et sont équivalents selon la sémantique des contraintes spécifiques${\style d'affichage S'}$

Une séquence de transitions est une dérivation. Un but G peut être prouvé s'il existe une dérivation de to pour un certain magasin de contraintes satisfiable S . Cette sémantique formalise les évolutions possibles d'un interpréteur qui choisit arbitrairement le littéral du but à traiter et la clause pour remplacer les littéraux. En d'autres termes, un but est prouvé sous cette sémantique s'il existe une séquence de choix de littéraux et de clauses, parmi les nombreuses éventuellement, qui conduisent à un but vide et à un magasin satisfiable. ${\displaystyle \langle G,\emptyset \rangle }$${\displaystyle \langle \emptyset ,S\rangle }$

Les interprètes réels traitent les éléments de l'objectif dans un ordre LIFO : les éléments sont ajoutés au premier plan et traités à partir du front. Ils choisissent également la clause de la deuxième règle en fonction de l'ordre dans lequel elles sont écrites, et réécrivent le magasin de contraintes lorsqu'il est modifié.

Le troisième type de transition possible est le remplacement du magasin de contraintes par un équivalent. Ce remplacement est limité à ceux effectués par des méthodes spécifiques, telles que la propagation de contraintes . La sémantique de la programmation logique de contraintes est paramétrique non seulement pour le type de contraintes utilisées mais aussi pour la méthode de réécriture du magasin de contraintes. Les méthodes spécifiques utilisées en pratique remplacent le magasin de contraintes par une plus simple à résoudre. Si le magasin de contraintes est insatisfiable, cette simplification peut détecter cette insatisfiabilité parfois, mais pas toujours.

Le résultat de l'évaluation d'un objectif par rapport à un programme logique de contraintes est défini si l'objectif est prouvé. Dans ce cas, il existe une dérivation de la paire initiale vers une paire où le but est vide. Le magasin de contraintes de cette deuxième paire est considéré comme le résultat de l'évaluation. En effet, le magasin de contraintes contient toutes les contraintes supposées satisfiables pour prouver le but. En d'autres termes, le but est prouvé pour toutes les évaluations de variables qui satisfont à ces contraintes.

L'égalité par paires des termes de deux littéraux est souvent notée de manière compacte par : c'est un raccourci pour les contraintes . Une variante courante de la sémantique pour la programmation logique de contraintes s'ajoute directement au magasin de contraintes plutôt qu'à l'objectif. ${\displaystyle L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')}$${\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'}$${\displaystyle L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')}$

Termes et conditions

Différentes définitions de termes sont utilisées, générant différents types de programmation logique de contraintes : sur des arbres, des réels ou des domaines finis. Une sorte de contrainte toujours présente est l'égalité des termes. De telles contraintes sont nécessaires car l'interpréteur ajoute t1=t2au but chaque fois qu'un littéral P(...t1...)est remplacé par le corps d'une nouvelle variante de clause dont la tête est P(...t2...).

Termes de l'arborescence

La programmation logique par contraintes avec des termes arborescents émule la programmation logique normale en stockant les substitutions en tant que contraintes dans le magasin de contraintes. Les termes sont des variables, des constantes et des symboles de fonction appliqués à d'autres termes. Les seules contraintes considérées sont les égalités et les inégalités entre les termes. L'égalité est particulièrement importante, car des contraintes comme celles-ci t1=t2sont souvent générées par l'interprète. Les contraintes d'égalité sur les termes peuvent être simplifiées, c'est-à-dire résolues, via l' unification :

Une contrainte t1=t2peut être simplifiée si les deux termes sont des symboles de fonction appliqués à d'autres termes. Si les deux symboles de fonction sont les mêmes et que le nombre de sous-termes est également le même, cette contrainte peut être remplacée par l'égalité deux à deux des sous-termes. Si les termes sont composés de symboles de fonction différents ou du même foncteur mais sur un nombre différent de termes, la contrainte est insatisfiable.

Si l'un des deux termes est une variable, la seule valeur autorisée que la variable peut prendre est l'autre terme. En conséquence, l'autre terme peut remplacer la variable dans le magasin d'objectifs et de contraintes actuel, supprimant ainsi pratiquement la variable de la considération. Dans le cas particulier d'égalité d'une variable avec elle-même, la contrainte peut être supprimée comme toujours satisfaite.

Dans cette forme de satisfaction de contraintes, les valeurs des variables sont des termes.

Réels

La programmation de logique de contrainte avec des nombres réels utilise des expressions réelles comme termes. Lorsqu'aucun symbole de fonction n'est utilisé, les termes sont des expressions sur des réels, incluant éventuellement des variables. Dans ce cas, chaque variable ne peut prendre comme valeur qu'un nombre réel.

Pour être précis, les termes sont des expressions sur des variables et des constantes réelles. L'égalité entre les termes est une sorte de contrainte qui est toujours présente, car l'interpréteur génère l'égalité des termes lors de l'exécution. Par exemple, si le premier littéral du but courant est A(X+1)et que l'interpréteur a choisi une clause qui est A(Y-1):-Y=1après la réécriture des variables, les contraintes ajoutées au but courant sont X+1=Y-1et . Les règles de simplification utilisées pour les symboles de fonction ne sont évidemment pas utilisées : n'est pas insatisfiable simplement parce que la première expression est construite avec et la seconde avec . ${\style d'affichage Y=1}$X+1=Y-1+-

Les réels et les symboles de fonction peuvent être combinés, conduisant à des termes qui sont des expressions sur des réels et des symboles de fonction appliqués à d'autres termes. Formellement, les variables et les constantes réelles sont des expressions, comme tout opérateur arithmétique sur d'autres expressions. Les variables, les constantes (symboles de fonction à arité nulle) et les expressions sont des termes, comme tout symbole de fonction appliqué à des termes. En d'autres termes, les termes sont construits sur des expressions, tandis que les expressions sont construites sur des nombres et des variables. Dans ce cas, les variables s'étendent sur des nombres réels et des termes . En d'autres termes, une variable peut prendre un nombre réel comme valeur, tandis qu'une autre prend un terme.

L'égalité de deux termes peut être simplifiée en utilisant les règles pour les termes de l'arbre si aucun des deux termes n'est une expression réelle. Par exemple, si les deux termes ont le même symbole de fonction et le même nombre de sous-termes, leur contrainte d'égalité peut être remplacée par l'égalité des sous-termes.

Domaines finis

La troisième classe de contraintes utilisées dans la programmation logique par contraintes est celle des domaines finis. Les valeurs des variables sont dans ce cas prises dans un domaine fini, souvent celui des nombres entiers . Pour chaque variable, un domaine différent peut être spécifié : X::[1..5]par exemple signifie que la valeur de Xest comprise entre 1et 5. Le domaine d'une variable peut également être donné en énumérant toutes les valeurs qu'une variable peut prendre ; par conséquent, la déclaration de domaine ci-dessus peut également être écrite X::[1,2,3,4,5]. Cette deuxième façon de spécifier un domaine permet des domaines qui ne sont pas composés d'entiers, tels que X::[george,mary,john]. Si le domaine d'une variable n'est pas précisé, il est supposé être l'ensemble des entiers représentables dans le langage. Un groupe de variables peut se voir attribuer le même domaine en utilisant une déclaration comme [X,Y,Z]::[1..5].

Le domaine d'une variable peut être réduit lors de l'exécution. En effet, comme l'interpréteur ajoute des contraintes au magasin de contraintes, il effectue une propagation de contraintes pour imposer une forme de cohérence locale , et ces opérations peuvent réduire le domaine des variables. Si le domaine d'une variable devient vide, le magasin de contraintes est incohérent et l'algorithme revient en arrière. Si le domaine d'une variable devient un singleton , la variable peut se voir attribuer la valeur unique dans son domaine. Les formes de consistance généralement appliquées sont la consistance d' arc , la cohérence de l' hyper-arc , et la consistance limite . Le domaine actuel d'une variable peut être inspecté à l'aide de littéraux spécifiques ; par exemple, dom(X,D)trouve le domaine actuel Dd'une variable X.

Comme pour les domaines de réels, les foncteurs peuvent être utilisés avec des domaines d'entiers. Dans ce cas, un terme peut être une expression sur des nombres entiers, une constante ou l'application d'un foncteur sur d'autres termes. Une variable peut prendre un terme arbitraire comme valeur, si son domaine n'a pas été spécifié comme étant un ensemble d'entiers ou de constantes.

Le magasin de contraintes

Le magasin de contraintes contient les contraintes qui sont actuellement supposées satisfiables. On peut considérer quelle est la substitution actuelle pour la programmation logique régulière. Lorsque seuls les termes de l'arbre sont autorisés, le magasin de contraintes contient des contraintes sous la forme t1=t2; ces contraintes sont simplifiées par unification, d'où des contraintes de forme variable=term; de telles contraintes sont équivalentes à une substitution.

Cependant, le magasin de contraintes peut également contenir des contraintes sous la forme t1!=t2, si la différence !=entre les termes est autorisée. Lorsque des contraintes sur des domaines réels ou finis sont autorisées, le magasin de contraintes peut également contenir des contraintes spécifiques au domaine comme X+2=Y/2, etc.

Le magasin de contraintes étend le concept de substitution actuelle de deux manières. Premièrement, il ne contient pas seulement les contraintes dérivées de l'assimilation d'un littéral à la tête d'une nouvelle variante d'une clause, mais aussi les contraintes du corps des clauses. Deuxièmement, il ne contient pas seulement des contraintes de forme variable=valuemais aussi des contraintes sur le langage de contraintes considéré. Alors que le résultat d'une évaluation réussie d'un programme logique régulier est la substitution finale, le résultat d'un programme logique à contraintes est le magasin de contraintes final, qui peut contenir une contrainte de la forme variable=valeur mais en général peut contenir des contraintes arbitraires.

Les contraintes spécifiques au domaine peuvent provenir du magasin de contraintes à la fois du corps d'une clause et de l'assimilation d'un littéral à une tête de clause : par exemple, si l'interpréteur réécrit le littéral A(X+2)avec une clause dont la nouvelle tête de variante est A(Y/2), la contrainte X+2=Y/2est ajoutée à le magasin de contraintes. Si une variable apparaît dans une expression du domaine réel ou fini, elle ne peut prendre une valeur que dans les réels ou le domaine fini. Une telle variable ne peut pas prendre comme valeur un terme composé d'un foncteur appliqué à d'autres termes. Le magasin de contraintes est insatisfiable si une variable est liée pour prendre à la fois une valeur du domaine spécifique et un foncteur appliqué aux termes.

Une fois qu'une contrainte est ajoutée au magasin de contraintes, certaines opérations sont effectuées sur le magasin de contraintes. Les opérations effectuées dépendent du domaine et des contraintes considérés. Par exemple, l' unification est utilisée pour les égalités d'arbres finis, l' élimination des variables pour les équations polynomiales sur les réels, la propagation de contraintes pour imposer une forme de cohérence locale pour les domaines finis. Ces opérations visent à rendre le magasin de contraintes plus simple à vérifier pour la satisfiabilité et à résoudre.

A la suite de ces opérations, l'ajout de nouvelles contraintes peut modifier les anciennes. Il est essentiel que l'interprète soit capable d'annuler ces modifications lorsqu'il revient en arrière. La méthode de cas la plus simple consiste pour l'interpréteur à sauvegarder l'état complet du magasin à chaque fois qu'il fait un choix (il choisit une clause pour réécrire un objectif). Il existe des méthodes plus efficaces pour permettre au magasin de contraintes de revenir à un état précédent. En particulier, on peut simplement enregistrer les modifications apportées au magasin de contraintes entre deux points de choix, y compris les modifications apportées aux anciennes contraintes. Cela peut être fait en sauvegardant simplement l'ancienne valeur des contraintes qui ont été modifiées ; cette méthode est appelée trailing . Une méthode plus avancée consiste à enregistrer les modifications apportées aux contraintes modifiées. Par exemple, une contrainte linéaire est modifiée en modifiant son coefficient : l'enregistrement de la différence entre l'ancien et le nouveau coefficient permet d'annuler une modification. Cette deuxième méthode est appelée backtracking sémantique , car la sémantique du changement est sauvegardée plutôt que l'ancienne version des contraintes uniquement.

Étiquetage

Les littéraux d'étiquetage sont utilisés sur des variables sur des domaines finis pour vérifier la satisfiabilité ou la satisfiabilité partielle du magasin de contraintes et pour trouver une affectation satisfaisante. Un littéral d'étiquetage est de la forme labeling([variables]), où l'argument est une liste de variables sur des domaines finis. Chaque fois que l'interpréteur évalue un tel littéral, il effectue une recherche dans les domaines des variables de la liste pour trouver une affectation qui satisfait toutes les contraintes pertinentes. Typiquement, cela se fait par une forme de retour en arrière : les variables sont évaluées dans l'ordre, en essayant toutes les valeurs possibles pour chacune d'elles, et en retournant en arrière lorsqu'une incohérence est détectée.

La première utilisation du littéral d'étiquetage est de vérifier la satisfiabilité réelle ou la satisfiabilité partielle du magasin de contraintes. Lorsque l'interpréteur ajoute une contrainte au magasin de contraintes, il n'y applique qu'une forme de cohérence locale. Cette opération peut ne pas détecter d'incohérence même si le magasin de contraintes est insatisfiable. Un littéral d'étiquetage sur un ensemble de variables impose un contrôle de satisfiabilité des contraintes sur ces variables. En conséquence, l'utilisation de toutes les variables mentionnées dans le magasin de contraintes entraîne la vérification de la satisfiabilité du magasin.

La deuxième utilisation du littéral d'étiquetage est de déterminer en fait une évaluation des variables qui satisfont le magasin de contraintes. Sans le littéral d'étiquetage, les variables reçoivent des valeurs uniquement lorsque le magasin de contraintes contient une contrainte de la forme X=valueet lorsque la cohérence locale réduit le domaine d'une variable à une seule valeur. Un littéral d'étiquetage sur certaines variables force l'évaluation de ces variables. En d'autres termes, une fois que le littéral d'étiquetage a été pris en compte, toutes les variables reçoivent une valeur.

Typiquement, les programmes logiques de contraintes sont écrits de telle sorte que les littéraux d'étiquetage ne soient évalués qu'après qu'autant de contraintes que possible aient été accumulées dans le magasin de contraintes. En effet, les littéraux d'étiquetage imposent la recherche, et la recherche est plus efficace s'il y a plus de contraintes à satisfaire. Un problème de satisfaction de contraintes est typiquement résolu par un programme logique de contraintes ayant la structure suivante :

solve(X):-constraints(X), labeling(X)
constraints(X):- (all constraints of the CSP)

Lorsque l'interpréteur évalue le goal solve(args), il place le corps d'une nouvelle variante de la première clause dans le goal actuel. Puisque le premier objectif est constraints(X'), la deuxième clause est évaluée et cette opération déplace toutes les contraintes dans l'objectif actuel et éventuellement dans le magasin de contraintes. Le littéral labeling(X')est ensuite évalué, forçant une recherche d'une solution du magasin de contraintes. Étant donné que le magasin de contraintes contient exactement les contraintes du problème de satisfaction de contraintes d'origine, cette opération recherche une solution du problème d'origine.

Reformulations de programmes

Un programme logique de contraintes donné peut être reformulé pour améliorer son efficacité. Une première règle est que les littéraux étiquetés doivent être placés après qu'autant de contraintes sur les littéraux étiquetés aient été accumulées dans le magasin de contraintes. Alors qu'en théorie est équivalente à , la recherche qui est effectuée lorsque l'interpréteur rencontre le littéral d'étiquetage est sur un magasin de contraintes qui ne contient pas la contrainte . En conséquence, il peut générer des solutions, telles que , qui s'avèrent plus tard ne pas satisfaire cette contrainte. D'autre part, dans la deuxième formulation, la recherche n'est effectuée que lorsque la contrainte est déjà dans le magasin de contraintes. Par conséquent, la recherche ne renvoie que les solutions qui lui sont cohérentes, profitant du fait que des contraintes supplémentaires réduisent l'espace de recherche. A(X):-labeling(X),X>0A(X):-X>0,labeling(X)X>0X=-1

Une deuxième reformulation qui peut augmenter l'efficacité consiste à placer des contraintes avant les littéraux dans le corps des clauses. Encore une fois, et sont en principe équivalents. Cependant, le premier peut nécessiter plus de calculs. Par exemple, si le magasin de contraintes contient la contrainte , l'interpréteur évalue récursivement dans le premier cas ; s'il réussit, il découvre alors que le magasin de contraintes est incohérent lors de l'ajout de . Dans le second cas, lors de l'évaluation de cette clause, l'interpréteur ajoute d'abord au magasin de contraintes, puis évalue éventuellement . Comme le stockage de contraintes après l'ajout de s'avère incohérent, l'évaluation récursive de n'est pas du tout effectuée. A(X):-B(X),X>0A(X):-X>0,B(X)X<-2B(X)X>0X>0B(X)X>0B(X)

Une troisième reformulation qui peut augmenter l'efficacité est l'ajout de contraintes redondantes. Si le programmeur sait (par quelque moyen que ce soit) que la solution d'un problème satisfait une contrainte spécifique, il peut inclure cette contrainte pour provoquer l'incohérence du magasin de contraintes dès que possible. Par exemple, s'il est connu à l'avance que l'évaluation de B(X)se traduira par une valeur positive pour X, le programmeur peut ajouter X>0avant toute occurrence de B(X). Par exemple, A(X,Y):-B(X),C(X)échouera sur l'objectif A(-2,Z), mais cela n'est découvert que lors de l'évaluation du sous-objectif B(X). D'un autre côté, si la clause ci-dessus est remplacée par , l'interpréteur revient en arrière dès que la contrainte est ajoutée au magasin de contraintes, ce qui se produit avant que l'évaluation de even ne commence. A(X,Y):-X>0,A(X),B(X)X>0B(X)

Règles de gestion des contraintes

Les règles de gestion des contraintes ont été initialement définies comme un formalisme autonome pour spécifier les solveurs de contraintes, et ont ensuite été intégrées dans la programmation logique. Il existe deux types de règles de gestion des contraintes. Les règles du premier genre précisent que, sous une condition donnée, un ensemble de contraintes est équivalent à un autre. Les règles du second genre précisent que, sous une condition donnée, un ensemble de contraintes en implique une autre. Dans un langage de programmation à logique de contrainte prenant en charge les règles de gestion des contraintes, un programmeur peut utiliser ces règles pour spécifier les réécritures possibles du magasin de contraintes et les ajouts possibles de contraintes à celui-ci. Voici des exemples de règles :

A(X) <=> B(X) | C(X)
A(X) ==> B(X) | C(X)

La première règle indique que, si B(X)est impliqué par le magasin, la contrainte A(X)peut être réécrite comme C(X). Par exemple, N*X>0peut être réécrit comme X>0si le magasin impliquait que N>0. Le symbole <=>ressemble à l'équivalence en logique et indique que la première contrainte est équivalente à la dernière. En pratique, cela implique que la première contrainte peut être remplacée par la seconde.

La deuxième règle spécifie à la place que cette dernière contrainte est une conséquence de la première, si la contrainte du milieu est entraînée par le magasin de contraintes. En conséquence, si se A(X)trouve dans le magasin de contraintes et B(X)est impliqué par le magasin de contraintes, alors C(X)peut être ajouté au magasin. A la différence du cas d'équivalence, il s'agit d'un ajout et non d'un remplacement : la nouvelle contrainte est ajoutée mais l'ancienne demeure.

L'équivalence permet de simplifier le magasin de contraintes en remplaçant certaines contraintes par des contraintes plus simples ; en particulier, si la troisième contrainte dans une règle d'équivalence est true, et que la deuxième contrainte est impliquée, la première contrainte est supprimée du magasin de contraintes. L'inférence permet l'ajout de nouvelles contraintes, ce qui peut conduire à prouver l'incohérence du magasin de contraintes, et peut généralement réduire la quantité de recherche nécessaire pour établir sa satisfiabilité.

Les clauses de programmation logique en conjonction avec les règles de gestion des contraintes peuvent être utilisées pour spécifier une méthode pour établir la satisfiabilité du magasin de contraintes. Différentes clauses sont utilisées pour mettre en œuvre les différents choix de la méthode ; les règles de gestion des contraintes sont utilisées pour réécrire le magasin de contraintes pendant l'exécution. A titre d'exemple, on peut implémenter le backtracking avec propagation unitaire de cette façon. Let holds(L)représente une clause propositionnelle, dans laquelle les littéraux de la liste Lsont dans le même ordre qu'ils sont évalués. L'algorithme peut être implémenté en utilisant des clauses pour le choix d'affecter un littéral à vrai ou faux, et des règles de gestion de contraintes pour spécifier la propagation. Ces règles spécifient que holds([l|L])peut être supprimé si l=truesuit du magasin, et il peut être réécrit comme holds(L)s'il l=falsesuit du magasin. De même, holds([l])peut être remplacé par l=true. Dans cet exemple, le choix de la valeur d'une variable est mis en œuvre à l'aide de clauses de programmation logique ; cependant, il peut être encodé dans des règles de gestion de contraintes en utilisant une extension appelée règles de gestion de contraintes disjonctives ou CHR ^∨ .

Évaluation ascendante

La stratégie standard d'évaluation des programmes logiques est descendante et en profondeur d'abord : à partir du but, un certain nombre de clauses sont identifiées comme pouvant éventuellement prouver le but, et une récursivité sur les littéraux de leurs corps est effectuée. Une stratégie alternative consiste à partir des faits et à utiliser des clauses pour dériver de nouveaux faits ; cette stratégie est appelée bottom-up . Elle est considérée comme meilleure que celle descendante lorsque l'objectif est de produire toutes les conséquences d'un programme donné, plutôt que de prouver un objectif unique. En particulier, trouver toutes les conséquences d'un programme de la manière standard descendante et en profondeur d'abord peut ne pas se terminer alors que la stratégie d'évaluation ascendante se termine.

La stratégie d'évaluation ascendante maintient l'ensemble des faits prouvés jusqu'à présent lors de l'évaluation. Cet ensemble est initialement vide. À chaque étape, de nouveaux faits sont dérivés en appliquant une clause de programme aux faits existants et sont ajoutés à l'ensemble. Par exemple, l'évaluation ascendante du programme suivant nécessite deux étapes :

A(q).
B(X):-A(X).

L'ensemble des conséquences est initialement vide. À la première étape, A(q)est la seule clause dont le corps peut être prouvé (parce qu'elle est vide), et A(q)est donc ajoutée à l'ensemble actuel des conséquences. A la deuxième étape, puisque A(q)est prouvée, la deuxième clause peut être utilisée et B(q)s'ajoute aux conséquences. Comme aucune autre conséquence ne peut être prouvée à partir de {A(q),B(q)}, l'exécution se termine.

L'avantage de l'évaluation ascendante par rapport à l'évaluation descendante est que les cycles de dérivations ne produisent pas de boucle infinie . En effet, l'ajout d'une conséquence à l'ensemble actuel de conséquences qui la contient déjà n'a aucun effet. Par exemple, l'ajout d'une troisième clause au programme ci-dessus génère un cycle de dérivations dans l'évaluation descendante :

A(q).
B(X):-A(X).
A(X):-B(X).

Par exemple, lors de l'évaluation de toutes les réponses à l'objectif A(X), la stratégie descendante produirait les dérivations suivantes :

A(q)
A(q):-B(q), B(q):-A(q), A(q)
A(q):-B(q), B(q):-A(q), A(q):-B(q), B(q):-A(q), A(q)

En d'autres termes, la seule conséquence A(q)est produite en premier, mais ensuite l'algorithme effectue un cycle sur les dérivations qui ne produisent aucune autre réponse. Plus généralement, la stratégie d'évaluation descendante peut cycler sur des dérivations possibles, éventuellement lorsqu'il en existe d'autres.

La stratégie ascendante n'a pas le même inconvénient, car les conséquences déjà dérivées n'ont aucun effet. Sur le programme ci-dessus, la stratégie ascendante commence à s'ajouter A(q)à l'ensemble des conséquences ; dans la deuxième étape, B(X):-A(X)est utilisé pour dériver B(q); dans la troisième étape, les seuls faits qui peuvent être déduits des conséquences actuelles sont A(q)et B(q), qui sont cependant déjà dans l'ensemble des conséquences. En conséquence, l'algorithme s'arrête.

Dans l'exemple ci-dessus, les seuls faits utilisés étaient des littéraux de base. En général, chaque clause qui ne contient que des contraintes dans le corps est considérée comme un fait. Par exemple, une clause A(X):-X>0,X<10est également considérée comme un fait. Pour cette définition étendue des faits, certains faits peuvent être équivalents sans être syntaxiquement égaux. Par exemple, A(q)est équivalent à A(X):-X=qet les deux sont équivalents à A(X):-X=Y, Y=q. Pour résoudre ce problème, les faits sont traduits sous une forme normale dans laquelle la tête contient un tuple de variables toutes différentes ; deux faits sont alors équivalents si leurs corps sont équivalents sur les variables de la tête, c'est-à-dire que leurs ensembles de solutions sont les mêmes lorsqu'on les restreint à ces variables.

Comme décrit, l'approche ascendante a l'avantage de ne pas considérer les conséquences qui ont déjà été dérivées. Cependant, il peut encore dériver des conséquences qui sont entraînées par celles déjà dérivées tout en n'étant égal à aucune d'entre elles. À titre d'exemple, l'évaluation ascendante du programme suivant est infinie :

A(0).
A(X):-X>0.
A(X):-X=Y+1, A(Y).

L'algorithme d'évaluation ascendant déduit d'abord ce qui A(X)est vrai pour X=0et X>0. Dans la deuxième étape, le premier fait avec la troisième clause permet la dérivation de A(1). Dans la troisième étape, A(2)est dérivé, etc. Cependant, ces faits sont déjà entraînés par le fait qui A(X)est vrai pour tout non négatif X. Cet inconvénient peut être surmonté en vérifiant les faits d' implication qui doivent être ajoutés à l'ensemble actuel de conséquences. Si la nouvelle conséquence est déjà entraînée par l'ensemble, elle ne lui est pas ajoutée. Étant donné que les faits sont stockés sous forme de clauses, éventuellement avec des "variables locales", l'implication est limitée aux variables de leurs têtes.

Programmation logique de contraintes concurrentes

Les versions concurrentes de la programmation logique de contraintes visent à programmer des processus concurrents plutôt qu'à résoudre des problèmes de satisfaction de contraintes . Les objectifs de la programmation logique par contraintes sont évalués simultanément ; un processus concurrent est donc programmé comme évaluation d'un but par l' interprète .

Syntaxiquement, les programmes logiques à contraintes concurrentes sont similaires aux programmes non concurrents, la seule exception étant que les clauses incluent des gardes , qui sont des contraintes qui peuvent bloquer l'applicabilité de la clause dans certaines conditions. Sémantiquement, la programmation logique à contraintes concurrentes diffère de ses versions non concurrentes car une évaluation d'objectif est destinée à réaliser un processus concurrent plutôt que de trouver une solution à un problème. Plus particulièrement, cette différence affecte le comportement de l'interpréteur lorsque plus d'une clause est applicable : la programmation logique de contraintes non simultanées essaie récursivement toutes les clauses ; la programmation logique de contraintes concurrentes n'en choisit qu'une. C'est l'effet le plus évident d'une directionnalité voulue de l'interprète, qui ne révise jamais un choix qu'il a pris auparavant. D'autres effets de ceci sont la possibilité sémantique d'avoir un objectif qui ne peut pas être prouvé alors que l'ensemble de l'évaluation n'échoue pas, et une manière particulière d'assimiler un objectif et une tête de clause.

Applications

Programmation logique contrainte a été appliquée à un certain nombre de domaines, tels que la planification automatisée , l' inférence de type , génie civil , génie mécanique , circuit numérique vérification, le contrôle du trafic aérien , des finances et autres.

Histoire

La programmation logique par contraintes a été introduite par Jaffar et Lassez en 1987. Ils ont généralisé l'observation que les termes équations et déséquations de Prolog II étaient une forme spécifique de contraintes, et ont généralisé cette idée aux langages de contraintes arbitraires. Les premières implémentations de ce concept ont été Prolog III , CLP(R) et CHIP .

Voir également

• BPrologue
• BNR Prolog (alias CLP (BNR))
• Ciao
• CLP(R)
• Distribué Oz Mozart
• Éclipse
• Prologue GNU
• SWI-Prolog

Les références

• Dechter, Rina (2003). Traitement des contraintes . Morgan Kaufmann. ISBN 1-55860-890-7. ISBN  1-55860-890-7
• Apt, Krzysztof (2003). Principes de programmation par contraintes . La presse de l'Universite de Cambridge. ISBN 0-521-82583-0. ISBN  0-521-82583-0
• Marriott, Kim ; Peter J. Stuckey (1998). Programmation avec contraintes : Une introduction . Presse MIT. ISBN  0-262-13341-5
• Frühwirth, Thom; Slim Abdennadher (2003). L'essentiel de la programmation par contraintes . Springer. ISBN 3-540-67623-6. ISBN  3-540-67623-6
• Jaffar, Joxan ; Michael J. Maher (1994). "Programmation en logique de contraintes : une enquête" . Journal de programmation logique . 19/20 : 503-581. doi : 10.1016/0743-1066 (94) 90033-7 .
• Colmerauer, Alain (1987). "L'ouverture de l'univers Prolog III". Octet . Août.

Les références