Some works in progress on finite domain constraint solvers concern the implemen- tation 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) are used during domain reduction by some solvers. In this paper, we use a formalization of explanations by proof trees in a fixpoint framework based on iteration of monotonic local con- sistency 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.
RÉSUMÉ. Nous présentons un algorithme heuristique pour déterminer une solution d’un problème de satisfaction de contraintes continu. Cet algorithme, appelé Recherche Locale Dichotomique ( ), combine la recherche locale, la bissection et la contraction d’intervalles avec la propagation de contraintes. Nous présentons des résultats expérimentaux et les comparons avec un algorithme de recherche locale pure basé sur la stratégie d’évolution.
Le probleme de l'isomorphisme de graphes consiste a prouver que deux graphes donnes ont la meme structure. Ce probleme peut tres facilement etre modelise en un probleme de satisfaction de puis etre resolu par un solveur de contraintes. Toutefois, sur ce type de problemes, la programmation par est bien moins efficace que les algorithmes dedies qui sont capables de tirer partie de la semantique globale du probleme. Nous introduisons dans cet article une nouvelle contrainte globale dediee au probleme de l'isomorphisme de graphes. Nous definissons ensuite l'algorithme de filtrage associe a cette contrainte. Celui-ci exploite les aretes du graphe de facon globale afin de reduire le domaine des variables. Nous montrons aussi que cette contrainte globale est decomposable en un ensemble de contraintes de distance propageant mieux les reductions des domaines que les contraintes d'aretes habituellement utilisees pour ce probleme.
RESUME. L’analyse de terminaison des programmes logiques a ete sujette a une recherche intensive durant les deux dernieres decennies. La majorite des travaux s’est interessee a la terminaison universelle gauche d’une classe donnee de requetes, c’est-a-dire au fait que toutes les derivations des requetes de cette classe produites par un moteur Prolog sont finies. En revanche, l’etude du probleme dual : la non-terminaison par rapport a la regle de selection gauche, i.e l’existence d’une requete dans une classe donnee qui admet une derivation gauche infinie, a fait l’objet de peu d’articles. Dans ce papier, nous etudions la non-terminaison dans le contexte de la programmation logique avec contraintes. Nous reformulons, dans ce cadre plus abstrait, les concepts que nous avions definis pour la programmation logique, ce qui nous donne des criteres necessaires et suffisants exprimes de facon logique ainsi que des preuves plus simples. Par ailleurs, en reconsiderant nos travaux precedents, nous demontrons que dans un certain sens, nous detenions deja le meilleur critere syntaxique dans le cas de la programmation logique. Enfin, nous decrivons un ensemble d’algorithmes corrects pour l’inference de non-terminaison des programmes CLP.
The development of formal models is often a key step when developing safety or mission critical software. In this setting it is vital to formally check and validate these formal models before translating them into code. I will present ProB, a toolset for the B method which was developed using constraint logic programming technology. ProB allows fully automatic animation of B models, and can be used to systematically check a B model for errors. ProB supports B features such as non-deterministic operations, ANY statements, operations with complex arguments, sets, sequences, functions, lambda abstractions, set comprehensions, constants and properties, and many more. ProB's animation facilities allow users to gain confidence in their specifications, and unlike other animators, the user does not have to guess the right values for the operation arguments or choice variables. This is achieved by using co-routining and finite domain constraint solving. On top of the animation features, ProB contains a temporal model checker and a constraint-based model checker, both of which can be used to detect various errors in B specifications.
The analysis of biochemical networks is mainly done using relational or procedural languages. Combining or designing new analyses requires lot of programming effort that cannot be reused for other analyses. To overcome these limitations, we introduce CP(BioNet) a new constraint programming domain for the analysis of biochemical networks. Analyses are formulated using constraints over graph domain variables. The constraints are then solved by a constraint solver designed for biochemical networks. This provides a flexible and powerful approach as simple analyses can then easily be combined to form complex ones. We focus here on Constrained path finding, finding a path from node A to node B in a graph with additional constraints, such as requiring this path to include a predefined set of mandatory intermediate nodes. Constraints for path finding are introduced and their implementation (propagators) is described. A prototype is presented and constrained path finding experiments are performed and analyzed to illustrate the benefits of this new approach.
We propose a direct interpretation for constraint-based linguistic formalisms in which the notions of derivation and hierarchy give way to the more flexible notion of property sat- isfaction between categories. Such frameworks define sentence acceptability in terms of the properties that must be satisfied by groups of categories (e.g. English noun phrases can be de- scribed in Property Grammar terms (Blache01a) through a few properties such as precedence (a determiner must precede a noun); uniqueness (there must be only one determiner); exclusion (an adjective phrase must not coexist with a superlative); and so on. Rather than resulting in either a parse tree or failure, such frameworks characterize a sentence through the list of the properties it satisfies and the list of properties it violates. This allows us to parse incomplete and incorrect input in a very modular and adaptable, while efficient, manner.
RÉSUMÉ. Nous proposons une caractérisation en termes de modèles des approximations calcu- lées par une consistance pendant la résolution d'un CSP sur les domaines finis. Nous propo- sons d'abord un premier programme CLP défini dont le plus grand point-fixe représente un état consistant. Ce cadre est suffisamment général pour être appliqué à l'arc-consistance, à la consistance de bornes ou à n'importe quel autre schéma d'approximation. De plus, motivé par d'autres approches visant à représenter les solutions d'un CSP par les modèles stables de programmes logiques, nous proposons un programme normal dont les modèles stables sont les états consistants du CSP. ABSTRACT. We provide here a model-theoretic characterization of the approximations computed by a consistency while solving a finite domain CSP. At first, we propose a definite CLP program which allows to characterize the computed approximation by its fixpoints. This framework is general enough to be applied to (hyper)arc-consistency, bound-consistency or any approx- imation scheme. Moreover, motivated by other approaches of CSP representations by logic programs with stable model semantics, the computed approximation is also represented in a natural way by the stable models of another (normal) CLP program.
Nous presentons dans cet article les bases d’un nouveau modele de calcul permettant de combiner des methodes completes et incompletes pour la resolution de problemes de satisfaction de contraintes. Ce schema algorithmique utilise des techniques de propagation de contraintes dans un contexte evolutionniste integrant egalement des heuristiques de recherche locale. L’uniformite des structures utilisees autorise une interaction plus homogene entre les differentes methodes mises en oeuvre et permet egalement de beneficier au mieux de leurs atouts respectifs. La grande flexibilite de ce modele offre egalement la possibilite d’en envisager diverses extensions. Nous mettons en avant l’interet de notre approche sur quelques exemples par le biais d’une implementation.
RÉSUMÉ. Nous présentons PICPA, un nouvel algorithme pour traiter les problèmes multiobjectif continus sous contraintes. Cet algorithme combine des techniques de propagation de contraintes à des concepts évolutionnaires. À la différence des algorithmes évolutionnaires classiques qui ne donnent que des solutions heuristiques, PICPA est capable de calculer des bornes du front Pareto optimal tout en produisant des solutions approchées très précises.
