Contraintes Diophantiennes Linéaires : résolution et coopération inter-résolveurs - Université de Lorraine Accéder directement au contenu
Thèse Année : 1998

Linear diophantine constraints : solving and cooperation of solvers

Contraintes Diophantiennes Linéaires : résolution et coopération inter-résolveurs

Farid Ajili
  • Fonction : Auteur
  • PersonId : 756483
  • IdRef : 153560762

Résumé

The emergency of deduction with constraints as a new programming paradigm, which incorporates declarativity and efficiency, has intensified the need for the design of new efficient constraint solvers and the integration of various computation domains. Until now, most of the available constraint solvers are incomplete because they compute some solutions, but not all the solution set. We are first interested in complete solving of linear diophantine constraints. Afterwards, we investigate the combination of unification and built-in constraints. Complete solvers of linear diophantine equations do exist. However, there was no solver which directly provides the solution set basis of an equational and inequational system without turning inequations to equations by introducing slack variables. We present the first solver of a system of equations and inequations, which computes the solution set basis and avoids the adding of slack variables. Like most of the available complete solving methods, our solver does not dynamically exploit constraints in order to efficiently prune the se arch space. We cooperate our solver with propagation techniques. This cooperation aims at integrating local information based reasoning which is able to anticipate some failures and to exploit pruning opportunities. Our result is a new solver over finite domains. Finally, we propose a framework for the combination of built-in and equational unification constraints in presence of functions from terms to built-ins. The study of an instance of the framework where only homomorphisms are allowed shows how to filter information through cooperating solvers in order to reach the so-called quasi-solved forms.
L'émergence de la déduction avec contraintes comme un nouveau paradigme de programmation ralliant la déclarativité et l'efficacité a accentué le besoin de concevoir de nouveaux résolveurs efficaces et d'intégrer divers domaines de calcul. Actuellement, la plupart des résolveurs de contraintes sont incomplets, car ils ne calculent que certaines solutions, mais pas tout l'ensemble des solutions. Nous nous intéressons tout d'abord à. la résolution complète de contraintes diophantiennes linéaires et la coopération de leurs résolveurs. Nous étudions ensuite la combinaison de contraintes d'unification et prédéfinies. Il existe beaucoup de résolveurs complets d'équations diophantiennes linéaires. Il n'existait pas de résolveurs complets qui calculent directement une base génératrice de l'ensemble des solutions d'un système d'équations et d'inéquations sans coder les inéquations par des équations en introduisant des variables d'écart. Nous présentons le premier résolveur de systèmes d'équations et d'inéquations calculant la base génératrice de l'ensemble des solutions, qui évite l'ajout de variables auxiliaires. Comme la plupart des méthodes de résolution complètes, notre résolveur n'exploite pas dynamiquement les contraintes en vue d'élaguer intelligemment l'espace de recherche. Nous coopérons notre résolveur avec les techniques de propagation. Cette coopération vise l'intégration d'un raisonnement à base d'informations locales qui est capable d'anticiper certains échecs et d'exploiter des opportunités d'élagage. Il en résulte, en outre, un nouveau résolveur sur les domaines finis. Enfin, nous proposons un formalisme de combinaison de contraintes prédéfinies et d'unification équationnelle en présence de fonctions des termes vers le domaine prédéfini. Nous étudions l'instance du formalisme où on permet seulement des homomorphismes et nous montrons qu'il est possible de faire collaborer les deux résolveurs dans le but d'atteindre des formes dites quasi-résolues.
Fichier non déposé

Dates et versions

tel-01747057 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01747057 , version 1

Accès intranet

Citer

Farid Ajili. Contraintes Diophantiennes Linéaires : résolution et coopération inter-résolveurs. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1998. Français. ⟨NNT : 1998NAN10025⟩. ⟨tel-01747057⟩
25 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More