«Résolution incrémentale d'équations linéaires
dans Z»
Patricia Mainguet (LIMOS, Clermont-Ferrand)
Résumé - Nous étudions le problème de la satisfiabilité d'un système d'équations linéaires à variables dans Z. L'approche classique consiste à travailler sur des domaines finis où les variables prennent leur valeur dans des intervalles bornés des entiers. Nous avons choisi de considérer directement Z et de calculer la satisfiabilité en mettant le système sous forme soluble. Plusieurs algorithmes de calcul de forme soluble existent sur les domaines R ou Q mais ne sont pas adaptés à Z car les coefficients des systèmes ainsi calculés ne sont pas entiers. L'idée essentielle est de générer un coefficient unitaire. Nous présentons deux algorithmes incrémentaux qui calculent la forme soluble de Gauss-Jordan. Ils se distinguent l'un de l'autre par la mèthode de génération des coefficients unitaires mais ont en commun les propriétés de terminaison, complétude et correction.
«Optimisation des Q-matrices pour la résolution de contraintes
linéaires»
David-Olivier Azulay et Jean-François Pique (Université Aix-Marseille)
Résumé - Nous utilisons le formalisme des Q-matrices pour une résolution efficace basée sur des calculs entiers de systèmes linéaires. Nous décrivons un algorithme optimisé pour l'opération de Q-pivot des Q-matrices, ce qui permet d'améliorer sensiblement les performances des solveurs de contraintes linéaires en précision parfaite. Nous détaillons enfin un codage des Q-matrices approprié à l'algorithme décrit, et montrons les améliorations obtenues.
«Acceleration methods for numeric CSPS»
Yahia Lebbah et Olivier Lhomme (École des Mines de Nantes)
Abstract - This paper introduces a new approach to accelerate the convergence of numeric csp filtering algorithms, by using extrapolation methods. Extrapolation methods are used in numerical analysis to accelerate the convergence of real numbers sequences. We show how to use them for solving numeric csps, leading to drastic improvement in efficiency.