# Une sémantique opérationnelle pour les QCHR

Igor Stéphan, Vincent Barichard

► To cite this version:

Igor Stéphan, Vincent Barichard. Une sémantique opérationnelle pour les QCHR. 16èmes Journées d'Intelligence Artificielle Fondamentale (JIAF 2022), PFIA 2022, Jun 2022, Saint-Étienne, France. hal-04031272

HAL Id: hal-04031272

https://univ-angers.hal.science/hal-04031272

Submitted on 15 Mar 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Une sémantique opérationnelle pour les QCHR

Igor Stéphan¹ Vincent Barichard¹

¹ LERIA, Université d'Angers, France

igor.stephan@univ-angers.fr vincent.barichard@univ-angers.fr

## Abstract

Nous passons du formalisme QCSP (Quantified Constraint Satisfaction Problems) à QCHR (Quantified Constraint Handling Rules) en permettant la construction d'un lieu dynamique et l'utilisation de contraintes définies par l'utilisateur. QCSP offre un cadre naturel pour exprimer les problèmes PSPACE comme des jeux finis à deux joueurs. Pour définir un modèle QCSP, le lieu doit être connu au préalable et ne peut pas être construit dynamiquement même si le pire cas ne se produira pas. Pour surmonter ce problème, nous définissons le nouveau formalisme QCHR qui permet de construire le lieu dynamiquement pendant la résolution. Nos modèles QCHR présentent d'excellentes performances lorsque le lieu est statique et surpassent les approches QCSP lorsque le lieu est dynamique. Cet article présente une sémantique opérationnelle sous la forme d'un ensemble de règles de transition, très proche de l'implantation effective, par extension de la sémantique opérationnelle de CHR (Constraint Handling Rules).

## 1 Introduction

Le passage du formalisme des QCSP (pour *Quantified Constraint Satisfaction Problems*) à celui de QCHR (pour *Quantified Constraint Handling Rule*) est motivé par les difficultés de développement d'applications réelles en QCSP. Une sémantique formelle de QCHR ainsi qu'une preuve de concept utilisant un système de calcul des séquents est présenté dans [4]. Dans ce présent article, nous définissons une sémantique opérationnelle décrivant précisément le fonctionnement de la résolution d'un QCHR.

QCSP [8, 25, 17, 5, 23, 21, 3] est une généralisation des problèmes de satisfaction de contraintes (CSP) dans lesquels les variables peuvent être quantifiées existentiellement (comme dans CSP) mais également universellement. Un QCSP est une alternance de variables quantifiées existentiellement et universellement sur des domaines finis, appelé le lieu, suivi d'un CSP. Les variables universellement quantifiées représentent des paramètres incontrôlables tels que les événements météorologiques. Un QCSP peut être

vu comme un jeu à deux joueurs dans lequel les variables existentiellement quantifiées représentent un joueur A et les variables universellement quantifiées représentent un joueur B.

QCSP+ [5], une extension de QCSP, a été proposée pour faciliter la modélisation des jeux à deux joueurs. QCSP+ utilise des séquences de quantifications restreintes au lieu des séquences de quantifications standards. Un QCSP/QCSP+ est valide si le joueur A a une stratégie pour gagner, c'est-à-dire une stratégie pour fixer les variables existentiellement quantifiées telle que, quel que soit le paramètre choisi par le joueur B, le CSP sous-jacent est satisfait. QCSP/QCSP+ est un cadre de modélisation riche qui conduit à une modélisation succincte. Mais cette extension augmente également la complexité de la résolution de NP-complet à PSPACE-complet. Pour intégrer un problème réel dans un QCSP/QCSP+, il faut modéliser chaque partie du problème et tout doit être énoncé a priori. Certains problèmes (tic-tac-toe, reversi, puissance-4) répondent à cette exigence, mais d'autres (dames, échecs) ne le font pas. QCSP/QCSP+ ne peut pas être utilisé pour modéliser des jeux et des problèmes dont le nombre de coups n'est pas connu à priori. De plus, même si tout peut être énoncé statiquement, le modèle QCSP implique tous les coups possibles et sureste le nombre de coups dans le pire des cas. Par exemple, il est difficile d'encoder des jeux tels que certaines règles contraignent les coups futurs en fonction des coups passés [6] : la résolution d'un QCSP cherchera des solutions pour tous les coups possibles du joueur B, alors que certains d'entre eux ont été rendus impossibles par les coups précédents. Lorsqu'un QCSP/QCSP+ est défini, la résolution repose sur un solveur QCSP [17, 3, 25]. Ce solveur est un programme boîte noire qui résout une instance d'un modèle donné. Comme la plupart des solveurs QCSP/QCSP+ sont basés sur des solveurs CSP, il n'y a pas de moyen facile d'aider et guider le processus de résolution en prenant en compte les propriétés spécifiques d'un problème quantifié. Dans ce travail, nous utilisons un nouveau cadre pour modéliser les problèmes quantifiés d'une manière dynamique.
CHR (pour Constraint Handling Rules) [11, 12, 16, 13, 14, 15] est un langage à base de règles d'inférence à chaînage avant qui remplacent les contraintes du problème par d'autres plus simples jusqu'à la résolution complète. Chaque règle est composée d'une tête (un ensemble de contraintes devant exister dans un store d'éléments pour déclencher la règle), d'une garde (conditions à remplir, comme la valeur d'un paramètre d'une des contraintes capturées par la tête, pour exécuter la règle) et d'un corps (liste de contraintes à ajouter lorsque la règle est déclenchée). CHR est un langage dont l'objectif est de manipuler des contraintes déclaratives au sens de la programmation logique par contraintes [18, 19, 20]. CHR est une extension qui permet d'introduire des contraintes définies par l'utilisateur, c'est-à-dire des prédicats du premier ordre, dans un langage hôte donné comme Prolog, Lisp, Java, ou C/C++. CHR définit la simplification des contraintes définies par l'utilisateur, qui remplace les contraintes par des contraintes plus simples tout en préservant l'équivalence logique. CHR définit également la propagation des contraintes définies par l'utilisateur qui ajoute de nouvelles contraintes; ces contraintes sont logiquement redondantes mais peuvent entraîner des simplifications supplémentaires. CHR permet d'utiliser des gardes qui sont des séquences d'instructions du langage hôte définissant des conditions à satisfaire pour déclencher la règle. CHR définit enfin la simpagation sur les contraintes définies par l'utilisateur qui mélange et subsume la simplification et la propagation. Les règles de CHR (simpagation) sont appliquées sur des multi-ensembles de contraintes. L'application répétée de ces règles sur un multi-ensemble de contraintes initiales résout incrémentalement ces contraintes. Le principe du chaînage avant exprime un non-déterminisme don't care, permettant des implémentations efficaces.

CHR<sup>V</sup> [1] est une extension de CHR introduisant le don't know non-déterminisme [7]. Ce non-déterminisme est offert gratuitement lorsque le langage hôte est Prolog. Ce non-déterminisme permet de spécifier facilement des problèmes de la classe de complexité NP mais ce n'est pas le cas pour le reste de la Hiérarchie Polynomiale et, en général, tout problème exprimé avec des quantifications alternées (bien que le formalisme soit Turing-complet).

Cet article reprend le formalisme QCHR (pour Quantified Constraint Handling Rules) dans lequel la règle de simpagation est étendue à une règle de simpagation existentielle mais aussi à une règle de simpagation universelle. La simpagation existentielle (resp. universelle) a les mêmes conditions pour être appliquée qu'une règle de simpagation mais le corps est existentiellement (resp. universellement) quantifié sur une variable et un domaine (fini). Nous obtenons un formalisme pour lequel il n'est pas nécessaire de déclarer à priori l'alternance des quantificateurs mais où les quantificateurs sont générés quand ils sont nécessaires. Cette propriété offre une facilité de programmation

par rapport à QCSP/QCSP+ où il faut toujours déclarer un lieu fini. Avec QCHR, nous pouvons spécifier certains jeux potentiellement infinis par récursion.

Le nouveau cadre des QCHR a été défini dans [4] par une sémantique exprimée sous la forme d'un calcul des séquents directement issu d'une sémantique, exprimée elle aussi dans ce formalisme venant de la théorie de la preuve, mais pour CHR. Dans ce présent article, nous donnons une autre sémantique, que nous prouvons comme étant équivalente à la première, sous une forme opérationnelle basée sur la notion d'état et de transition, comme une extension de la sémantique opérationnelle $\omega_r$ de CHR [10] qui décrit de manière fine le fonctionnement du langage au plus près de son implantation dans son langage hôte, le C++.

La section 2 présente intuitivement la syntaxe de notre formalisme QCHR, illustre sur deux exemples emblématiques pourquoi il n'est pas toujours approprié de modéliser et résoudre avec QCSP/QCSP+, et montre la facilité de modélisation et l'efficacité de résolution de notre nouveau formalisme. La section 3 présente notre proposition, le langage QCHR : en premier lieu, sa syntaxe et en second lieu sa sémantique opérationnelle. La section 4 présente une discussion sur le lien entre QCHR et d'autres travaux connexes ainsi que des liens vers l'implémentation et des expérimentations déjà réalisées. La section 5 conclut et trace quelques perspectives.

## 2 Exemples motivant notre approche

Notre objectif principal est de pouvoir modéliser des problèmes quantifiés lorsque le lieu peut être construit dynamiquement pendant la résolution. Deux problèmes bien connus sont utilisés comme fil conducteur : le jeu Nim et le Puissance 4. De manière informelle, le formalisme CHR est étendu avec deux nouvelles règles : la règle existentielle (simpagation QCHR)

$$K_1, \dots, K_m \setminus D_1, \dots, D_n < \exists> \{it, inf, sup\} \text{garde} \mid \Omega^B$$

et la règle universelle (simpagation QCHR)

$$K_1, \dots, K_m \setminus D_1, \dots, D_n < \forall> \{it, inf, sup\} \text{garde} \mid \Omega^B$$

La tête $(K_1, \dots, K_m \setminus D_1, \dots, D_n)$, le corps $\Omega^B$ et la garde de ces règles sont interprétés de la même manière que dans le formalisme CHR : Les contraintes $K_1, \dots, K_n$ sont conservées comme dans la propagation et les contraintes $D_1, \dots, D_m$ sont supprimées comme dans la simplification; les contraintes du corps $\Omega^B = B_1, \dots, B_p$ sont les contraintes ajoutées; si $\Omega^B = true$, rien n'est ajouté; si $\Omega^B = false$, le calcul échoue (true et false sont deux symboles réservés). Les deux symboles inf et sup désignent, respectivement, la borne inférieure et la borne supérieure d'un intervalle entier. La variable it est censée apparaître dans le corps $\Omega^B$. La sémantique informelle de ces règles est la
suivante : Le corps $\Omega^B$ de la règle existentielle conduit à un succès (resp. un échec) si au moins une valeur (resp. toutes les valeurs) $v$ prise dans l'intervalle $[inf..sup]$ conduit le corps $[it \leftarrow v](\Omega^B)$ (où les occurrences de $it$ dans $\Omega^B$ sont remplacées par $v$) à un succès (resp. un échec). De la même manière, le corps $\Omega^B$ de la règle universelle conduit à un succès (resp. un échec) si toutes les valeurs (resp. au moins une valeur) $v$ prises dans l'intervalle $[inf..sup]$ conduisent le corps $[it \leftarrow v](\Omega^B)$ à un succès (resp. un échec). Si une règle QCHR existentielle (resp. universelle) conserve toutes les contraintes de sa tête multiple, c'est une règle de propagation existentielle (resp. universelle) et elle est notée $(K_1, \dots, K_m) \exists> \{it, inf, sup\} garde | \Omega^B$ (resp. $(K_1, \dots, K_m) \forall> \{it, inf, sup\} garde | \Omega^B$) ; si une règle QCHR existentielle (resp. universelle) ne conserve aucune des contraintes de sa tête multiple, il s'agit d'une règle de simplification existentielle (resp. universelle) et elle est notée $(D_1, \dots, D_n) \langle \exists> \{it, inf, sup\} garde | \Omega^B$) (resp. $(D_1, \dots, D_n) \langle \forall> \{it, inf, sup\} garde | \Omega^B$).

**Le jeu de Nim.** Le jeu de Nim est un jeu à deux joueurs qui se joue avec un tas de pièces ou d'allumettes. Le but du jeu est de prendre la dernière allumette. Chaque joueur peut prendre de une à trois allumettes. Dans la variante Fibonacci, le nombre minimum est d'une allumette et le maximum au premier tour de jeu est d'une allumette de moins que le nombre initial d'allumettes. Ensuite, chaque joueur peut prendre de un à deux fois plus d'allumettes que l'adversaire au tour de jeu précédent. Le joueur A commence. Par exemple, avec 4 allumettes, le joueur A prend 1 allumette. Ensuite, le joueur B peut prendre 3 allumettes mais s'il le fait, il perd immédiatement puisque le coup n'est pas autorisé. Le joueur B peut donc prendre 1 ou 2 allumettes. Mais quoi qu'il prenne, il perd puisque le joueur A prendra les allumettes restantes. La partie la plus longue possible a 4 tours : chaque joueur prend une allumette à chaque tour de jeu. Ainsi, le QCSP a 4 quantificateurs puisque le lieu est défini statiquement. Avec un nombre pair $p$ d'allumettes, la spécification QCSP est la suivante ($x_i$, resp. $y_i$, correspond au nombre d'allumettes choisies par le joueur A, resp. B, au tour $i$) : $R_A(1)$ est vrai (le joueur A choisit entre 1 et $p-1$ allumettes) et pour tous les $i$, $1 < i \le \frac{p}{2}$, $R_A(i) = (1 \le x_i \le 2*y_{i-1}) \land (x_i + \sum_{j \le i} (x_j + y_j) \le p)$ et pour tout $i$, $1 \le i \le \frac{p}{2}$, $R_B(i) = (1 \le y_i \le 2*x_i) \land (\sum_{j \le i} (x_j + y_j) \le p)$ (chaque joueur prend de un à deux fois plus d'allumettes que l'adversaire au tour précédent) [3] :

$$ \exists x_1 \forall y_1 \dots \exists x_{\frac{p}{2}} \forall y_{\frac{p}{2}} \exists o_1 \dots \exists o_{\frac{p}{2}} \\ R_A(1) \land (R_B(1) \rightarrow o_1) \land (o_1 \leftrightarrow (R_A(2) \land o_2)) \land \\ (o_2 \leftrightarrow (R_B(2) \rightarrow o_3)) \land \dots \land (o_{\frac{p}{2}} \leftrightarrow (R_B(\frac{p}{2}) \rightarrow \perp)) $$

avec $x_1, y_1, \dots, x_{\frac{p}{2}}, y_{\frac{p}{2}} \in [1..p-1]$ et $o_1, \dots, o_{\frac{p}{2}}$ des variables booléennes. Pour chaque nombre initial d'allumettes, le modèle général doit être instancié. Par exemple,

avec $p = 4$, on obtient le QCSP suivant :

$$ \exists x_1 \forall y_1 \exists x_2 \forall y_2 \exists o_1 \exists o_2 \\ ((y_1 \le 2 * x_1) \land (x_1 + y_1 \le 4)) \rightarrow o_1) \land \\ (o_1 \leftrightarrow (((x_2 \le 2 * y_1) \land (x_1 + y_1 + x_2 \le 4)) \land o_2)) \land \\ (o_2 \leftrightarrow (((y_2 \le 2 * x_2) \land (x_1 + y_1 + x_2 + y_2 \le 4)) \rightarrow \perp)) $$

avec $x_1, y_1, x_2, y_2 \in \{1, 2, 3\}$ et $o_1, o_2$ des variables intermédiaires booléennes (permettant de décomposer le problème en plusieurs contraintes réifiées). Ce QCSP est valide si le premier joueur a une stratégie pour choisir les valeurs des variables existentiellement quantifiées telle que, quelle que soit le choix de l'adversaire pour ses variables universelle-ment quantifiées, ce premier joueur gagne (c'est-à-dire que le CSP est vrai).

Le programme QCHR suivant résout le jeu Nim avec la variante Fibonacci d'un nombre pair ou impair d'allumettes ($N$ représente deux fois le nombre d'allumettes choisies par un joueur et $R$ représente le nombre restant d'allumettes dans le tas) :

$$ \begin{aligned} u &@nfB(N, R) \langle \forall \rangle \{it, 1, \min(N, R)\} nfA(2 * it, R - it) \\ e &@nfA(N, R) \langle \exists \rangle \{it, 1, \min(N, R)\} nfB(2 * it, R - it) \end{aligned} $$

Ces règles sont construites de la même manière : ce sont des règles de simplification existentielles/universelles avec une garde vide (omise). Le nom (optionnel) de la règle est séparé du reste de la règle par le symbole $@$. Deux contraintes $nfA(\cdot, \cdot)$ et $nfB(\cdot, \cdot)$ sont utilisées pour mémoriser les informations d'un tour du jeu. À chaque exécution d'une des deux règles, la contrainte identifiée par la tête est supprimée, puis une nouvelle est postée dans le corps. Les paramètres du quantificateur ($\forall$ ou $\exists$) donnent la définition des bornes inférieure et supérieure, et le corps qui exprime que si un joueur a choisi de prendre $it$ allumettes, son adversaire ne peut choisir qu'entre 1 et $\min(2 * it, R)$ allumettes. Le premier joueur peut choisir librement entre 1 et le nombre initial d'allumettes moins 1 :

$$ l@nim_fibo(R) \Rightarrow nfA(R - 1, R) $$

Le lieu n'est pas défini statiquement comme pour un QCSP mais dynamiquement. Notons que le cas d'arrêt de la récursion est caché dans la sémantique de la règle universelle lorsque la borne inférieure devient plus grande que la borne supérieure.

**Le jeu de Puissance 4.** Le jeu de Puissance 4 est un jeu à deux joueurs dans lequel les joueurs choisissent d'abord une couleur. Il se joue sur une grille suspendue verticale-ment. À chaque tour, un joueur choisit une colonne de la grille et laisse tomber une pièce de sa couleur à partir du haut de celle-ci. Les pièces tombent directement vers le bas, occupant l'emplacement le plus bas disponible dans la colonne. Le gagnant est le premier joueur à former une ligne horizontale, verticale ou diagonale de quatre de ses propres pièces.
Le jeu de Puissance 4 peut également être modélisé par un QCSP. Afin de modéliser tous les déroulements possibles, une grille est construite pour chaque tour de jeu. Il y a autant de tours de jeu qu'il y a d'emplacements dans la grille. Par conséquent, le modèle QCSP implique nombre de lignes × nombre de colonnes grilles liées entre elles par des contraintes (voir [22] pour plus de détails sur le modèle QCSP). De plus, des contraintes doivent être ajoutées pour détecter les colonnes pleines, les coups invalides et les grilles gagnantes. Mais, même si un QCSP peut être utilisé, le lieu est dynamique (un joueur peut gagner la partie sans remplir complètement le plateau) et le modèle statique est volumineux et difficilement compréhensible. En comparaison, le modèle QCHR est plus adapté, plus léger et plus lisible. Soit NC le nombre de colonnes de la grille. Le modèle QCHR suivant calcule une stratégie gagnante si une telle stratégie existe :

$$
\begin{align*}
\mathit{if}\_{\perp} @ \mathit{ifRule}(\perp, N) &\Leftrightarrow \mathit{coin}(N), \mathit{cfe}(\mathit{isWon}(N)) \\
u_{\top} @ \mathit{cfu}(\top) &\Leftrightarrow \mathit{true} \\
u_{\perp} @ \mathit{cfu}(\perp) &< \forall> \{it, 1, NC\} \mathit{ifRule}(\mathit{isFull}(it), it) \\
e_{\top} @ \mathit{cfe}(\top) &\Leftrightarrow \mathit{false} \\
e_{\perp} @ \mathit{cfe}(\perp) &< \exists> \{it, 1, NC\} \mathit{coin}(it), \mathit{cfu}(\mathit{isWon}(it))
\end{align*}
$$

où coin(), isFull() et isWon() sont des prédicats intégrés (fonctions implémentées dans le langage hôte) déjà définies : coin() place une pièce dans la colonne donnée et génère un échec si la colonne est pleine ; isFull() renvoie $\top$ si la colonne est pleine et $\perp$ sinon ; isWon() renvoie $\top$ si un alignement de quatre pièces est trouvé et $\perp$ sinon. Ces fonctions analysent une grille qui est remplie en fonction des déplacements des joueurs.

Le lieu n'est pas défini statiquement comme pour QCSP mais dynamiquement. Par conséquent, la taille du lieu est égale au nombre de coups effectués pendant la partie et non au pire cas possible.

## 3 Le langage QCHR

Une contrainte est considérée comme un prédicat du premier ordre. Seuls trois types de contraintes prédéfinies sont nécessaires : true, false et la contrainte d'égalité syntaxique désignée par $\dagger$, avec une théorie de l'égalité désignée ET pour les variables et les constantes<fnref n="1" />. Pour deux séquences de contraintes $K_1, \dots, K_m \dagger k_1, \dots, k_m$ signifie $K_1 \dagger k_1, \dots, K_m \dagger k_m$ et pour deux contraintes $c(t_1, \dots, t_n) \dagger c(s_1, \dots, s_n)$ signifie $t_1 \dagger s_1, \dots, t_n \dagger s_n$.

### 3.1 Syntaxe de QCHR

Le formalisme QCHR est défini comme suit : une règle QCHR est une règle de la forme $(k_1, \dots, k_m, d_1, \dots, d_n, b_1, \dots, b_p)$ des contraintes utilisateur; $\inf$ et $\sup$ des entiers; it une variable entière; garde une séquence d'instructions dans le langage hôte ou des égalités) :

[Règle de simpagation]

$$ (k_1, \dots, k_m \setminus d_1, \dots, d_n \Leftrightarrow \text{garde} | \Omega^B) $$

avec $n \ge 0$ et $m \ge 0$,

[Règle de simpagation existentielle]

$$ (k_1, \dots, k_m \setminus d_1, \dots, d_n < \exists> \{it, \inf, \sup\} \text{garde} | \Omega^B) $$

avec $n \ge 0$ et $m \ge 0$,

[Règle de simpagation universelle]

$$ (k_1, \dots, k_m \setminus d_1, \dots, d_n < \forall> \{it, \inf, \sup\} \text{garde} | \Omega^B) $$

avec $n \ge 0$ et $m \ge 0$.

$$ \text{et } \Omega^B = b_1, \dots, b_p \text{ avec } p > 0 \text{ ou true ou false.} $$

Une règle de propagation (resp. simplification) est un cas particulier de la règle de simpagation où l'ensemble $\{d_1, \dots, d_n\}$ (resp. $\{k_1, \dots, k_m\}$) est vide. Ceci est vrai également pour les règles de simpagation existentielles et universelles.

### 3.2 La sémantique $\omega_r^{\exists\forall}$

Notre système de transitions est basé sur les états d'exécution de [10] pour CHR.

**Definition 3.1 (État d'exécution)** Une contrainte identifiée A\#i (ou token) est une contrainte A définie par l'utilisateur avec un certain entier unique i, son identité. Un token $<\exists\Omega^B>$ et un token $<\forall\Omega^B>$ sont composés (dans cet ordre) d'une variable entière, de deux entiers (les bornes inférieure et supérieure) et d'une séquence de contraintes définies par l'utilisateur. Une contrainte numérotée A\#i:o est une contrainte identifiée A\#i avec un entier unique o fonction de i. Un état d'exécution est soit un des symboles réservés : Failure et Success, soit un tuple $\langle\Omega, S, H\rangle_c$ où $\Omega$ (le but actuel) représente une séquence de contraintes (numérotées) ou de contraintes définies par l'utilisateur ou false, S (le store actuel) représente un multi-ensemble de contraintes identifiées, H (l'historique courant) représente un ensemble de mots, chacun enregistrant le nom d'une règle et les identités des contraintes identifiées, c représente un compteur qui identifie le prochain nombre entier libre pouvant être utilisé pour numéroter une contrainte identifiée.

**Definition 3.2 (Continuation d'exécution)** Un lieu est une séquence de $\exists$ et de $\forall$. Une continuation de décision est une séquence d'états d'exécution. Une continuation d'exécution est une paire $\mathcal{B}\Sigma$ où $\mathcal{B}$ est un lieu et $\Sigma$ est une continuation de décision.

<footnote n="1">1. Nous n'utilisons pas de symboles fonctionnels mais le langage est plus riche que les simples variables et constantes puisqu'on peut utiliser les instructions du langage hôte qui sont évaluées avant que l'égalité ne soit appliquée sur une expression complètement instanciée. C'est le cas pour les opérations arithmétiques dans la modélisation du jeu Nim ou pour des fonctions plus ad hoc comme isFull et isWon dans la modélisation du jeu du Puissance 4.</footnote>
Pour un but initial $\Omega$, la continuation d'exécution initiale est $[\langle\Omega, \emptyset, \emptyset\rangle_1]$.

La sémantique opérationnelle $\omega_r^{\exists\forall}$ est basée sur un ensemble de règles de transition qui font correspondre une continuation d'exécution à une autre. Les six premières règles<fnref n="2" /> sont des extensions directes des règles de transition de la sémantique $\omega_r$ [10] pour CHR : le lieu est ignoré et le premier état d'exécution de la continuation d'exécution est considéré comme un état d'exécution de $\omega_r$.

### 3.3 Extension de la sémantique $\omega_r$

Les règles de transition suivantes [Activate], [Reactivate], [Drop], [Simplify], [Propagate], et [Default] sont des extensions directes des règles de transition $\omega_r$ de [10]. Dans ce qui suit, certaines contraintes (A, $k_1, \dots, k_m, d_1, \dots, d_n$), des ensembles de token (S, $S^K$, $S^D, \dots$), des séquences de contraintes ($\Omega, \Omega^B$) et certains ensembles d'historique ($H, H'$) sont utilisés, un lieu $\mathcal{B}$ peut être vide. Le but est composée d'une séquence de contraintes donnée sous forme de liste en intention ([tête | queue]) ou en extension. La majorité des règles suivantes sont illustrées dans l'exemple 3.1.

**La règle de transition [Activate] :**

$$ \mathcal{B}[\langle[A | \Omega], S, H\rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle[A\#c : 1 | \Omega], \{A\#c\} \uplus S, H\rangle_{c+1} | \Sigma] $$

La règle de transition [Activate] active la première contrainte A du but $[A | \Omega]$. A est identifié par $c$ (le prochain identifiant libre), ajouté au store de contraintes $S$ et numéroté par 1 avant d'être remplacé dans le but. Le prochain identifiant libre est incrémenté. La règle de transition [Activate] prépare la contrainte A qui est prête à être testée avec sa première occurrence dans la tête des règles du programme.

**La règle de transition [Reactivate] :**

$$ \mathcal{B}[\langle[A\#i | \Omega], S, H\rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle[A\#i : 1 | \Omega], S, H\rangle_c | \Sigma] $$

Lorsqu'une contrainte A n'est pas supprimée par une règle du programme, elle reste dans le store de contraintes. Si un de ses paramètres est mis à jour (par exemple lorsque deux variables logiques sont placées dans la même classe d'équivalence), la contrainte A est réactivée et placée au début du but. La règle de transition [Reactivate] prépare la contrainte identifiée $A\#i$ et la numérote avec 1 afin d'être prête à être testée avec sa première occurrence dans la tête des règles du programme.

**La règle de transition [Drop] :**

$$ \mathcal{B}[\langle[A\#i : o | \Omega], S, H\rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle\Omega, S, H\rangle_c | \Sigma] $$

La règle de transition [Drop] supprime la contrainte identifiée $A\#i$ du but si elle n'a pas d'o-ième occurrence dans le programme. A reste toujours dans le store de contraintes $S$ et peut être réactivé si nécessaire.

**La règle de transition [Simplify] :** Si la o-ième occurrence de la contrainte A correspond à $d_j$ dans une règle de simpagation

$$ r@ (k_1, \dots, k_m \setminus d_1, \dots, d_{j-1}, d_j, d_{j+1}, \dots, d_n \Leftrightarrow \Omega^B) $$

du programme, alors

$$ \mathcal{B}[\langle[A\#i : o | \Omega], \{A\#i\} \uplus S^K \uplus S^{D^1} \uplus S^{D^2} \uplus S, H\rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle\Omega^B \oplus \Omega, S^K \uplus S, H'\rangle_c | \Sigma] $$

avec

- $r$ le nom (optionnel) de la règle;

- $S^K = \{K_1\#i_1, \dots, K_m\#i_m\}$,
  $S^{D^1} = \{D_1\#i_{m+1}, \dots, D_{j-1}\#i_{m+j-1}\}$,
  $S^{D^2} = \{D_{j+1}\#i_{m+j+1}, \dots, D_n\#i_{m+n}\}$ tels que :
  - $K_1, \dots, K_m \doteq k_1, \dots, k_m$
  - $D_1, \dots, D_{j-1} \doteq d_1, \dots, d_{j-1}$
  - $D_{j+1}, \dots, D_n \doteq d_{j+1}, \dots, d_n$
  - $A \doteq d_j$
- $H' = H$

La règle de transition [Simplify] applique une règle de simpagation si sa tête correspond à certaines contraintes du store de contraintes. Les (ensembles de) token $S^{D^1}, S^{D^2}$ et $A\#i$ sont supprimés du store de contraintes, $A\#i$ est supprimé du but tandis que $\Omega^B$, le corps de la règle, est ajouté au but. L'historique reste le même puisque la règle ne sera plus jamais déclenchée avec le même ensemble de token (les (ensembles de) token $S^{D^1}, S^{D^2}$ et $A\#i$ ayant été supprimés).

**La règle de [Propagate] :** Si la o-ième occurrence de la contrainte A correspond à $k_j$ dans une règle de simpagation

$$ r@ (k_1, \dots, k_{j-1}, k_j, k_{j+1}, \dots, k_m \setminus d_1, \dots, d_n \Leftrightarrow \Omega^B) $$

du programme alors (avec $S^K = S^{K^1} \uplus S^{K^2}$)

$$ \mathcal{B}[\langle[A\#i : o | \Omega], \{A\#i\} \uplus S^K \uplus S^{D^1} \uplus S, H\rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle\Omega^B \oplus [A\#i : o | \Omega], \{A\#i\} \uplus S^K \uplus S, H'\rangle_c | \Sigma] $$

avec

- $r$ le nom (optionnel) de la règle;

- $S^{K^1} = \{K_1\#i_1, \dots, K_{j-1}\#i_{j-1}\}$,
  $S^{K^2} = \{K_{j+1}\#i_{j+1}, \dots, K_m\#i_m\}$,
  $S^D = \{D_1\#i_{m+1}, \dots, D_n\#i_{m+n}\}$ tels que :
  - $K_1, \dots, K_{j-1} \doteq k_1, \dots, k_{j-1}$
  - $K_{j+1}, \dots, K_m \doteq k_{j+1}, \dots, k_m$

<footnote n="2">2. Puisque nous ne considérons pas la contrainte construite, nous n'avons pas la transition [Solve] de la sémantique $\omega_r$.</footnote>
— $D_1, \dots, D_n \doteq d_1, \dots, d_n$

— $A \doteq k_j$

— $H' = H$ if ($n \neq 0$)

— $\{\text{r.i.i}_1 \dots \text{r.i}_m \notin H \text{ and } H' = H \cup \{\text{r.i.i}_1 \dots \text{r.i}_m\} \text{ si } (n=0)$

La règle de transition [Propagate] applique une règle de simpagation si sa tête correspond à certaines contraintes du store de contraintes. De plus, si la règle est une règle de propagation (c'est-à-dire ($n=0$)), nous devons être sûrs que la règle n'a pas été déclenchée auparavant en vérifiant $\text{r.i.i}_1 \dots \text{r.i}_m \notin H$. Les contraintes à supprimer $S^D$ sont supprimées du store de contraintes et $\Omega^B$, le corps de la règle, est ajouté au but. Pour une règle de propagation, l'historique est mis à jour avec $\text{r.i.i}_1 \dots \text{r.i}_m$, sinon, il reste identique.

**La règle de transition [Default] :**

$$ \mathcal{B}[\langle [A\#i : o | \Omega], S, H \rangle_c | \Sigma] $$

$$ \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle [A\#i : o + 1 | \Omega], S, H \rangle_c | \Sigma] $$

La règle de transition [Default] met à jour la contrainte active du but. Elle incrémente son nombre d'occurrences afin d'être prête pour la règle de transition suivante.

## 3.4 Règles de transition pour la quantification existentielle

**La règle de transition [∃ - Simplify] :** Si la o-ième occurrence de la contrainte A correspond à la contrainte $d_j$ dans une règle de simpagation existentielle

$$ r@k_1, \dots, k_m \setminus d_1, \dots, d_{j-1}, d_j, d_{j+1}, \dots, d_n \quad \langle \exists \rangle \{it, inf, sup\} \Omega^B $$

du programme et $inf \le sup$ alors

$$ \mathcal{B}[\langle [A\#i : o | \Omega], \{A\#i\} \uplus S^K \uplus S^{D^1} \uplus S^{D^2} \uplus S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle [\langle \exists \rangle (it, [inf, sup], \Omega^B)|\Omega], S^K \uplus S, H' \rangle_c | \Sigma] $$

avec les mêmes conditions que la règle de transition [Simplify].

La règle de transition [∃ - Simplify] applique une règle de simpagation existentielle si les contraintes de sa tête correspondent à des token du store. Les (ensembles de) token $S^D$, $S^{D^2}$ et $A\#i$ sont éliminés du store; de plus, le token $A\#i$ est effacé du but. Un nouveau niveau existentiel est ajouté au lieur $\mathcal{B}$ et un token $\langle \exists \Omega^B \rangle$ est ajouté au but. Ce token $\langle \exists \Omega^B \rangle$ est prêt à être déplié par la règle de transition [∃ - Unfolding]. L'historique demeure le même puisque la règle ne pourra jamais être déclenchée avec le même ensemble de token (les (ensembles de) token $S^D$, $S^{D^2}$ et $A\#i$ ayant été supprimés).

**La règle de transition [∃ - Propagate] :** Si la o-ième occurrence de la contrainte A correspond à la contrainte $k_j$ d'une règle de simpagation existentielle

$$ r@k_1, \dots, k_{j-1}, k_j, k_{j+1}, \dots, k_m \setminus d_1, \dots, d_n \quad \langle \exists \rangle \{it, inf, sup\} \Omega^B $$

du programme et $inf \le sup$ ($S^K = S^{K^1} \uplus S^{K^2}$) alors

$$ \mathcal{B}[\langle [A\#i : o | \Omega], \{A\#i\} \uplus S^K \uplus S^D \uplus S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle [\langle \exists \rangle (it, [inf, sup], \Omega^B)|\Omega], S^K \uplus S, H' \rangle_c | \Sigma] $$

avec les mêmes conditions que la règle de transition [Propagate].

La règle de transition [∃ - Propagate] applique une règle de simpagation existentielle si les contraintes de sa tête correspondent à des token du store. De plus, si la règle est une règle de propagation (c'est-à-dire ($n=0$)), nous devons être sûrs que la règle n'a pas déjà été déclenchée auparavant en vérifiant que $\text{r.i.i}_1 \dots \text{r.i}_m \notin H$. Les token de l'ensemble $S^D$ sont éliminées du store. Un nouveau niveau existentiel est ajouté au lieur $\mathcal{B}$ et un token $\langle \exists \Omega^B \rangle$ est ajouté au but. Ce token $\langle \exists \Omega^B \rangle$ est prêt à être déplié par la règle de transition [∃ - Unfolding]. Pour une règle de propagation, l'historique est mis-à-jour avec $\text{r.i.i}_1 \dots \text{r.i}_m$, sinon, il reste identique.

**La règle de transition [∃ - Unfolding] :** Si $inf \le sup$ alors

$$ \mathcal{B}[\langle [\langle \exists \rangle (it, [inf, sup], \Omega^B)|\Omega], S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle [it \leftarrow inf](\Omega^B), S, H \rangle_c, \langle [\langle \exists \rangle (it, [inf + 1, sup], \Omega^B)|\Omega], S, H \rangle_c | \Sigma] $$

La règle de transition [∃ - Unfolding] déplie le token $\langle \exists \Omega^B \rangle$ d'une étape. Une telle étape consiste en l'extraction et la vérification du corps $\Omega^B$ dans lequel la variable locale it est substituée par la borne inférieure inf du domaine du token $\langle \exists \Omega^B \rangle$; elle ajoute aussi au but $\Omega$ un nouveau token $\langle \exists \Omega^B \rangle$ avec une borne inférieure incrémentée. Ce nouveau token $\langle \exists \Omega^B \rangle$ sera déplié si $[it \leftarrow inf](\Omega^B)$ échoue.

**La règle de transition [∃ - Failure] :** Si $inf > sup$ alors

$$ \mathcal{B}[\langle [\langle \exists \rangle (it, [inf, sup], \Omega^B)|\Omega], S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[Failure | \Sigma] $$

La règle de transition [∃ - Failure] s'applique si $inf > sup$ et si les token $\langle \exists \Omega^B \rangle$ dépliés échouent. Cela clôt et élimine le niveau courant du lieur. En éliminant le niveau courant du lieur, le token $\langle \exists \Omega^B \rangle$ et le reste du but $\Omega$ sont aussi éliminés et l'état d'exécution Failure prend la place de l'état d'exécution courant.

**Le règle de transition [∃ - SuccessPropagate] :**

$$ \mathcal{B}[Success, \langle [\langle \exists \rangle (it, [inf, sup], \Omega^B)|\Omega], S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle \Omega, S, H \rangle_c | \Sigma] $$

La règle de transition [∃ - SuccessPropagate] s'applique lorsque qu'un corps $\Omega^B$ déplié est un succès (c-à-d l'état d'exécution Success est rencontré). La règle de transition [∃ - SuccessPropagate] clôt et élimine le niveau courant du lieur. Comme le token $\langle \exists \Omega^B \rangle$ réussit, le reste du but $\Omega$ doit être poursuivi au niveau supérieur du lieur.
**La règle de transition $[\exists - FailurePropagate]$ :**

$$ \mathcal{B}\exists[\mathit{Failure}|\Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}\exists\Sigma $$

La règle de transition $[\exists - FailurePropagate]$, lorsqu'un corps $\Omega^B$ déplié est un échec (c'est-à-dire l'état d'exécution $\langle [it \leftarrow inf](\Omega^B), S, H \rangle_c$ s'est réécrit en l'état d'exécution *Failure*), poursuit le parcours des éléments de la quantification existentielle (car alors $\Sigma = [\langle \langle \exists \rangle (it, [inf + 1, sup], \Omega^B)|\Omega], S, H \rangle_c | \_])$.

## 3.5 Règles de transition pour la quantification universelle

**La règle de transition $[\forall - Simplify]$ :** Si la o-ième occurrence de la contrainte A correspond à la contrainte $d_j$ de la règle de simpagation universelle

$$ r@k_1, \dots, k_m \setminus d_1, \dots, d_{j-1}, d_j, d_{j+1}, \dots, d_n <\forall>\{it, inf, sup\} \Omega^B $$

du programme et $inf \le sup$ alors

$$ \mathcal{B}[\langle[A\#i : o | \Omega], \{A\#i\} \uplus S^K \uplus S^{D^1} \uplus S^{D^2} \uplus S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}\forall[\langle\langle\forall\rangle(it, [inf, sup], \Omega^B)|\Omega], S^K \uplus S, H' \rangle_c | \Sigma] $$

avec les mêmes conditions que la règle de transition $[Simplify]$.

La règle de transition $[\forall - Simplify]$ applique une règle de simpagation universelle si les contraintes de sa tête correspondent à des *token du store*. Les (ensembles de) tokens $S^{D^1}$, $S^{D^2}$ et $A\#i$ sont éliminés du *store*; de plus, le *token A\#i* est éliminé du but. Un nouveau niveau universel est ajouté au lieu et un *token <\forall\Omega^B>*) est ajouté au but. Ce *token <\forall\Omega^B>*) est prêt à être déplié par la règle de transition $[\forall - Unfolding]$. L'historique demeure le même puisque la règle ne pourra jamais être déclenchée avec le même ensemble de *token* (les (ensembles de) *tokens* $S^{D^1}$, $S^{D^2}$ et $A\#i$ ayant été supprimés).

**La règle de transition $[\forall - Propagate]$ :** Si la o-ième occurrence de la contrainte A correspond à la contrainte $k_j$ d'une règle de simpagation universelle

$$ r@k_1, \dots, k_{j-1}, k_j, k_{j+1}, \dots, k_m \setminus d_1, \dots, d_n <\forall>\{it, inf, sup\} \Omega^B $$

du programme et $inf \le sup$ alors

$$ \mathcal{B}[\langle[A\#i : o | \Omega], \{A\#i\} \uplus S^{K^1} \uplus S^{K^2} \uplus S^D \uplus S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}\forall[\langle\langle\forall\rangle(it, [inf, sup], \Omega^B)|\Omega], S^K \uplus S, H' \rangle_c | \Sigma] $$

avec les mêmes conditions que la règle de transition $[Propagate]$.

La règle de transition $[\forall - Propagate]$ applique une règle de simpagation universelle si les contraintes de sa tête correspondent avec des *token du store*. De plus, si la règle est

une règle de propagation (c'est-à-dire ($n = 0$)) nous devons être sûrs que la règle n'a pas été déclenchée auparavant en vérifiant $r.i.i_1...i_m \notin H$. Un nouveau niveau universel est ajouté au lieu $\mathcal{B}$ et un *token <\forall\Omega^B>*) est ajouté au but. Ce *token <\forall\Omega^B>*) est prêt à être déplié par la règle de transition $[\forall - Unfolding]$. Pour une règle de propagation, l'historique est mis-à-jour avec $r.i.i_1...i_m$, sinon, il reste identique.

Nous remarquons que les règles de transition $[\forall - Simplify]$ et $[\forall - Propagate]$ ajoutent toutes les deux un niveau au lieu $\mathcal{B}$. Ce faisant, elles ouvrent un sous-espace pour la résolution du but actuel. Le but sera résolu et un succès ou un échec sera traité en retour. Cela correspond au concept d'arbre de recherche et d'ouverture de nœuds dans le domaine de la résolution de problèmes combinatoires.

**La règle de transition $[\forall - Unfolding]$ :**

$$ \mathcal{B}\forall[\langle\langle\forall\rangle(it, [inf, sup], \Omega^B)|\Omega], S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}\forall[\langle [it \leftarrow inf](\Omega^B), S, H \rangle_c, \langle\langle\forall\rangle(it, [inf + 1, sup], \Omega^B)|\Omega], S, H \rangle_c | \Sigma] $$

avec $inf \le sup$.

La règle de transition $[\forall - Unfolding]$ traite et fait avancer le *token <\forall\Omega^B>*) d'une étape. Une étape consiste à extraire et vérifier le corps $\Omega^B$ où la variable locale *it* est substituée par la borne inférieure *inf* du domaine du *token <\forall\Omega^B>*)*. Il ajoute également au but $\Omega$ un nouveau *token <\forall\Omega^B>*)* avec une limite inférieure incrémentée. Le nouveau *token <\forall\Omega^B>*)* sera développé si le $\Omega^B$ actuel réussit.

**La règle de transition $[\forall - Success]$ :** Avec $inf > sup$

$$ \mathcal{B}\forall[\langle\langle\forall\rangle(it, [inf, sup], \Omega^B)|\Omega], S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\langle\Omega, S, H \rangle_c | \Sigma] $$

La règle de transition $[\forall - Success]$ s'applique si $inf > sup$ ce qui signifie que tous les *token <\forall\Omega^B>*)* développés ont réussi. La règle de transition $[\forall - Success]$ ferme le niveau actuel du lieu. Comme le *token <\forall\Omega^B>*)* a réussi, le $\Omega$ restant doit être poursuivi au niveau précédent de $\mathcal{B}$.

**La règle de transition $[\forall - FailurePropagate]$ :**

$$ \mathcal{B}\forall[\mathit{Failure}, \sigma | \Sigma] \rightsquigarrow_r^{\exists\forall} \mathcal{B}[\mathit{Failure} | \Sigma] $$

La règle de transition $[\forall - FailurePropagate]$ s'applique lorsqu'un $\Omega^B$ développé a échoué. La règle de transition $[\forall - FailurePropagate]$ ferme et rejette le niveau actuel du lieu. En rejetant le niveau actuel, le *token <\forall\Omega^B>*)* et le $\Omega$ restant sont également supprimés, puis un *Failure* est placé à la place de l'appel de la contrainte au niveau supérieure précédent de $\mathcal{B}$.
**La règle de transition $[\forall - SuccessPropagate]$ :**

$$ \mathcal{B} \forall [Success | \Sigma] \rightsquigarrow_r^{\exists \forall} \mathcal{B} \forall \Sigma $$

La règle de transition $[\forall - SuccessPropagate]$, lorsqu'un corps $\Omega^B$ déplié est un succès (c'est-à-dire l'état d'exécution $\langle [it \leftarrow inf] (\Omega^B), S, H \rangle_c$ s'est réécrit en l'état d'exécution *Success*), poursuit le parcours des éléments de la quantification universelle (car alors $\Sigma = [\langle<\forall>(it, [inf + 1, sup]), \Omega^B\rangle|\Omega, S, H \rangle_c | \_])$.

## 3.6 Le but est une conjonction

**La règle de transition $[Success]$ :**

$$ \mathcal{B}[\langle \cdot, S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists \forall} \mathcal{B}[Success | \Sigma] $$

La règle de transition $[Success]$ introduit l'état d'exécution *Success* lorsqu'une suite d'exécutions a réussi. Un tel cas se produit lorsque le but de l'état d'exécution devient vide (c'est-à-dire que tous les éléments ont été traités avec succès).

**La règle de transition $[Failure]$ :**

$$ \mathcal{B}[\langle \text{false} | \Omega \rangle, S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists \forall} \mathcal{B}[Failure | \Sigma] $$

La règle de transition $[Failure]$ remplace une continuation d'exécution qui a échouée par l'état d'exécution *Failure*. Un état d'exécution échoue uniquement si une contrainte *false* est rencontrée lors du traitement du but.

**La règle de transition $[true]$ :**

$$ \mathcal{B}[\langle [true|\Omega], S, H \rangle_c | \Sigma] \rightsquigarrow_r^{\exists \forall} \mathcal{B}[\langle \Omega, S, H \rangle_c | \Sigma] $$

La plupart des règles de transition sont illustrées dans l'exemple suivant, qui applique la sémantique $\omega_r^{\exists \forall}$ au jeu du NimFibo décrit en section 2.

### Exemple 3.1

* u @ \_nfB(N, R)<\forall>{it, 1, min(N, R)}
  nfA(2 * it, R - it)

* e @ \_nfA(N, R)<\exists>{it, 1, min(N, R)}
  nfB(2 * it, R - it)

* init @ \_nim_fibo(R) ⇔ nfA(R - 1, R)

[ \langle nim_fibo(4), 0, 0 \rangle_1 ]
  \rightsquigarrow_r^{\exists \forall} [Activate]

[ \langle nim_fibo(4)#1 : 1], {nim_fibo(4)#1}, 0 \rangle_2 ] (1)

\rightsquigarrow_r^{\exists \forall} [Simplify]

[ \langle nfA(3, 4), 0, 0 \rangle_2 ] (2)

\rightsquigarrow_r^{\exists \forall} [Activate] \rightsquigarrow_r^{\exists \forall} [\exists - Simplify]

[ \langle<\exists>(i, [1, 3], nfB(2 * i, 4 - i)), 0, 0 \rangle_3 ] (4)

\rightsquigarrow_r^{\exists \forall} [\exists - Unfolding]

[ \langle nfB(2, 3), 0, 0 \rangle_3, 
    \langle<\exists>(i, [2, 3], nfB(2 * i, 4 - i)), 0, 0 \rangle_3 ] (5)

$$ \text{avec } \sigma_1^{\exists} = \langle [\langle\exists>(i, [2, 3], nfB(2 * i, 4 - i))], 0, 0 \rangle_3 \rangle $$

$$ \begin{align} \rightsquigarrow_r^{\exists \forall} & [\text{Activate}] \rightsquigarrow_r^{\exists \forall} [\forall - \text{Simplify}] \nonumber \\ \exists \forall & [ \langle [\langle\forall>(i, [1, 2], nfA(2 * i, 3 - i))], 0, 0 \rangle_4, \nonumber \\ & \qquad \sigma_1^{\exists} \rangle ] \tag{7} \end{align} $$

$$ \begin{align} \rightsquigarrow_r^{\exists \forall} & [\forall - \text{Unfolding}] \nonumber \\ \exists \forall & [ \langle [nfA(2, 2)], 0, 0 \rangle_4, \nonumber \\ & \qquad \langle[\langle\forall>(i, [2, 2], nfA(2 * i, 3 - i))], 0, 0 \rangle_4, \sigma_1^{\exists} \rangle ] \tag{8} \end{align} $$

avec

$$ \left\{ \begin{array}{l} \sigma_{1,1}^{\exists} = \langle [\langle\forall>(i, [2, 2], nfA(2 * i, 3 - i))], 0, 0 \rangle_4 \\ \sigma_{1,1,1}^{\exists} = \langle [\langle\exists>(i, [2, 2], nfB(2 * i, 2 - i))], 0, 0 \rangle_5 \\ \sigma_{1,1,1,1}^{\exists} = \langle [\langle\forall>(i, [2, 1], nfA(2 * i, 1 - i))], 0, 0 \rangle_6 \end{array} \right. $$

$$ \rightsquigarrow_r^{\exists \forall} [\text{Activate}] \rightsquigarrow_r^{\exists \forall} [\exists - \text{Simplify}] \rightsquigarrow_r^{\exists \forall} [\exists - \text{Unfolding}] $$

$$ \rightsquigarrow_r^{\exists \forall} [\text{Activate}] \rightsquigarrow_r^{\exists \forall} [\forall - \text{Simplify}] \rightsquigarrow_r^{\exists \forall} [\forall - \text{Unfolding}] $$

$$ \rightsquigarrow_r^{\exists \forall} [\text{Activate}] \rightsquigarrow_r^{\exists \forall} [\exists - \text{Simplify}] $$

$$ \rightsquigarrow_r^{\exists \forall} [\exists - \text{Failure}] $$

$$ \exists \forall \exists \forall [ \text{Failure}, \sigma_{1,1,1,1}^{\exists}, \sigma_{1,1,1}^{\exists}, \sigma_{1,1}^{\exists} ] \tag{17} $$

$$ \begin{align} \rightsquigarrow_r^{\exists \forall} & [\forall - \text{FailurePropagate}] \nonumber \\ \exists \forall \exists & [ \text{Failure}, \nonumber \\ & \qquad \langle [\langle\exists>(i, [2, 2], nfB(2 * i, 2 - i)), 0, 0 \rangle_5, \sigma_{1,1}^{\exists}, \sigma_1^{\exists} \rangle ] \tag{18} \end{align} $$

$$ \begin{align} \rightsquigarrow_r^{\exists \forall} & [\exists - \text{FailurePropagate}] \nonumber \\ \exists \forall \exists & [ \langle [\langle\exists>(i, [2, 2], nfB(2 * i, 2 - i)), 0, 0 \rangle_5, \sigma_{1,1}^{\exists}, \sigma_1^{\exists} \rangle ] \tag{19} \end{align} $$

$$ \begin{align} \rightsquigarrow_r^{\exists \forall} & [\exists - \text{Unfolding}] \nonumber \\ \exists \forall \exists & [ \langle [nfB(4, 0)], 0, 0 \rangle_5, \nonumber \\ & \qquad \langle[\langle\exists>(i, [3, 2], nfB(2 * i, 2 - i)), 0, 0 \rangle_5, \sigma_{1,1}^{\exists}, \sigma_1^{\exists} \rangle ] \tag{20} \end{align} $$

$$ \text{avec} \quad \left\{ \begin{array}{l} \sigma_1^{\exists} = \langle [\langle\exists>(i, [3, 2], nfB(2 * i, 2 - i)), 0, 0 \rangle_5 \\ \sigma_1^{\exists, 1, 2} = \langle [\langle\forall>(i, [3, 2], nfA(2 * i, 3 - i)), 0, 0 \rangle_4 \\ \sigma_{1,2,1,1} = \langle [\langle\exists>(i, [2, 1], nfB(2 * i, 1 - i)), 0, 0 \rangle_5 \end{array} \right. $$

$$ \begin{align} \rightsquigarrow_r^{\exists \forall} & [\text{Activate}] \rightsquigarrow_r^{\exists \forall} [\forall - \text{Simplify}] \rightsquigarrow_r^{\exists \forall} [\forall - \text{Success}] \nonumber \\ \exists \forall \exists & [ \langle \cdot, 0, 0 \rangle_6, \sigma_{1,1,2}^{\exists}, \sigma_{1,1}^{\exists}, \sigma_1^{\exists} ] \tag{23} \end{align} $$

$$ \begin{align} \rightsquigarrow_r^{\exists \forall} & [\text{Success}] \nonumber \\ \exists \forall \exists & [ \text{Success}, \nonumber \\ & \qquad \langle [\langle\exists>(i, [3, 2], nfB(2 * i, 2 - i)), 0, 0 \rangle_5, \sigma_{1,1}^{\exists}, \sigma_1^{\exists} \rangle ] \tag{24} \end{align} $$

$$ \exists \forall [ \langle \cdot, 0, 0 \rangle_5, \sigma_{1,1}^{\exists}, \sigma_1^{\exists} ] \tag{25} $$

$$ \rightsquigarrow_r^{\exists \forall} [\text{Success}] \rightsquigarrow_r^{\exists \forall} [\forall - \text{SuccessPropagate}] $$

$$ \exists \forall [ \langle [\langle\forall>(i, [2, 2], nfA(2 * i, 3 - i)), 0, 0 \rangle_4, \sigma_1^{\exists} \rangle ] \tag{27} $$
<figure><img src="image_2.png" /></figure>

[ Success ] (41)

Le théorème suivant établit la correction et la compléture de la sémantique $\omega_r^{\exists\forall}$ par rapport à la sémantique $\omega_r^{\exists\forall} (\stackrel{*}{\sim}^{\exists\forall} r)$ représente la fermeture transitive de la relation $\stackrel{\sim}{\rightarrow}^{\exists\forall} r$).

La sémantique $\omega^{\exists\forall}$ de QCHR est définie par un calcul des séquents qui opère sur des séquents ($P \blacktriangleright \Omega \blacktriangle S \vdash S'$) où $P$ est un programme QCHR, $\Omega$ est un but, $S$ est le store avant la résolution du but et $S'$ est le but à l'issue de la résolution (voir [4] pour une description complète du système de calcul des séquents).

### Théorème 3.1 (Correction et compléture de $\omega_r^{\exists\forall}$)

Correction et compléture de la sémantique $\omega_r^{\exists\forall}$ par rapport à la sémantique $\omega^{\exists\forall}$.

Soit $P$ un programme QCHR. Il existe une preuve dans $\omega^{\exists\forall}$ pour le séquent ($P \blacktriangleright \Omega \blacktriangle S \vdash S'$) si et seulement si il existe une exécution dans $\omega_r^{\exists\forall}$ telle que $[\langle\Omega, S, \emptyset\rangle_1] \stackrel{*}{\sim}^{\exists\forall} [\langle\emptyset, S', H\rangle_c]$.

## 4 Discussion

Tous les solveurs QCSP de l'état de l'art ont le même inconvénient : ils explorent des espaces combinatoires beaucoup plus grands que l'espace de recherche naturel du problème original. Dans [3], la signification de la notion du "talon d'Achille", initialement introduite pour les formules booléennes quantifiées (QBF) [9, 24, 27, 28] dans [2] correspond à la difficulté de détecter que les contraintes booléennes sont nécessairement vraies sous une certaine affectation partielle. Cette notion a été étendue aux QCSP, mais sa portée a été étendue. Il s'agit désormais de déterminer comment éviter l'exploration d'espaces combinatoires dont on sait qu'ils sont inutiles par construction. Cette définition inclut la capture des actions illégales du joueur $B$ mais aussi la fin du jeu avant le dernier tour, évitant ainsi d'explorer un espace de recherche sur-dimensionné. Déjà cité, [5, 26] propose le nouveau langage QCSP+ qui utilise des séquences de quantification restreintes au lieu des séquences de quantification standard. [3] introduit un nouvel outil, inspiré de la règle de coupe de Prolog comme outil sous la responsabilité du concepteur du QCSP, pour élaguer les parties de l'espace de recherche qui sont par construction connues pour être inutiles. D'autres approches proposent de modifier plus ou moins le langage QCSP/QCSP+ pour surmonter les différents inconvénients : [6] propose le nouveau langage Strategic CSP où les variables universelles adaptent leur

domaine pour être compatibles avec les choix précédents ; [23] propose également un nouveau langage mais restreint aux CSP de jeux markoviens, basé explicitement sur la notion d'état, afin de modéliser et de résoudre efficacement les problèmes de contrôle de systèmes dynamiques complète-ment observables et markoviens. Ce langage est facilement et efficacement exprimé en QCHR. La sémantique opérationnelle $\omega_r^{\exists\forall}$ pour les QCHR présentée dans cet article a été implémentée dans QCHR++ , un solveur QCHR basé sur le solveur CHR++$^3$. Ce dernier ayant été étendu par l'ajout de deux nouveaux éléments à sa grammaire : exists et **forall**. Les résultats obtenus sur trois jeux connus (le jeu de la Matrice, le jeu de Nim (version Fibonacci) et le jeu du Puissance 4) sont présentés et commentés dans [4]. Il en ressort qu'un problème modélisé en QCHR est plus léger et plus compréhensible qu'un modèle QCSP. De plus, les performances du solveur QCHR++ sont équivalentes à celles du solveur QCSP voire supérieures de plusieurs ordres de grandeur lorsque le lieu peut être construit dynamiquement.

## 5 Conclusion

Cet article reprend le formalisme QCHR, une extension de CHR avec quantification, et propose une sémantique opérationnelle décrivant de manière fine l'exécution d'un programme QCHR. QCHR permet de modéliser des lieurs dynamiques qui se développent au fur et à mesure de l'exploration de l'arbre de recherche. Ceci permet de surmonter l'un des principaux inconvénients du cadre QCSP. Nous avons d'abord donné quelques modèles QCHR très intuïtifs démontrant l'intérêt d'une modélisation dynamique où le lieu se développe au fur et à mesure de l'exploration de l'arbre de recherche. Nous avons ensuite présenté une sémantique opérationnelle basée sur des états d'exécution ainsi que les règles de transition permettant sa mise en œuvre. Nous avons enfin montré la correction et la compléture de notre sémantique opérationnelle par rapport à la sémantique formelle présentée dans [4].

Nous pensons que ce nouveau formalisme permet de modéliser plus facilement les problèmes contraints avec quantification et offre une nouvelle approche lorsque le lieu ne peut être défini statiquement. Dans le futur, nous prévoyons de nous attaquer à des problèmes qui ne peuvent pas être traités avec QCSP tels que les problèmes où un lieu statique ne peut pas être trouvé.

## Références

[1] Abdennadher, S. et H. Schütz: *CHR : A Flexible Query Language*. Dans *Proceedings of the 3rd Internation*

<footnote n="3">3. CHR++ est un solveur CHR construit au dessus du langage C++, il peut être téléchargé à l'adresse https://gitlab.com/vynce/chrpp</footnote>
nal Conference on Flexible Query Answering Systems, pages 1–14, 1998.

[2] Ansotegui, C., C. Gomes et B. Selman: *Achilles' Heel of QBF*. Dans *Proceedings of the 20th National Conference on Artificial Intelligence (AAAI'05)*, pages 275–281, 2005.

[3] Barichard, V. et I. Stéphan: *The cut tool for QCSP*. Dans *Proceedings of the 26th IEEE International Conference on Tools with Artificial Intelligence (IC-TAI'14)*, pages 883–890, 2014.

[4] Barichard, V. et I. Stéphan: *Quantified Constraint Handling Rules*. Dans *Proceedings 35th International Conference on Logic Programming (ICLP'19)*, tome 306 de EPTCS, pages 210–223, 2019.

[5] Benedetti, M., A. Lallouet et J. Vautard: QCSP made Practical by virtue of Restricted Quantification. Dans *Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI'07)*, pages 38–43, 2007.

[6] Bessiere, C. et G. Verger: *Strategic constraint satisfaction problems*. Dans *Proceedings of the Workshop on Modelling and Reformulation*, 2006.

[7] Betz, H. et T.W. Frühwirth: *Linear-Logic Based Analysis of Constraint Handling Rules with Disjunction*. ACM Transactions on Computational Logic, 14(1):37, 2013.

[8] Bordeaux, L. et E. Monfroy: *Beyond NP : Arc-Consistency for Quantified Constraints*. Dans *Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP'02)*, pages 371–386, 2002.

[9] Cadoli, M., A. Giovanardi et M. Schaerf: *An Algorithm to Evaluate Quantified Boolean Formulae*. Dans *Proceedings of the 15th National Conference on Artificial Intelligence (AAAI'98)*, pages 262–267, 1998.

[10] Duck, G.J., P.J. Stuckey, M.G. de la Banda et C. Holzbaur: *The Refined Operational Semantics of Constraint Handling Rules*. Dans *Proceedings of the 20th International Conference on Logic Programming (ICLP'04)*, pages 90–104, 2004.

[11] Frühwirth, T.W.: *Constraint Handling Rules*. rapport technique, ECRC, 1992.

[12] Frühwirth, T.W.: *Constraint Handling Rules*. Dans *Constraint Programming : Basics and Trends*, pages 90–107, 1994.

[13] Frühwirth, T.W.: *Constraint Handling Rules*. Cambridge University Press, 2009.

[14] Frühwirth, T.W. et S. Abdennadher: *Essentials of Constraint Programming*. Springer-Verlag, 2003.

[15] Frühwirth, T.W. et F. Raiser (rédacteurs): *Constraint Handling Rules : Compilation, Execution, and Analysis*. March 2011.

[16] Frühwirth, T.W.: *Theory and Practice of Constraint Handling Rules*. Journal of Logic Programming, 37(1-3):95–138, 1998.

[17] Gent, I.P., P. Nightingale, A. Rowley et K. Stergiou: *Solving quantified constraint satisfaction problems*. Artificial Intelligence, 172(6-7):738–771, 2008.

[18] Hentenryck, P. Van: *Constraint logic programming*. Knowledge Engineering Review, 6(3):151–194, 1991.

[19] Jaffar, J. et J. L. Lassez: *Constraint Logic Programming*. Dans *Proceedings of the 14th Annual ACM Symposium on Principles of Programming Languages*, pages 111–119, 1987.

[20] Jaffar, J. et M.J. Maher: *Constraint Logic Programming : A Survey*. Journal of Logic Programming, 19/20:503–581, 1994.

[21] Mamoulis, N. et K. Stergiou: *Algorithms for Quantified Constraint Satisfaction Problems*. Dans *Proceedings of the 10th International Conference on Principles and Practice of Constraint Programming (CP'04)*, pages 752–756, 2004.

[22] Nightingale, P.: *Consistency and the Quantified Constraint Satisfaction Problem*, PhD thesis, University of St Andrews, 2007.

[23] Pralet, C. et G. Verfaillie: *Beyond QCSP for Solving Control Problems*. Dans *Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP'11)*, pages 744–758, 2011.

[24] Rabe, M. et L. Tentrup: *CAQE : A Certifying QBF Solver*. Dans *Formal Methods in Computer-Aided Design (FMCAD'15)*, pages 136–143, 2015.

[25] Verger, G. et C. Bessiere: *BlockSolve : a Bottom-Up Approach for Solving Quantified CSPs*. Dans *Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming (CP'06)*, pages 635–649, 2006.

[26] Verger, G. et C. Bessiere: *Guiding Search in QCSP<sup>+</sup> with Back-Propagation*. Dans *Proceedings of the 14th International Conference on Principles and Practice of Constraint Programming (CP'08)*, pages 175–189, 2008.

[27] Zhang, L.: *Solving QBF with Combined Conjunctive and Disjunctive Normal Form*. Dans *Proceedings of the 21st National Conference on Artificial Intelligence (AAAI'06)*, 2006.

[28] Zhang, L. et S. Malik: *Conflict Driven Learning in a Quantified Boolean Satisfiability Solver*. Dans *Proceedings of the International Conference on Computer Aided Design (ICCAD'02)*, pages 442–449, 2002.