Publications

Blache (2000) introduced Property Grammar as a formalism where linguistic information is represented in terms of non hierarchical constraints. This feature gives it an adequate expressive power to handle complex linguistic phenomena, such as long distance dependencies, and also agrammatical sentences (Blache, 2004). Recently, Duchier et al. (2009) proposed a model-theoretic semantics for property grammar. The present paper follows up on that work and explains how to turn such a formalization into a constraint optimization problem, solvable using constraint programming techniques. This naturally leads to an implementation of a fully constraint-based parser for property grammars.

Les Grammaires de Propriétés (GP) constituent un formalisme à base de contraintes capable de décrire à la fois des énoncés bien-formés et des énoncés agrammaticaux, ce qui en fait un formalisme particulièrement intéressant pour traiter de la gradience de grammaticalité, comme l'a démontré Prost (2008). Duchier et al (2009) ont défini une sémantique des grammaires de propriétés en théorie des modèles. Cet article poursuit ce travail en montrant comment, à partir de cette sémantique, définir l'analyse syntaxique en GP sous la forme d'un Problème de Satisfaction de Contraintes (CSP), traitable au moyen de la programmation par contraintes.

This paper proposes a model for explanations in a set theoretical framework using the notions of closure or fixpoint. In this approach, sets of rules associated with monotonic operators allow to define proof trees. The proof trees may be considered as a declarative view of the trace of a computation. We claim they are explanations of the results of a computation. This notion of explanation is applied to constraint logic programming, and it is used for declarative error diagnosis. It is also applied to constraint programming, and it is used for constraint retraction.

This paper proposes a model for explanations in a set theoretical framework using the notions of closure or fixpoint. In this approach, sets of rules associated with monotonic operators allow to define proof trees. The proof trees may be considered as a declarative view of the trace of a computation. We claim they are explanations of the result of a computation. First, the general scheme is given. Then, it is applied to Constraint Logic Programming, next to Constraint Satisfaction Problems.

Some works in progress on finite domain constraint solvers concern the implementation of a XML trace of the computation according to the OADymPPaC DTD (for example in GNU-Prolog, PaLM, CHIP). Because of the large size of traces, even for small toy problems, some tools are needed to understand this trace. Explanations of value withdrawal (or nogoods) during domain reduction are used by some solvers in finite domain constraint programming. In this paper, we use a formalization of explanations by proof trees in a fixpoint framework based on iteration of monotonic local consistency operators. Proof trees provide a declarative view of the computations by constraint propagation. We show how explanations may be naturally extracted from the OADymPPaC trace format. Explanations allow a better understanding of the domain reductions in the trace.

Certains travaux en cours sur les solveurs de contraintes dans les domaines finis concernent l'implantation d'une trace XML du calcul, selon la DTD OADymPPaC (par exemple en GNU-Prolog, PaLM, CHIP). A cause de la grande taille des traces, même pour de petits exemples jouets, on a besoin d'outils pour comprendre cette trace. Des explications de retrait de valeurs (ou nogoods) pendant la réduction de domaine sont utilisées par certains solveurs en programmation par contraintes dans l es domaines finis. Dans ce papier, nous utilisons une formalisation des explications par des arbres de preuve dans un cadre point fixe basé sur l'itération d'opérateurs monotones de consistance locale. Les arbres de preuve donnent une vue déclarative des calculs par propagation de contrainte. Nous montrons comment des explications peuvent être extraites de façon naturelle du format de trace OADymPPaC. Les explications permettent une meilleure compréhension des réductions de domaine dans la trace.

Depuis quelques années, la programmation par contraintes a montré son efficacité pour traiter les problèmes difficiles, tant au point de vue de leur modélisation que de leur résolution. Quand les domaines sont finis, les problèmes ainsi modélisés sont appelés problèmes de satisfaction de contraintes. Les solveurs utilisés pour obtenir leurs solutions mêlent des techniques de retraits de valeurs par des notions de consistance (la réduction de domaine) à des techniques de recherche systématique (l'énumération). Récemment différentes notions d'explications ont été introduites, que ce soit pour améliorer l'efficacité des méthodes de l'énumération ou pour traiter les problèmes sur-contraints ou dynamiques. L'idée est d'enregistrer de l'information expliquant les retraits de valeurs afin de pouvoir l'utiliser, pour éviter d'explorer tout l'arbre de recherche lors de l'énumération, pour choisir une contrainte à relaxer quand un problème est sur-contraint ou encore pour réintroduire des valeurs dans les domaines quand une contrainte est relaxée. Cette thèse propose trois contributions au domaine de la programmation par contraintes. Tout d'abord la réduction de domaine est formalisée en terme ensembliste et vue comme un calcul de point fixe. Ce cadre général, dans lequel l'énumération s'intègre aisément, s'applique à tout type de solveur effectuant de la réduction de domaine. De plus, il permet une définition naturelle d'une notion générale d'explication: les arbres explicatifs. Ces arbres de preuve sont inductivement définis par des règles exprimant le retrait d'une valeur comme conséquence d'autres retraits. Les notions existantes d'explications peuvent aisément en être extraites. Enfin, la structure arborescente des arbres explicatif est utilisée pour adapter le diagnostic déclaratif de réponse manquante à la programmation par contrainte. En effet, les arbres explicatifs peuvent être considérés comme une trace déclarative du calcul du solveur et peuvent donc aider à la compréhension de l'absence d'une réponse.

The paper proposes a theoretical approach of the debugging of constraint programs based on a notion of explanation tree. The proposed approach is an attempt to adapt algorithmic debugging to constraint programming. In this theoretical framework for domain reduction, explanations are proof trees explaining value removals. These proof trees are defined by inductive definitions which express the removals of values as consequences of other value removals. Explanations may be considered as the essence of constraint programming. They are a declarative view of the computation trace. The diagnosis consists in locating an error in an explanation rooted by a symptom.

In this paper, we present a general scheme for incremental constraint retraction algorithms that encompasses all existing algorithms. Moreover, we introduce some necessary conditions to ensure the correctness of any incremental constraint retraction algorithms. This rather theoretical work is based on the notion of explanation for constraint programming and is exemplified within the PALM system: a constraint solver allowing dynamic constraint retractions.

The report proposes a theoretical approach of the debugging of constraint programs based on the notion of explanation tree (D1.1.1 and D1.1.2 part 2). The proposed approach is an attempt to adapt algorithmic debugging to constraint programming. In this theoretical framework for domain reduction, explanations are proof trees explaining value removals. These proof trees are defined by inductive definitions which express the removals of values as consequence of other value removals. Explanations may be considered as the essence of constraint programming. They are a declarative view of the computation trace. The diagnosis consists in locating an error in an explanation rooted by a symptom.

Solvers on finite domains use local consistency notions to remove values from the domains. This paper defines value withdrawal explanations. Domain reduction is formalized with chaotic iterations of monotonic operators. To each operator is associated its dual which will be described by a set of rules. For classical consistency notions, there exists a natural such system of rules. They express value removals as consequences of other value removals. The linking of these rules inductively defines proof trees. Such a proof tree clearly explains the removal of a value (the root of the tree). Explanations can be considered as the essence of domain reduction.

Constraint logic programming combines declarativity and efficiency thanks to constraint solvers implemented for specific domains. Value withdrawal explanations have been efficiently used in several constraints programming environments but there does not exist any formalization of them. This paper is an attempt to fill this lack. Furthermore, we hope that this theoretical tool could help to validate some programming environments. A value withdrawal explanation is a tree describing the withdrawal of a value during a domain reduction by local consistency notions and labeling. Domain reduction is formalized by a search tree using two kinds of operators: for local consistency notions and for labeling. These operators are defined by sets of rules. Proof trees are built with respect to these rules. For each removed value, there exists such a proof tree which is the withdrawal explanation of this value.

Solvers on finite domains use local consistency notions to remove values from the domains. This paper defines value withdrawal explanations. Domain reduction is formalized with chaotic iterations of monotonic operators. To each operator is associated its dual which will be described by a set of rules. For classical consistency notions, there exists a natural such system of rules. They express value removals as consequences of other value removals. The linking of these rules inductively defines proof trees. Such a proof tree clearly explains the removal of a value (the root of the tree). Explanations can be considered as the essence of domain reduction.

Using a filtering technique is crucial to reduce the search space. Most of the solvers (CHIP, GNU-Prolog, ILOG Solver, CHOCO) use reduction operators and a propagation mechanism to enforce a local consistency. This scheme is quite universally used on static CSPs. But we do not have such an unanimity when relaxing constraints. Several techniques have been proposed to deal with dynamicity. The problem we address here is two-fold. First, we highlight that it is possible to generalize the proposed techniques to relax constraints. Second, we show a sufficient work to do in order to incrementally relax a constraint.

Ce rapport a pour but de fournir un modèle théorique pour la propagation et le labeling. Ce modèle est adapté aux solveurs sur domaines finis utilisés par chacun des partenaires du projet: GNU-Prolog (INRIA), CHIP (Cosytec) et Choco (EMN). Un calcul est formalisé par un arbre dans lequel chaque branche correspondà une itération chaotique d'opérateurs et où chaque feuille peut-être décrite en terme de clôture. Ce modèle est bien adapté aux notions d'explications qui seront utiles pour la mise au point de programmes avec contraintes. Ce rapport fait suite à la réalisation d1.1.1 qui traitait de la réduction de domaine. Il sera étendu pour inclure un langage hôte dans la prochaine réalisation.

Using a filtering technique is crucial to reduce the search space. Most of the solvers (CHIP, GNU-Prolog, ILOG Solver, CHOCO) use reduction operators and a propagation mechanism to enforce a local consistency. This scheme is quite universally used on static CSPs. But we do not have such an unanimity when relaxing constraints. Several techniques have been proposed to deal with dynamicity. The problem we address here is two-fold. First, we highlight that it is possible to generalize the proposed techniques to relax constraints. Second, we show a sufficient work to do in order to incrementally relax a constraint.

Constraint programming is an important programming paradigm of the last years. It combines declarativity and efficiency thanks to constraint solvers which are implemented for specific domains. We are interested here in the case of reduction of finite domains. In the paper, it is formalized with chaotic iterations of monotonic operators. A first notion of explanation, which have been proved very useful in many applications, is then defined in a declarative way in terms of closure. An explanation set for a value removal is a set of operators which always remove this value whatever the order of application of these operators is. A monotonic operator can always be defined by a set of rules (in the sense of inductive definition of Aczel). Furthermore, the paper shows that for classical notions of local consistency, such a system of rules can be expressed in a natural way. They express value removals as consequences of other value removals. So, a more precise notion of explanation can be obtained: the linking of these rules allows to inductively define proof trees. Such a proof tree clearly explains the removal of a value (the root of the tree) by the solver, it is then called an explanation for this value withdrawal. Explanations are the essence of domain reduction.

The aim of this report is to provide the theoretical foundations of domain reduction. The model is well suited to the solvers on finite domains which are used on the respective platforms of each partner of the project: GNU-Prolog (INRIA), CHIP (COSYTEC) and PaLM (EMN). A computation is formalized by a chaotic iteration of operators and the result is described as a closure. The model is well suited to the definition of traces and explanations which will be useful for the debugging of constraint programs. This report only deals with the reduction stage. It will be extended to the labeling and the host language in next reports.

This work is devoted to constraint solving motivated by the debugging of constraint logic programs a la GNU-Prolog. The paper focuses only on the constraints. In this framework, constraint solving amounts to domain reduction. A computation is formalized by a chaotic iteration. The computed result is described as a closure. This model is well suited to the design of debugging notions and tools, for example failure explanations or error diagnosis. In this paper we detail an application of the model to an explanation of a value withdrawal in a domain. Some other works have already shown the interest of such a notion of explanation not only for failure analysis.

This work is devoted to constraint solving motivated by the debugging of constraint logic programs a la GNU-Prolog. The paper focuses only on the constraints. In this framework, constraint solving amounts to domain reduction. A computation is formalized by a chaotic iteration. The computed result is described as a closure. This model is well suited to the design of debugging notions and tools, for example failure explanations or error diagnosis. In this paper we detail an application of the model to an explanation of a value withdrawal in a domain. Some other works have already shown the interest of such a notion of explanation not only for failure analysis.