The method of moment (MoM) [1] is a widely used method in electromagnetics to solve static and dynamic electromagnetic problems on varying geometries. However, in closely spaced geometries coupled with large aspect ratios, e.g. a large parallel plate capacitor with very small separation gap, the problem exhibits several challenges. Firstly, the close proximity of the field and source elements presents problems with convergence in numerical evaluations of the interactions between them. Secondly, the aspect ratio of the geometry gives an approximation whereby to far field points, the source contributions from locations that are far apart appear to cancel each other. This leads to high condition numbers in the system matrix. This thesis explores the potential solution to these problems as well as the application of modular fast and direct (MFD) [2] solver to expedite the solution of such problems.

This study focuses on developing novel modeling techniques for fiber-reinforced composites with polymer and ceramic matrix based on Peridynamic approach. To capture the anisotropic material behaviors of composites under quasi-static and dynamic loading conditions, a new peridynamic model for composite laminate and a modified peridynamic approach for non-uniform discretization are proposed in this study. In order to achieve the numerical implementation of the proposed model and approach, a mixed implicit-explicit solver based on GPU parallel computing is developed as well. The new peridynamic model for composite laminates does not have any limitation in fiber orientation, material properties and stacking sequence. It can capture the expected orthotropic material properties and coupling behaviors in laminates with symmetric and asymmetric layups. Unlike the previous models, the new model enables the evaluation of stress and strain fields in each ply of the laminate. Therefore, it permits the use of existing stress- or strain-based failure criteria for damage prediction. The computation of strain energy stored at material points allows the energy-based failure criteria required for delamination propagation and fatigue crack growth. The capability of this approach is verified against benchmark solutions, and validated by comparison with the available experimental results for three laminate layups with an open hole under tension and compression. The modified peridynamic approach for non-uniform discretization enables computational efficiency and removes the effect of geometric truncations in the simulation. This approach is a modification to the original peridynamic theory by splitting the strain energy associated with an interaction between two material points according to the volumetric ratio arising from the presence of non-uniform discretization and variable horizon. It also removes the requirement for correction of peridynamic material parameters due to surface effects. The accuracy of this approach is verified against the benchmark solutions, and demonstrated by considering cracking in nuclear fuel pellet subjected to a thermal load with non-uniform discretizations. Unlike the previous peridynamic simulations which primarily employs explicit algorithm, this study introduces implicit algorithm to achieve peridynamic simulation under quasi-static loading condition. The Preconditioned Conjugate Gradient (PCG) and Generalized Minimal Residual (GMRES) algorithms are implemented with GPU parallel computing technology. Circulant preconditioner provides significant acceleration in the convergence of peridynamic analyses. To predict damage evolution, the simulation is continued with standard explicit algorithms. The validity and performance of this mixed implicit-explicit solver is established and demonstrated with benchmark tests.

Currently, the accurate prediction of the impact of an extreme wave on infrastructure located near shore is difficult to assess. There is a lack of established methods to accurately quantify these impacts. Extreme waves, such as tsunamis generate, through breaking, extremely powerful hydraulic bores that impact and significantly damage coastal structures and buildings located close to the shoreline. The damage induced by such hydraulic bores is often due to structural failure. Examples of devastating coastal disasters are the 2004 Indian Ocean Tsunami, 2005 Hurricane Katrina and most recently, the 2011 Tohoku Japan Tsunami. As a result, more advanced research is needed to estimate the magnitude of forces exerted on structures by such bores. This research presents results of a numerical model based on the Smoothed Particle Hydrodynamics (SPH) method which is used to simulate the impact of extreme hydrodynamic forces on shore protection walls. Typically, fluids are modeled numerically based on a Lagrangian approach, an Eulerian approach or a combination of the two. Many of the common problems that arise from using more traditional techniques can be avoided through the use of SPH-based models. Such challenges include the model computational efficiency in terms of complexity of implementation. The SPH method allows water particles to be individually modeled, each with their own characteristics, which then accurately depicts the behavior and properties of the flow field. An open source code, known as SPHysics, was used to run the simulations presented in this thesis. Several cases analysed consist of hydraulic bores impacting a flat vertical wall as well as a sloping seawall. The analysis includes comparisons of the numerical results with published experimental data. The model is shown to accurately reproduce the formation of solitary waves as well as their propagation and breaking. The impacting bore profiles as well as the resulting pressures are also efficiently simulated using the model.

Cette thèse porte sur la résolution séquentielle et parallèle du problème de la satisfiabilité propositionnelle(SAT). Ce problème important sur le plan théorique admet de nombreuses applications qui vont de la vérification formelle de matériels et de logiciels à la cryptographie en passant par la planification et la bioinformatique. Plusieurs contributions sont apportées dans cette thèse. La première concerne l’étude et l’intégration des concepts d’intensification et de diversification dans les solveurs SAT parallèle de type portfolio. Notre seconde contribution exploite l’état courant de la recherche partiellement décrit par les récentes polarités des littéraux « progress saving », pour ajuster et diriger dynamiquement les solveurs associés aux différentes unités de calcul. Dans la troisième contribution, nous proposons des améliorations de la stratégie de réduction de labase des clauses apprises. Deux nouveaux critères, permettant d’identifier les clauses pertinentes pour la suite de la recherche, ont été proposés. Ces critères sont utilisés ensuite comme paramètre supplémentaire de diversification dans les solveurs de type portfolio. Finalement, nous présentons une nouvelle approche de type diviser pour régner où la division s’effectue par ajout de contraintes particulières. / In this thesis, we deal with the sequential and parallel resolution of the problem SAT. Despite of its complexity, the resolution of SAT problem is an excellent and competitive approach for solving thecombinatorial problems such as the formal verification of hardware and software, the cryptography, theplanning and the bioinfomatics. Several contribution are made in this thesis. The first contribution aims to find the compromise of diversification and intensification in the solver of type portfolio. In our second contribution, we propose to dynamically adjust the configuration of a core in a portfolio parallel sat solver when it is determined that another core performs similar work. In the third contribution, we improve the strategy of reduction of the base of learnt clauses, we construct a portfolio strategy of reduction in parallel solver. Finally, we present a new approach named "Virtual Control" which is to distribute the additional constraints to each core in a parallel solver and verify their consistency during search.

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 cette thèse nous avons tout d'abord développé un solveur neutronique de cinétique transport 3D en géométrie déstructurée avec une discrétisation spatiale par éléments finis discontinus (solveur MINARET). L'écriture d'un tel code représente en soi une contribution importante dans la physique des réacteurs car il permettra de connaître de façon très précise l'état du c¿ur au cours d'accidents graves. Il jouera aussi un rôle important pour des études de fluence de la cuve des réacteurs. D'un point de vue mathématique, l'apport le plus important a consisté en l'implémentation d'algorithmes adaptés aux architectures de calcul parallèle, permettant de réduire de façon significative les temps de calcul. Un effort particulier a été mené pour paralléliser de façon efficace la variable temporelle par l'algorithme pararéel en temps. Nous avons ensuite cherché à développer une méthode qui permettrait d'utiliser MINARET comme outil de surveillance pendant l'opération d'un réacteur nucléaire. Une des difficultés majeures de ce problème réside dans le besoin de fournir les simulations en temps réel. La question a été abordée en développant tout d'abord une généralisation de la méthode Empirical Interpolation (EIM) grâce à laquelle on a pu définir un processus d'interpolation bien posé pour des fonctions appartenant à des espaces de Banach. Ceci est rendu possible par l'utilisation de formes linéaires d'interpolation au lieu des traditionnels points d'interpolation et une partie de cette thèse a été consacrée à la compréhension des propriétés théoriques de cette méthode (analyse de convergence sous hypothèse d'ensemble de petite dimension de Kolmogorov et étude de sa stabilité). / In this thesis, we have first developed a time dependent 3D neutron transport solver on unstructured meshes with discontinuous Galerkin finite elements spatial discretization. The solver (called MINARET) represents in itself an important contribution in reactor physics thanks to the accuracy that it can provide in the knowledge of the state of the core during severe accidents. It will also play an important role on vessel fluence calculations. From a mathematical point of view, the most important contribution has consisted in the implementation of algorithms that are well adapted for modern parallel architectures and that significantly decrease the computing times. A special effort has been done in order to efficiently parallelize the time variable by the use of the parareal in time algorithm. On a second stage, we have developed the foundations of a method with which we could use MINARET to monitor in real time the population of neutrons during the operation of the reactor. One of the major difficulties relies in the necessity of providing computations in real time. This question has been addressed by proposing an extension of the Empirical Interpolation Method (EIM) thanks to which a well-posed interpolation procedure has been defined for functions belonging to Banach spaces. This is possible thanks to the use of interpolating linear forms instead of the traditional interpolation points and a part of this thesis has been devoted to the understanding of the theoretical properties of this method (convergence analysis under the hypothesis of small Kolmogorov n-width and stability of the procedure).

abstract: The quest to find efficient algorithms to numerically solve differential equations isubiquitous in all branches of computational science. A natural approach to address this problem is to try all possible algorithms to solve the differential equation and choose the one that is satisfactory to one's needs. However, the vast variety of algorithms in place makes this an extremely time consuming task. Additionally, even after choosing the algorithm to be used, the style of programming is not guaranteed to result in the most efficient algorithm. This thesis attempts to address the same problem but pertinent to the field of computational nanoelectronics, by using PETSc linear solver and SLEPc eigenvalue solver packages to efficiently solve Schrödinger and Poisson equations self-consistently. In this work, quasi 1D nanowire fabricated in the GaN material system is considered as a prototypical example. Special attention is placed on the proper description of the heterostructure device, the polarization charges and accurate treatment of the free surfaces. Simulation results are presented for the conduction band profiles, the electron density and the energy eigenvalues/eigenvectors of the occupied sub-bands for this quasi 1D nanowire. The simulation results suggest that the solver is very efficient and can be successfully used for the analysis of any device with two dimensional confinement. The tool is ported on www.nanoHUB.org and as such is freely available. / Dissertation/Thesis / Masters Thesis Electrical Engineering 2020

Constraint-Based Local Search (CBLS) is a technology used to solve computationally hard optimisation problems. A model written in a solver-independent modelling language needs to be processed before it can be solved by a CBLS solver. In this processing step, it is necessary to identify invariants and create an invariant structure. How to best obtain such a structure, or even how to identify a good structure, is not clear. The purpose of this project is to develop a framework for evaluating invariant structures and structure identification schemes. To do this, we introduce a set of metrics, which are also evaluated. The evaluation shows that these metrics are useful for evaluating invariant structures and structure identification schemes. We introduce a notion of optimal invariant structures and show that these can in many cases be produced by simple structure identification schemes. Finally, we present a strategy that improves on these schemes and yields optimal invariant structures in even more cases.

This thesis deals with the problematic of test-data generation for relational databases. The aim of the this thesis is to design and implement tool which meets defined constrains and allows us to generate test-data. This tool uses SMT solver for constraint solving and test-data generation.