Cette thèse présente une méthode parallèle de résolution de systèmes linéaires creux basée sur un algorithme multigrille géométrique. Les estimations de la solution sont calculées par méthode directe sur le niveau grossier ou par méthode itérative de type splitting sur les maillages raffinés; des opérateurs inter-grilles sont définis pour interpoler les solutions approximatives entre les différents niveaux de raffinements. Ce solveur est utilisé dans le cadre de simulations électromagnétiques en 3D (équations de Maxwell en régime harmonique discrétisées par éléments finis de Nédélec de premier ordre) en tant que méthode stationnaire ou comme préconditionneur d’une méthode de Krylov (GMRES). / Multigrid algorithm. The system is solved thanks to a direct method on the coarse mesh anditerative splitting method on refined meshes; inter-grid operators are defined to interpolate theapproximate solutions on the different refinement levels. Applied to 3D electromagnetic simulations(Nédélec first order finite element approximation of time harmonic Maxwell equations) thissolver is used either as a stationary method or as a preconditioner for a Krylov subspace method(GMRES).

Quoique très difficile à résoudre, le problème de satisfiabilité Booléenne (SAT) est fréquemment utilisé lors de la modélisation d’applications industrielles. À cet effet, les deux dernières décennies ont vu une progression fulgurante des outils conçus pour trouver des solutions à ce problème NP-complet. Deux grandes avenues générales ont été explorées afin de produire ces outils, notamment l’approche logicielle et matérielle. Afin de raffiner et améliorer ces solveurs, de nombreuses techniques et heuristiques ont été proposées par la communauté de recherche. Le but final de ces outils a été de résoudre des problèmes de taille industrielle, ce qui a été plus ou moins accompli par les solveurs de nature logicielle. Initialement, le but de l’utilisation du matériel reconfigurable a été de produire des solveurs pouvant trouver des solutions plus rapidement que leurs homologues logiciels. Cependant, le niveau de sophistication de ces derniers a augmenté de telle manière qu’ils restent le meilleur choix pour résoudre SAT. Toutefois, les solveurs modernes logiciels n’arrivent toujours pas a trouver des solutions de manière efficace à certaines instances SAT. Le but principal de ce mémoire est d’explorer la résolution du problème SAT dans le contexte du matériel reconfigurable en vue de caractériser les ingrédients nécessaires d’un solveur SAT efficace qui puise sa puissance de calcul dans le parallélisme conféré par une plateforme FPGA. Le prototype parallèle implémenté dans ce travail est capable de se mesurer, en termes de vitesse d’exécution à d’autres solveurs (matériels et logiciels), et ce sans utiliser aucune heuristique. Nous montrons donc que notre approche matérielle présente une option prometteuse vers la résolution d’instances industrielles larges qui sont difficilement abordées par une approche logicielle. / Though very difficult to solve, the Boolean satisfiability problem (SAT) is extensively used to model various real-world applications and problems. Over the past two decades, researchers have tried to provide tools that are used, to a certain degree, to find solutions to the Boolean satisfiability problem. The nature of these tools is broadly divided in software and reconfigurable hardware solvers. In addition, the main algorithms used to solve this problem have also been complemented with heuristics of various levels of sophistication to help overcome some of the NP-hardness of the problem. The end goal of these tools has been to provide solutions to industrial-sized problems of enormous size. Initially, reconfigurable hardware tools provided a promising avenue to accelerating SAT solving over traditional software based solutions. However, the level of sophistication of software solvers overcame their hardware counterparts, which remained limited to smaller problem instances. Even so, modern state-of-the-art software solvers still fail unpredictably on some instances. The main focus of this thesis is to explore solving SAT on reconfigurable hardware in order to gain an understanding of what would be essential ingredients to add (and discard) to a very efficient hardware SAT solver that obtains its processing power from the raw parallelism of an FPGA platform. The parallel prototype solver that was implemented in this work has been found to be comparable with other hardware and software solvers in terms of execution speed even though no heuristics or other helping techniques were implemented. We thus show that our approach provides a very promising avenue to solving large, industrial SAT instances that might be difficult to handle by software solvers.

Le présent travail est consacré à l’approximation numérique des solutions du modèle aux moments M1 pour le transfert radiatif. Il s’agit, ici, de développer des solveurs numériques performants et précis capables de prédire avec précision et robustesse des écoulements où le transfert radiatif joue un rôle essentiel. Dans ce sens, plusieurs méthodes numériques ont été envisagées pour la dérivation des schémas numériques de type solveur de Godunov. Une attention particulière a été portée sur les solveurs préservant les ondes de contact stationnaires. En particulier, un schéma de relaxation et un solveur HLLC sont présentés dans ce travail. Pour chacun de ces solveurs, la robustesse de la méthode a été établie (positivité de l’énergie radiative et limitation du flux radiatif). La validation et l’intérêt des méthodes abordées sont exhibés à travers de nombreuses expériences numériques mono et multidimensionelles. / The present work is dedicated to the numerical approximation of the M1 moments model solutions for radiative transfer. The objective is to develop efficient and accurate numerical solvers, able to provide with precise and robust computations of flows where radiative transfer effects are important. With this aim, several numerical methods have been considered in order to derive numerical schemes based on Godunov type solvers. A particular attention has been paid to solvers preserving the stationary contact waves. Namely, a relaxation scheme and a HLLC solver are presented in this thesis. The robustness of each of these solvers has been established (radiative energy positivity and radiative flux limitation). Several numerical experiments in one and two space dimensions validate the developed methods and outline their interest.

Quoique très difficile à résoudre, le problème de satisfiabilité Booléenne (SAT) est fréquemment utilisé lors de la modélisation d’applications industrielles. À cet effet, les deux dernières décennies ont vu une progression fulgurante des outils conçus pour trouver des solutions à ce problème NP-complet. Deux grandes avenues générales ont été explorées afin de produire ces outils, notamment l’approche logicielle et matérielle. Afin de raffiner et améliorer ces solveurs, de nombreuses techniques et heuristiques ont été proposées par la communauté de recherche. Le but final de ces outils a été de résoudre des problèmes de taille industrielle, ce qui a été plus ou moins accompli par les solveurs de nature logicielle. Initialement, le but de l’utilisation du matériel reconfigurable a été de produire des solveurs pouvant trouver des solutions plus rapidement que leurs homologues logiciels. Cependant, le niveau de sophistication de ces derniers a augmenté de telle manière qu’ils restent le meilleur choix pour résoudre SAT. Toutefois, les solveurs modernes logiciels n’arrivent toujours pas a trouver des solutions de manière efficace à certaines instances SAT. Le but principal de ce mémoire est d’explorer la résolution du problème SAT dans le contexte du matériel reconfigurable en vue de caractériser les ingrédients nécessaires d’un solveur SAT efficace qui puise sa puissance de calcul dans le parallélisme conféré par une plateforme FPGA. Le prototype parallèle implémenté dans ce travail est capable de se mesurer, en termes de vitesse d’exécution à d’autres solveurs (matériels et logiciels), et ce sans utiliser aucune heuristique. Nous montrons donc que notre approche matérielle présente une option prometteuse vers la résolution d’instances industrielles larges qui sont difficilement abordées par une approche logicielle. / Though very difficult to solve, the Boolean satisfiability problem (SAT) is extensively used to model various real-world applications and problems. Over the past two decades, researchers have tried to provide tools that are used, to a certain degree, to find solutions to the Boolean satisfiability problem. The nature of these tools is broadly divided in software and reconfigurable hardware solvers. In addition, the main algorithms used to solve this problem have also been complemented with heuristics of various levels of sophistication to help overcome some of the NP-hardness of the problem. The end goal of these tools has been to provide solutions to industrial-sized problems of enormous size. Initially, reconfigurable hardware tools provided a promising avenue to accelerating SAT solving over traditional software based solutions. However, the level of sophistication of software solvers overcame their hardware counterparts, which remained limited to smaller problem instances. Even so, modern state-of-the-art software solvers still fail unpredictably on some instances. The main focus of this thesis is to explore solving SAT on reconfigurable hardware in order to gain an understanding of what would be essential ingredients to add (and discard) to a very efficient hardware SAT solver that obtains its processing power from the raw parallelism of an FPGA platform. The parallel prototype solver that was implemented in this work has been found to be comparable with other hardware and software solvers in terms of execution speed even though no heuristics or other helping techniques were implemented. We thus show that our approach provides a very promising avenue to solving large, industrial SAT instances that might be difficult to handle by software solvers.

Les méthodes formelles pour la conception des software et hardware génèrent souvent des formules qui doivent être validées, de manière interactive ou automatique. Parmi les outils automatiques, les solveurs SMT (Satisfiabilité Modulo Théories) sont particulièrement adaptés à la résolution de ces obligations de preuve, puisque leur langage d'entrée est la logique équationnelle avec des symboles provenant de divers fragments décidables utiles tels que les symboles non interprétés, l'arithmétique linéaire et des structures de données habituelles comme les tableaux ou les listes. Dans cette thèse, nous présentons une approche pour combiner des procédures de décision et des solveurs propositionnels dans un solveur SMT. Cette approche est fondée non seulement sur l'échange d'égalités déductibles entre les procédures de décision, mais aussi sur la génération d'égalités de modèle par des procédures de décision. Cela étend très bien la procédure classique de combinaison due à Nelson-Oppen dans une simple plate-forme pour combiner sans heurts des théories convexes et non convexes. Deuxièmement, nous présentons un algorithme original pour le fragment de l'arithmétique, appelé la logique de différence, et les détails sur la façon de mettre en oeuvre une procédure de décision basée sur cet algorithme. La logique de différence est modélisée en utilisant la théorie des graphes. Les déductions et les vérification de la cohérence effectués par l'algorithme se font par des recherches de cycles négatifs et des calculs de plus courts chemins de manière incrémentale. La dernière partie de la thèse présente une variation incrémentale originale de la méthode du simplexe que nous utilisons pour construire une procédure de décision pour l'arithmétique linéaire. Comme pour la logique de différence, nous présentons les détails de la procédure de décision qui la rend approprié pour notre plate-forme de combinaison utilisée par des solveurs SMT. Les méthodes et les techniques décrites dans cette thèse ont été mises en oeuvre et sont disponibles dans notre solveur SMT open-source, veriT.

Les solveurs SMT sont des outils dédiés à la vérification d'un ensemble de formules mathématiques, en général sans quantificateurs, utilisant un certain nombre de théories prédéfinies, telles que la congruence, l'arithmétique linéaire sur les entiers, les rationnels ou les réels, les tableaux de bits ou les tableaux. Ajouter une nouvelle théorie à un solveur SMT nécessite en général une connaissance assez profonde du fonctionnement interne du solveur, et, de ce fait, ne peut en général être exécutée que par ses développeurs. Pour de nombreuses théories, il est également possible de fournir une axiomatisation finie en logique du premier ordre. Toutefois, si les solveurs SMT sont généralement complets et efficaces sur des problèmes sans quantificateurs, ils deviennent imprévisibles en logique du premier ordre. Par conséquent, cette approche ne peut pas être utilisée pour fournir une procédure de décision pour ces théories. Dans cette thèse, nous proposons un cadre d'application permettant de résoudre ce problème en utilisant des déclencheurs. Les déclencheurs sont des annotations permettant de spécifier la forme des termes avec lesquels un quantificateur doit être instancié pour obtenir des instances utiles pour la preuve. Ces annotations sont utilisées par la majorité des solveurs SMT supportant les quantificateurs et font partie du format SMT-LIB v2. Dans notre cadre d'application, l'utilisateur fournit une axiomatisation en logique du premier ordre de sa théorie, ainsi qu'une démonstration de sa correction, de sa complétude et de sa terminaison, et obtient en retour un solveur correct, complet et qui termine pour sa théorie. Dans cette thèse, nous décrivons comment un solveur SMT peut être étendu à notre cadre nous basant sur l'algorithme DPLL modulo théories, utilisé traditionnellement pour modéliser ls solveurs SMT. Nous prouvons également que notre extension a bien les propriétés attendues. L'effort à fournir pour implémenter cette extension dans un solveur SMT existant ne doit être effectué qu'une fois et le mécanisme peut ensuite être utilisé sur de multiples théories axiomatisées. De plus, nous pensons que, en général, cette implémentation n'est pas plus compliquée que l'ajout d'une unique théorie au solveur. Nous avons fait ce travail pour le solveur SMT Alt-Ergo, nous en présentons certains détails dans la thèse. Pour valider l'utilisabilité de notre cadre d'application, nous avons prouvé la complétude et la terminaison de plusieurs axiomatizations, dont une pour les listes impératives doublement chaînée, une pour les ensembles applicatifs et une pour les vecteurs de Ada. Nous avons ensuite utilisé notre implémentation dans Alt-Ergo pour discuter de l'efficacité de notre système dans différents cas.

Cette thèse propose une approche de filtrage originale, SND en abrégé pour Scoring-based Neighborhood Dominance, pour le problème d’isomorphisme de sous- graphe. En raisonnant sur des propriétés de dominance entre sommets basées sur diverses fonctions de score et de voisinage, SND apparait comme un puissant mécanisme de filtrage. Une spécialisation de SND est étudiée, elle est basée sur le nombre de chemins de longueur k comme fonction de score ainsi que trois manières de considérer le voisinage. Avec cette spécialisation, il est montré que SND est plus puissant que LAD et incomparable à SAC (Singleton Arc Consistency). L'étude expérimentale montre que SND atteint dans la plupart des cas les mêmes performances en terme de filtrage que SAC tout en étant plus rapide de plusieurs ordres de grandeurs. Cela permet de résoudre le problème d’isomorphisme de sous-graphe en étant beaucoup plus efficace que MAC et légèrement meilleur que LAD.Un solveur de contraintes est également proposé ainsi qu'une optimisation du processus de propagation de MAC. / This thesis presents anoriginal filtering approach, called SND(Scoring- based Neighborhood Dominance), for the subgraph isomorphism problem. By reasoning on vertex dominance properties based on various scoring and neigh- borhood functions, SND appears to be a filtering mechanism of strong inference potential. For example, the recently proposed method LAD is a particular case of SND. A specialization is studied of SND : by considering the number of k-length paths in graphs and three ways of relating sets of vertices. With this specialization, we prove that SND is stronger than LAD and incomparable to SAC (Single- ton Arc Consistency). Our experimental results show that SND achieves most of the time the same filtering performances as SAC (while being several orders of magnitude faster), which allows one to find subisomorphism functions far more efficiently than MAC, while slightly outperforming LAD.

Les solveurs SMT sont des outils dédiés à la vérification d'un ensemble de formules mathématiques, en général sans quantificateurs, utilisant un certain nombre de théories prédéfinies, telles que la congruence, l'arithmétique linéaire sur les entiers, les rationnels ou les réels, les tableaux de bits ou les tableaux. Ajouter une nouvelle théorie à un solveur SMT nécessite en général une connaissance assez profonde du fonctionnement interne du solveur, et, de ce fait, ne peut en général être exécutée que par ses développeurs. Pour de nombreuses théories, il est également possible de fournir une axiomatisation finie en logique du premier ordre. Toutefois, si les solveurs SMT sont généralement complets et efficaces sur des problèmes sans quantificateurs, ils deviennent imprévisibles en logique du premier ordre. Par conséquent, cette approche ne peut pas être utilisée pour fournir une procédure de décision pour ces théories. Dans cette thèse, nous proposons un cadre d'application permettant de résoudre ce problème en utilisant des déclencheurs. Les déclencheurs sont des annotations permettant de spécifier la forme des termes avec lesquels un quantificateur doit être instancié pour obtenir des instances utiles pour la preuve. Ces annotations sont utilisées par la majorité des solveurs SMT supportant les quantificateurs et font partie du format SMT-LIB v2. Dans notre cadre d'application, l'utilisateur fournit une axiomatisation en logique du premier ordre de sa théorie, ainsi qu'une démonstration de sa correction, de sa complétude et de sa terminaison, et obtient en retour un solveur correct, complet et qui termine pour sa théorie. Dans cette thèse, nous décrivons comment un solveur SMT peut être étendu à notre cadre nous basant sur l'algorithme DPLL modulo théories, utilisé traditionnellement pour modéliser ls solveurs SMT. Nous prouvons également que notre extension a bien les propriétés attendues. L'effort à fournir pour implémenter cette extension dans un solveur SMT existant ne doit être effectué qu'une fois et le mécanisme peut ensuite être utilisé sur de multiples théories axiomatisées. De plus, nous pensons que, en général, cette implémentation n'est pas plus compliquée que l'ajout d'une unique théorie au solveur. Nous avons fait ce travail pour le solveur SMT Alt-Ergo, nous en présentons certains détails dans la thèse. Pour valider l'utilisabilité de notre cadre d'application, nous avons prouvé la complétude et la terminaison de plusieurs axiomatizations, dont une pour les listes impératives doublement chaînée, une pour les ensembles applicatifs et une pour les vecteurs de Ada. Nous avons ensuite utilisé notre implémentation dans Alt-Ergo pour discuter de l’efficacité de notre système dans différents cas. / SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this thesis, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the thesis. To show that our framework can handle complex theories, we prove completeness and termination of three axiomatization, one for doubly-linked lists, one for applicative sets, and one for Ada's vectors. Our tests show that, when the theory is heavily used, our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating these data-structures.

Cette thèse présente différentes techniques permettant de résoudre le problème de satisfaction de formule booléenes utilisant le parallélisme et du calcul distribué. Dans le but de fournir une explication la plus complète possible, une présentation détaillée de l'algorithme CDCL est effectuée, suivi d'un état de l'art. De ce point de départ, deux pistes sont explorées. La première est une amélioration d'un algorithme de type portfolio, permettant d'échanger plus d'informations sans perte d'efficacité. La seconde est une bibliothèque de fonctions avec son interface de programmation permettant de créer facilement des solveurs SAT distribués. / This thesis presents different technique to solve the Boolean satisfiability problem using parallel and distributed architectures. In order to provide a complete explanation, a careful presentation of the CDCL algorithm is made, followed by the state of the art in this domain. Once presented, two propositions are made. The first one is an improvement on a portfolio algorithm, allowing to exchange more data without loosing efficiency. The second is a complete library with its API allowing to easily create distributed SAT solver.

Dans ce manuscrit, nous présentons une méthode d’optimisation de forme qui se base sur des paramètres géométriques comme des longueurs, des angles, etc. Nous nous appuyons sur des techniques d’optimisation basées sur un gradient. La sensibilité de la fonction objectif par rapport à la position des noeuds du maillage nous est fournie par un solveur adjoint que l’on considère comme une boîte noire. Afin d’optimiser par rapport aux paramètres CAO, nous nous concentrons sur l’évaluation de la sensibilité de la position des noeuds par rapport à ces paramètres. Ainsi, nous proposons deux approches par différences finies. La première méthode s’appuie sur une projection harmonique afin de comparer dans un même espace le maillage initial et celui obtenu suite à la variation d’un paramètre CAO. Les développements présentés dans ce manuscrit permettent d’étendre l’application aux formes ayant plusieurs frontières comme les collecteurs d’échappement. Nous avons développé une méthode d’interpolation adaptée à cette comparaison. L’ensemble du processus a été automatisé et nous en montrons l’entière efficacité sur des applications industrielles en aérodynamique interne. La deuxième méthode se base directement sur les géométries CAO pour évaluer cette sensibilité. Nous utilisons la définition intrinsèque des patches dans l’espace paramétrique (u;v) pour effectuer cette comparaison. Grâce à l’utilisation des coordonnées exactes en tout point de la surface fournies par la CAO, nous évitons d’avoir recours à une interpolation afin d’avoir la meilleure précision de calcul possible. Cependant, contrairement à la première méthode, elle requiert d’identifier les correspondances entre les patches d’une forme à l’autre. Une application sur un cas académique a été faite en aérodynamique externe. La pertinence de la première méthode a été démontrée sur des cas représentatifs et multiobjectifs, ce qui permettrait de faciliter son déploiement et son utilisation dans un cadre industriel. Quant à la deuxième méthode, nous avons montré son fort potentiel. Cependant, des développements supplémentaires seraient nécessaires pour une application plus poussée. Du fait qu’elles sont indépendantes des solveurs mécaniques et du nombre de paramètres, ces méthodes réduisent considérablement les temps de développement des produits, notamment en permettant l’optimisation multiphysique en grande dimension. / In this manuscript, we present a shape optimization method based on CAD parameters such as lengths, angles, etc. We rely on gradient-based optimization techniques. The sensitivity of the objective function, with respect to the mesh nodes position, is provided by an adjoint solver considered here as a black box. To optimize with respect to CAD parameters, we focus on computing the sensitivity of the nodes positions with respect to these parameters. Thus, we propose two approaches based on finite differences. The first method uses a harmonic projection to compare in the same space the initial mesh and the one obtained after a change of the set of CAD parameters. The developments presented in this manuscript open up new doors like the application to shapes with multiple borders such as exhaust manifolds. We also developed an interpolation method suitable for this comparison. The entire process is automated, and we demonstrate the entire effectiveness on internal aerodynamics industrial applications. The second method is directly based on the CAD geometries to assess this sensitivity. To perform this comparison, we use the intrinsic definition of the patches in the parametric space (u;v). Through the use of the exact coordinates at any point on the surface provided by the CAD, we avoid using an interpolation to get the best calculation accuracy possible. However, unlike the first method, it requires to identify the correspondence between patches from one shape to another. An application on an external aerodynamics academic case was made. The relevance of the first method is demonstrated on a representative multi-objective case, which facilitate its deployment use in an industrial environment. Regarding the second method, we showed its great potential. However, further developments are needed to handle more advanced cases. Because they are independent of the mechanical solver and the number of parameters, these methods significantly reduce product development time, particularly by allowing large and multiphysics optimization.