No description available.

Answer set programming (ASP) is a declarative programming paradigm oriented towards difficult combinatorial search problems. Syntactically, ASP programs look like Prolog programs, but solutions are represented in ASP by sets of atoms, and not by substitutions, as in Prolog. Answer set systems, such as Smodels, Smodelscc, and DLV, compute answer sets of a given program in the sense of the answer set (stable model) semantics. This is different from the functionality of Prolog systems, which determine when a given query is true relative to a given logic program. ASP has been applied to many areas of science and technology, from the design of a decision support system for the Space Shuttle to graph-theoretic problems arising in zoology and linguistics. The "native" answer set systems mentioned above are based on specialized search procedures. Usually these procedures are described fairly informally with the use of pseudocode. We propose an alternative approach to describing algorithms of answer set solvers. In this approach we specify what "states of computation" are, and which transitions between states are allowed. In this way, we define a directed graph such that every execution of a procedure corresponds to a path in this graph. This allows us to model algorithms of answer set solvers by a mathematically simple and elegant object, graph, rather than a collection of pseudocode statements. We use this abstract framework to describe and prove the correctness of the answer set solver Smodels, and also of Smodelscc, which enhances the former using learning and backjumping techniques. Answer sets of a tight program can be found by running a SAT solver on the program's completion, because for such a program answer sets are in a one-to-one correspondence with models of completion. SAT is one of the most widely studied problems in computational logic, and many efficient SAT procedures were developed over the last decade. Using SAT solvers for computing answer sets allows us to take advantage of the advances in the SAT area. For a nontight program it is still the case that each answer set corresponds to a model of program's completion but not vice versa. We show how to modify the search method typically used in SAT solvers to allow testing models of completion and employ learning to utilize testing information to guide the search. We develop a new SAT-based answer set solver, called Cmodels, based on this idea. We develop an abstract graph based framework for describing SAT-based answer set solvers and use it to represent the Cmodels algorithm and to demonstrate its correctness. Such representations allow us to better understand similarities and differences between native and SAT-based answer set solvers. We formally compare the Smodels algorithm with a variant of the Cmodels algorithm without learning. Abstract frameworks for describing native and SAT-based answer set solvers facilitate the development of new systems. We propose and implement the answer set solver called SUP that can be seen as a combination of computational ideas behind Cmodels and Smodels. Like Cmodels, solver SUP operates by computing a sequence of models of completion of the given program, but it does not form the completion. Instead, SUP runs the Atleast algorithm, one of the main building blocks of the Smodels procedure. Both systems Cmodels and SUP, developed in this dissertation, proved to be competitive answer set programming systems. / text

This dissertation introduces a novel fast direct solver and preconditioner for the solution of block tridiagonal linear systems that arise from the discretization of elliptic partial differential equations on a Cartesian product mesh, such as the variable-coefficient Poisson equation, the convection-diffusion equation, and the wave Helmholtz equation in heterogeneous media. The algorithm extends the traditional cyclic reduction method with hierarchical matrix techniques. The resulting method exposes substantial concurrency, and its arithmetic operations and memory consumption grow only log-linearly with problem size, assuming bounded rank of off-diagonal matrix blocks, even for problems with arbitrary coefficient structure. The method can be used as a standalone direct solver with tunable accuracy, or as a black-box preconditioner in conjunction with Krylov methods. The challenges that distinguish this work from other thrusts in this active field are the hybrid distributed-shared parallelism that can demonstrate the algorithm at large-scale, full three-dimensionality, and the three stressors of the current state-of-the-art multigrid technology: high wavenumber Helmholtz (indefiniteness), high Reynolds convection (nonsymmetry), and high contrast diffusion (inhomogeneity). Numerical experiments corroborate the robustness, accuracy, and complexity claims and provide a baseline of the performance and memory footprint by comparisons with competing approaches such as the multigrid solver hypre, and the STRUMPACK implementation of the multifrontal factorization with hierarchically semi-separable matrices. The companion implementation can utilize many thousands of cores of Shaheen, KAUST's Haswell-based Cray XC-40 supercomputer, and compares favorably with other implementations of hierarchical solvers in terms of time-to-solution and memory consumption.

No description available.

Numerical simulation of wave behaviour in shallow and deep water is often a key aspect of ocean, coastal, and river hydrodynamic studies. This thesis derives nonlinear one- and two-dimensional level I Green-Naghdi (GN) equations that model the motions of free surface waves in shallow water over non-uniform bed topography. By assuming fitted velocity profiles through the depth, GN equations are simpler than Boussinesq equations, while retaining the wave dispersion property. Implicit matrix solvers are used to solve the spatially discretised 1D and 2D GN equations, with a 4th order Runge Kutta scheme used for time integration. To verify the developed numerical solvers of 1D GN equations, a series of simulations are undertaken for standard benchmark tests including sloshing in a tank and solitary wave propagation over a flat bed. In all cases, grid convergence tests were conducted. In the sloshing test, both numerical schemes and the analytical solution were in complete agreement for small-amplitude free surface motions. At larger values of initial sloshing amplitude, the nonlinear effects caused the free surface waves to steepen, and eventually the numerical simulations became unstable. This could be resolved in future using a shock-capturing scheme. Excellent agreement was achieved between the numerical predictions and analytical solution for solitary waves propagating. The 2D GN equation solver was then verified for the benchmark tests of Gaussian hump sloshing and solitary wave propagation in closed basin. The predicted free surface motions for Gaussian hump sloshing were in good agreement with linear Fourier analytical solutions for a certain initial period, after which nonlinear effects started to dominate the numerical solution. A reversibility check was undertaken. Nonlinear effects were investigated by increasing the amplitude of the hump, and applying harmonic separation (by comparison against slosh predictions for a corresponding Gaussian trough). It was found that the even harmonic components provided a useful indication of the nonlinear behaviour of the 2D GN equations. 2D GN simulations of a 0.6 m amplitude solitary wave propagation in 1 m deep water over a flat, horizontal bed confirmed that nonlinear interaction was correctly modelled, when the solitary wave hit a solid wall and its runup reached 2.36 m which was 0.36m more than the linear analytical solution and almost identical to a second order solution.

abstract: Global optimization (programming) has been attracting the attention of researchers for almost a century. Since linear programming (LP) and mixed integer linear programming (MILP) had been well studied in early stages, MILP methods and software tools had improved in their efficiency in the past few years. They are now fast and robust even for problems with millions of variables. Therefore, it is desirable to use MILP software to solve mixed integer nonlinear programming (MINLP) problems. For an MINLP problem to be solved by an MILP solver, its nonlinear functions must be transformed to linear ones. The most common method to do the transformation is the piecewise linear approximation (PLA). This dissertation will summarize the types of optimization and the most important tools and methods, and will discuss in depth the PLA tool. PLA will be done using nonuniform partitioning of the domain of the variables involved in the function that will be approximated. Also partial PLA models that approximate only parts of a complicated optimization problem will be introduced. Computational experiments will be done and the results will show that nonuniform partitioning and partial PLA can be beneficial. / Dissertation/Thesis / Doctoral Dissertation Mathematics 2020

Testing code is important, but writing test cases can be time consuming, particularly for beginning programmers who are already struggling to write an implementation. We present TestBuilder, a system for test case generation which uses an SMT solver to generate inputs to reach specified lines in a function, and asks the user what the expected outputs would be for those inputs. The resulting test cases check the correctness of the output, rather than merely ensuring the code does not crash. Further, by querying the user for expectations, TestBuilder encourages the programmer to think about what their code ought to do, rather than assuming that whatever it does is correct. We demonstrate, using mutation testing of student projects, that tests generated by TestBuilder perform better than merely compiling the code using Python’s built-in compile function, although they underperform the tests students write when required to achieve 100% test coverage.

This project is an attempt to design a new English curriculum to fit a major organizational and philosophical change planned for Westmount Secondary School in the year 1990. Chapter 1 describes the context in which the innovation will take place, the nature of the innovation itself and the primary objective the changes is intended to fulfil; namely, the development of students who are self-directed problem-solvers. Chapter 2 attempts to clarify this objective by examining the origins of problem-solving in education and describing some recent accounts of its use, most notably in problem-based learning. Chapter 3 explores the philosophy of self-directed learning and differentiates among the many similar related terms. Autonomy is identified as the key feature of self-directed learning. Chapter 4 outlines the constraints on curriculum design imposed by the new English Guideline recently published by the Ministry of Education. Finally, in chapter 5 an attempt is made to identify the features common to both self-direction and problem-solving and adapt these to the requirements of "Westmount 1990" and the English Guideline. The result is a proposal for a problem-based independent Grade 12 course outlined in Chapter 6. / Thesis / Master of Arts (MA)

No description available.

In this thesis we discuss a formal approach to the design of concurrent error detection (CED) logic in field-programmable gate arrays (FPGAs). Single event upsets (SEUs) occurring in look-up table (LUT) configuration bits are considered as the fault model. Our approach involves representing the LUT network of the design implemented in the FPGA with constraints to model the presence of SEUs as a boolean formula in conjunctive normal form. A quantified boolean formula (QBF) based approach to designing CED logic based on parity check codes is found to be infeasible for designs of a realistic size. It is shown that a satisfiability (SAT) solver can be used to find variable assignments that indicate which circuit outputs can be corrupted by upset events in the specified fault model. An algorithm is presented to automatically generate a parity check code, which will identify with one clock cycle detection latency a malfunction caused by an SEU. The resulting parity check logic can be verified using a SAT solver and it is shown to require fewer LUT resources than duplication for most circuits. / Master of Applied Science (MASc)