O Objetivo deste trabalho foi implementar um resolvedor distribuído para o problema de satisfabilidade em lógica proposicional (SAT) que pudesse ser executado em uma grade de computadores. Foi analisada a influência que o número de máquinas utilizadas pela grade para resolver diversas instâncias do SAT exerce sobre o desempenho do resolvedor implementado / O Objetivo deste trabalho foi implementar um resolvedor distribuído para o problema de satisfabilidade em lógica proposicional (SAT) que pudesse ser executado em uma grade de computadores. Foi analisada a influência que o número de máquinas utilizadas pela grade para resolver diversas instâncias do SAT exerce sobre o desempenho do resolvedor implementado

The NP-complete k-SAT problem - decide wether a given formula is satisfiable - is of fundamental importance in theoretical computer science. In this dissertation we study random 4-SAT formulas with > 116 n^2 clauses. These formulas are almost surly unsatisfiable. Here we show the existence of a polynomial time algorithm that certifies the unsatisfiability. Therefore we study the discrepancy of hypergraphs and multigraphs. We also combine spectral techniques with approximation algorithms to achieve the new result. Our new algorithm is adaptable for Not-All-Equal-4-SAT and the 2-colouring of 4-uniform hypergraphs. We also extends the Hajos construction of non k-colourable graphs to non k-colourable uniform hypergraphs. / Das NP-vollständige Problem k-SAT ist von zentraler Bedeutung in der theoretischen Informatik. In der Dissertation werden zufällige 4-SAT-Formeln mit > n^2 vielen Klauseln studiert. Diese Formeln sind mit hoher Wahrscheinlichkeit unerfüllbar. Hier wird erstmalig die Existenz eines Algorithmus gezeigt, der diese Unerfüllbarkeit effizient verifiziert. Hierfür wird die geringe Diskrepanz von Hypergrpahen und Multigraphen betrachtet. Der Schlüssel zu diesem Algorithmus liegt in der Kombination von spektralen Techniken mit Approximationsalgorithmen der klassischen kombinatorischen Optimierung. Der vorgestellte Algorithmus kann auf den effizienten Nachweis der Unerfüllbarkeit von Not-All-Equal-4-SAT-Formeln und die Nicht-2-Färbbarkeit von 4-uniformen Hypergraphen erweitert werden. Es wird ebenfalls eine Erweiterung der Hajos-Konstruktion nicht k-färbbarer Graphen auf nicht k-färbbare uniforme Hypergraphen angegeben.

In contrast to a single clause a pseudo-Boolean (PB) constraint is much more expressive and hence it is easier to define problems with the help of PB constraints. But while PB constraints provide us with a high-level problem description, it has been shown that solving PB constraints can be done faster with the help of a SAT solver. To apply such a solver to a PB constraint we have to encode it with clauses into conjunctive normal form (CNF). While we can find a basic encoding into CNF which is equivalent to a given PB constraint, the solving time of a SAT solver significantly depends on different properties of an encoding, e.g. the number of clauses or if generalized arc consistency (GAC) is maintained during the search for a solution. There are various PB encodings that try to optimize or balance these properties. This thesis is about such encodings. For a better understanding of the research field an overview about the state-of-the art encodings is given. The focus of the overview is a simple but complete description of each encoding, such that any reader could use, implement and extent them in his own work. In addition two novel encodings are presented: The Sequential Weight Counter (SWC) encoding and the Binary Merger Encoding. While the SWC encoding provides a very simple structure – it is listed in four lines – empirical evaluation showed its practical usefulness in various applications. The Binary Merger encoding reduces the number of clauses a PB encoding needs while having the important GAC property. To the best of our knowledge currently no other encoding has a lower upper bound for the number of clauses produced by a PB encoding with this property. This is an important improvement of the state-of-the art, since both GAC and a low number of clauses are vital for an improved solving time of the SAT solver. The thesis also contributes to the development of new applications for PB constraint encodings. The programming library PBLib provides researchers with an open source implementation of almost all PB encodings – including the encodings for the special cases at-most-one and cardinality constraints. The PBLib is also the foundation of the presented weighted MaxSAT solver optimax, the PBO solver pbsolver and the WBO, PBO and weighted MaxSAT solver npSolver.

Self-efficacy is a person's own perception about performing a task with a certain level of proficiency (Bandura, 1986). An important affective aspect of learning chemistry is chemistry self-efficacy (CSE). Several researchers have found chemistry self-efficacy to be a fair predictor of achievement in chemistry. This study was done in a college preparatory chemistry class for science majors exploring chemistry self-efficacy and its change as it relates to achievement. A subscale of CAEQ, Chemistry Attitudes and Experiences Questionnaire (developed by Dalgety et al, 2003) as well as student interviews were used to determine student chemistry self-efficacy as it changed during the course. The questionnaire was given to the students five times during the semester: in the first class and the class before each the four tests taken through the semester. Twenty-six students, both men and women, of the four major races/ethnicities were interviewed three times during the semester and events that triggered changes in CSE were followed through the interviews. HLM (hierarchical linear modeling) was used to model the results of the CSE surveys. Among the findings, women who started at significantly lower CSE than men accomplished a significant gain by the end of the semester. Blacks' CSE trends through the semester were found to be significantly different from the rest of the ethnicities.

The aim of this project is to study the viscous Burgers' equation for the case where the viscosity is constant, but also when it contains a jump in viscosity. In the first case where the viscosity is constant, Burgers' is simply solved on a singular domain. For the case with jump in viscosity, Burgers' is solved on multiple domains with different viscosity. The different domains are then connected by applying inner boundary conditions at an interface in order to produce a singular solution. The inner boundary conditions are imposed using three different methods; simultaneous approximation term (SAT), projection and hybrid method, where the hybrid method is a combination of both the SAT and projection method. These methods are used in combination with a stable and high-order accurate summation by parts (SBP) finite difference approximation in MATLAB. The three methods are then compared to each other with respect to the least square error and the corresponding convergence rate to determine which method is the most preferable to use. The methods resulting in the highest convergence rates are the projection and the hybrid methods. These methods manage to live up to the expected convergence rates for all operators with different orders of accuracy and are therefore both good methods to use. However, the best method to use is the projection method since it is much simpler to implement than the two other methods but still achieves just as good convergence rates as the hybrid method.

This study examines how large scale assessments like the Scholastic Aptitude Test (SAT), developed for students proficient in academic English, may not produce reliable and valid outcomes for academically vulnerable students, namely English Language Learners (ELLs). This mixed-methods study was conducted to uncover differences between the old and new mathematics sections of the SAT, to see if differences in mathematical performance correlate to language abilities by looking at students’ approach, and to explore teacher perceptions, attitudes, and pedagogical practice in the instruction of English learners. The study took place in a New Jersey school district. Seventy-eight students of varying language proficiencies were administered an old and new SAT-Mathematics (SAT-M) section. After scores were statistically analyzed, fifteen students were purposefully chosen to be interviewed. For a more comprehensive view of scores, students were asked to think out loud as they completed selected test items and answer questions pertaining to their background, problem-solving methodology, misconceptions, and limitations. Similarly, nine teachers were given a survey and the exams to pinpoint difficult questions, explain why students struggle, identify what English learners’ needs are, and describe how the needs are met. Qualitative data revealed that students’ performance was a reflection of mathematical and/or language challenges, or lack of exposure to certain mathematical concepts. Additionally, test structure and time constraints had confounding effects on student performance. Even though a variety of cognitive processes were observed, they seemed more aligned to a student’s academic track rather than linguistic abilities. With ELLs usually consigned to lower track mathematics classes, the interconnectedness of class, language, and expectations remains critical. Teachers’ responses reveal their pessimism in overcoming students’ language access barrier and low sense of mathematical efficacy. Teachers’ efforts to provide a more equitable education to ELLs reveal tensions between reform curriculum and equity. Findings of this study contribute to the discussion on factors that may lead to the marginalization of ELLs on national assessments. The results have important implications for test construction and challenges the conceptualization of what “language” is and what being “college and career” ready means.

We consider diagonal-norm classical summation-by-parts (SBP) operators us-ing the simultaneous approximation term (SAT) method of imposing boundaryconditions. We derive a formula for the inverse of these SBP-SAT discretizationmatrices. This formula is then used to show that it is possible to construct a secondorder accurate SBP-SAT operator using only seven grid points.

There has been serious concerns about the pace at which juvenile criminality isincreasing globally(National Academies Press, 2001).Young people are increasinglybecoming susceptible to a wide variety of misdemeanors; from substance abuse and addictionto murder (ibid). Studies have empirically described many triggers as the root cause ofjuvenile delinquency (Archer, 2000).Some criminologists have attributed these types ofmisdemeanors to the environments to which these adolescents are/have been subjected to(Wikstrom, 2004). On this basis, this research aims to assess the liability, if any, ofbystanders/observers and enablers/facilitators of juvenile delinquency. The study employed aqualitative approach in evaluating the role of bystanders and enablers in juveniledelinquency. The outcome revealed that the majority of bystanders and enablers are equallyas guilty as the delinquent youth. Three theories were used to rationalize these findings; theanomie-strain theory, situational action theory and self control theory ( Chainey & Ratcliffe,2005). As a result, the study recommends adequate parental guidance, in-person supervision,parental awareness, governmental inclusion, the provision of social infrastructures as well asequal opportunities, among others.

No description available.

Low frequency acoustic room behaviour can be approximated using numerical methods. Traditionally, music studio control rooms are built with complex geometries, making their eigenmodes difficult to predict mathematically. Hence, a summation-by-parts method with simultaneous-approximation-terms is derived to approximate the time dependent acoustic wave equation in three dimensions. The derived model is limited to rectangular prismatic rooms but planned to be expanded to handle complex geometries in the future. Semi-reflecting boundary conditions are used, corresponding to tabulated reflection and absorption properties of real. walls. Two speakers are modeled as omnidirectional point sources placed on a boundary, to mimic common studio setups. Through tests and examination of eigenvalues of the matrices in the method, conditions for stability and reflection coefficients are derived. Simulations of sound pressure distribution produced by the model correlate well to room mode theory, suggesting the model to be accurate in the application of predicting low frequency acoustic room behaviour. However, the convergence rate of the model turns out to be lower than expected when point sources are introduced. Future steps towards applying the model to real music studio control rooms include modeling the walls as changes in density and wave speed rather than boundaries of the domain. This would potentially allow more complex geometries to be modeled within a larger, rectangular domain.