As the circuit size increases in modern electronics, the design process becomes more complicated. Even though the hardware design process is divided into multiple phases, many of the divided problems are still extremely time consuming to solve. One of these NP-hard problems is the routing problem. As electronics step into the deep submicron era, optimizing the routing becomes increasingly important. One of the methods to solve global routing is to formulate the problem as an integer programming (IP) problem. This formulation can then be relaxed into a linear programming problem and solved using interior point method. This thesis investigates two new approaches to optimize the speed of solving global routing using Karmarkar’s interior point method, as well as the effect of combining various optimizations with these new approaches. The first proposed approach is to utilize solution stability as the interior point loop converges, and attempt to remove solutions that have already stabilized. This approach reduces the problem size and allows subsequent interior point iterations to proceed faster. The second proposed approach is to solve the inner linear system (projection step) in interior point method in parallel. Experimental results show that for large routing problems, the performance of the solver is improved by the optimization approaches. The problem reduction stage allows for great speedup in the interior point iterations, without affecting the quality of the solution significantly. Furthermore, the timing required to solve inner linear system in the interior point method is improved by solving the problem in parallel. With these optimizations, solving the routing problem using the IP formation becomes increasingly more efficient. By solving an efficient parallel IP formation rather than a traditional sequential approach, more efficient optimal solutions which incorporate multiple conflicting objectives can be achieved.

Deciding the truth of a Quantified Boolean Formula (QBF) is a canonical PSPACE-complete problem. It provides a powerful framework for encoding problems that lie in PSPACE. These include many problems in automatic verification, and problems with discrete uncertainty or non-determinism. Two person adversarial games are another type of problem that are naturally encoded in QBF. It is standard practice to use Conjunctive Normal Form (CNF) when representing QBFs. Any propositional formula can be efficiently translated to CNF via the addition of new variables, and solvers can be implemented more efficiently due to the structural simplicity of CNF. However, the translation to CNF involves a loss of some structural information. This thesis shows that this structural information is important for efficient QBF solving, and shows how this structural information can be utilized to improve state-of-the-art QBF solving. First, a non-CNF circuit-based solver is presented. It makes use of information not present in CNF to improve its performance. We present techniques that allow it to exploit the duality between solutions and conflicts that is lost when working with CNF. This duality can also be utilized in the production of certificates, allowing both true and false formulas to have easy-to-verify certificates of the same form. Then, it is shown that most modern CNF-based solvers can benefit from the additional information derived from duality using only minor modifications. Furthermore, even partial duality information can be helpful. We show that for standard methods for conversion to CNF, some of the required information can be reconstructed from the CNF and greatly benefit the solver.

Deciding the truth of a Quantified Boolean Formula (QBF) is a canonical PSPACE-complete problem. It provides a powerful framework for encoding problems that lie in PSPACE. These include many problems in automatic verification, and problems with discrete uncertainty or non-determinism. Two person adversarial games are another type of problem that are naturally encoded in QBF. It is standard practice to use Conjunctive Normal Form (CNF) when representing QBFs. Any propositional formula can be efficiently translated to CNF via the addition of new variables, and solvers can be implemented more efficiently due to the structural simplicity of CNF. However, the translation to CNF involves a loss of some structural information. This thesis shows that this structural information is important for efficient QBF solving, and shows how this structural information can be utilized to improve state-of-the-art QBF solving. First, a non-CNF circuit-based solver is presented. It makes use of information not present in CNF to improve its performance. We present techniques that allow it to exploit the duality between solutions and conflicts that is lost when working with CNF. This duality can also be utilized in the production of certificates, allowing both true and false formulas to have easy-to-verify certificates of the same form. Then, it is shown that most modern CNF-based solvers can benefit from the additional information derived from duality using only minor modifications. Furthermore, even partial duality information can be helpful. We show that for standard methods for conversion to CNF, some of the required information can be reconstructed from the CNF and greatly benefit the solver.

Currently, the Southern Illinois University Carbondale (SIUC) power plant produces steam at high pressure to drive a high pressure (HP) turbine to make a portion of the electrical power needed by campus, then using 969 kPa (125 psig) steam to provide hot water all year, heat buildings, and to operate a low pressure (LP) turbine that powers the compressor of the central air conditioning (A/C) system. In the proposed system, the HP turbine is replaced by a much higher efficiency, multi-level turbine, the LP turbine is replaced with a motor and Variable Frequency Drive (VFD), and a cooling tower is added to condense more possible steam. This thesis has provided computer models to evaluate the economical feasibility of the proposed system, which are written by using Engineering Equation Solver (EES) software. The results of the study are presented in two cases. Case 1 examines the same amount of coal use between current and proposed systems, while Case 2 exames operating the high pressure boiler at the maximum rate. The results are a cost savings of $1,921,000 and $3,604,000 with payback periods of 4 and 2.2 years for Case 1 and Case 2, respectively. The annual primary energy saved and CO2 reduction from this modification was 200,000 GJ and 564,814 moles, respectively.

Many problems in nature can be represented as some kind of a satisfiability problem. Several SAT solvers and SMT solvers have been developed in the last decade with the goal of checking the satisfiability of different SAT problems. An all-solution satisfiability modulo theories on top of the Z3 SMT solver is presented that uses the clause blocking algorithm to find all the solution sets of a SAT problem. Then, an incremental All-SMT solver has been presented based on the all-SMT solver which is able to find the satisfiable answers of an incremental SMT problem based on the solution set of the original problem.

Desde a diminuição da tendência de aumento na frequência de processadores, uma nova tendência surgiu para permitir que softwares tirem proveito de harwares mais rápidos: a paralelização. Contudo, diferente de aumentar a frequência de processadores, utilizar parallelização requer um tipo diferente de programação, a programação paralela, que é geralmente mais difícil que a programação sequencial comum. Neste contexto, a paralelização automática apareceu, permitindo que o software tire proveito do paralelismo sem a necessidade de programação paralela. Nós apresentamos aqui duas propostas: SAT-PaDdlinG e RePaSAT. SAT-PaDdlinG é um SAT Solver DPLL paralelo que roda em GPU, o que permite que RePaSAT utilize esse ambiente. RePaSAT é a nossa proposta de uma máquina paralela que utiliza o Problema SAT para paralelizar automaticamente código sequencial. Como uma GPU provê um ambiente barato e massivamente paralelo, SAT-PaDdlinG tem como objetivo prover esse paralelismo massivo a baixo custo para RePaSAT, como para qualquer outra ferramenta ou problema que utilize SAT Solvers. / Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization. However, different from increasing the frequency of processors, using parallelization requires a different kind of programming, parallel programming, which is usually harder than common sequential programming. In this context, automatic parallelization has arisen, allowing software to take advantage of parallelism without the need of parallel programming. We present here two proposals: SAT-PaDdlinG and RePaSAT. SAT-PaDdlinG is a parallel DPLL SAT Solver on GPU, which allows RePaSAT to use this environment. RePaSAT is our proposal of a parallel machine that uses the SAT Problem to automatically parallelize sequential code. Because GPU provides a cheap, massively parallel environment, SATPaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.

Desde a diminuição da tendência de aumento na frequência de processadores, uma nova tendência surgiu para permitir que softwares tirem proveito de harwares mais rápidos: a paralelização. Contudo, diferente de aumentar a frequência de processadores, utilizar parallelização requer um tipo diferente de programação, a programação paralela, que é geralmente mais difícil que a programação sequencial comum. Neste contexto, a paralelização automática apareceu, permitindo que o software tire proveito do paralelismo sem a necessidade de programação paralela. Nós apresentamos aqui duas propostas: SAT-PaDdlinG e RePaSAT. SAT-PaDdlinG é um SAT Solver DPLL paralelo que roda em GPU, o que permite que RePaSAT utilize esse ambiente. RePaSAT é a nossa proposta de uma máquina paralela que utiliza o Problema SAT para paralelizar automaticamente código sequencial. Como uma GPU provê um ambiente barato e massivamente paralelo, SAT-PaDdlinG tem como objetivo prover esse paralelismo massivo a baixo custo para RePaSAT, como para qualquer outra ferramenta ou problema que utilize SAT Solvers. / Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization. However, different from increasing the frequency of processors, using parallelization requires a different kind of programming, parallel programming, which is usually harder than common sequential programming. In this context, automatic parallelization has arisen, allowing software to take advantage of parallelism without the need of parallel programming. We present here two proposals: SAT-PaDdlinG and RePaSAT. SAT-PaDdlinG is a parallel DPLL SAT Solver on GPU, which allows RePaSAT to use this environment. RePaSAT is our proposal of a parallel machine that uses the SAT Problem to automatically parallelize sequential code. Because GPU provides a cheap, massively parallel environment, SATPaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.

Desde a diminuição da tendência de aumento na frequência de processadores, uma nova tendência surgiu para permitir que softwares tirem proveito de harwares mais rápidos: a paralelização. Contudo, diferente de aumentar a frequência de processadores, utilizar parallelização requer um tipo diferente de programação, a programação paralela, que é geralmente mais difícil que a programação sequencial comum. Neste contexto, a paralelização automática apareceu, permitindo que o software tire proveito do paralelismo sem a necessidade de programação paralela. Nós apresentamos aqui duas propostas: SAT-PaDdlinG e RePaSAT. SAT-PaDdlinG é um SAT Solver DPLL paralelo que roda em GPU, o que permite que RePaSAT utilize esse ambiente. RePaSAT é a nossa proposta de uma máquina paralela que utiliza o Problema SAT para paralelizar automaticamente código sequencial. Como uma GPU provê um ambiente barato e massivamente paralelo, SAT-PaDdlinG tem como objetivo prover esse paralelismo massivo a baixo custo para RePaSAT, como para qualquer outra ferramenta ou problema que utilize SAT Solvers. / Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization. However, different from increasing the frequency of processors, using parallelization requires a different kind of programming, parallel programming, which is usually harder than common sequential programming. In this context, automatic parallelization has arisen, allowing software to take advantage of parallelism without the need of parallel programming. We present here two proposals: SAT-PaDdlinG and RePaSAT. SAT-PaDdlinG is a parallel DPLL SAT Solver on GPU, which allows RePaSAT to use this environment. RePaSAT is our proposal of a parallel machine that uses the SAT Problem to automatically parallelize sequential code. Because GPU provides a cheap, massively parallel environment, SATPaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.

Flood propagation over urban areas can cause an interaction between the free-surface flow and large underground pipe networks used for storm drainage and sewage, causing outflows and inflows at the bed. The associated waves may collide with each other and the surface waves. In this thesis the shallow water equations are used to model this type of wave interaction over dry or wet beds with bathymetry gradients and friction terms. The proposed shallow water scheme is solved based on finite volume high-resolution Godunov-type methods. The solver is well-balanced and can accurately balance the source terms and flux-gradients for the steady-state solutions. The solver also utilises a new type of Riemann wave speed to provide depth-positive results over nearly dry beds and dry states. Additionally a new type of source term is introduced in the continuity equation to model pipe inflow and outflow conditions at bed connections. For the standard one-dimensional shallow water equations the numerical results are validated with analytical solutions or other reference solutions provided in the literature. This includes the incipient Riemann problems for nearly dry and dry-states, steady flow over a hump in a rectangular channel and the wave propagation problem. Eventually, the generation of dry bed in the middle, over discontinuous topography is considered. Close agreement is achieved between the shallow water scheme and analytical or reference solutions for the above test cases. For the shallow water problems with influx/efflux source terms comparisons are made with STAR-CD, a commercial Navier-Stokes solver for general fluid flow prediction. The shallow water model is first used to simulate vertical flows through finite gaps in the bed. Next, the interaction of the vertical flows with a dam-break flow is considered for both dry and wet beds. An efflux number, En, is defined based on the vertical efflux velocity and the gap length. A parameter study is undertaken to investigate the effect of the one-dimensional approximation of the present model, for a range of non-dimensional efflux numbers. It is found that the shallow flow model gives sensible predictions at all times provided En<0.5, and for long durations for En>0.5. Dam break flow over an underground connecting pipe is also considered for the one-dimensional efflux problems. To solve two-dimensional problems the shallow water scheme uses the dimensional-splitting method which solves each one-dimensional Riemann problem in the x- and y-directions separately. The cross-derivative terms for second-order accuracy are incorporated by solving another Riemann problem in the orthogonal direction. For two-dimensional problems first the dam-break problems are considered over wet and dry beds. Then, flood propagation over complex terrain is demonstrated. Next, efflux discharge is modelled in isolation over a dry bed and then with dam-break interaction, comparing with STAR-CD results. Again very good agreement is shown between the two-dimensional shallow water model and STAR-CD for the efflux numbers of En<0.5. For modelling the inundation problem over an underground pipe network the solver is coupled with the general underground pipe network solver to calculate the efflux discharge as the flood waves pass through the pipe network. For analysing the pipe network with unknown effluxes an additional set of equations is incorporated into the solution of a general pipe network solver. The shallow water solver coupled to an underground pipe network is then used to simulate dam-break interaction with pipe networks with 9 and 25 nodes to demonstrate the versatility of the method.

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).