Spelling suggestions: "subject:"tat"" "subject:"stat""
151 |
Etude de systèmes de contraintes pour le raisonnement qualitatif temporel et spatial / Study of constraint systems for qualitative reasoningAlmeida, Dominique D' 03 December 2010 (has links)
La modélisation et la résolution de problèmes sous contraintes constituent un domaine majeur enIA. Par la nature diverse des contraintes, différents formalismes de représentation ont été proposés pour les exprimer de manière simple et compacte tout en garantissant une efficacité des outils de résolutions associés. Les formules propositionnelles, les réseaux de contraintes discrets (RCD) et qualitatives (RCQ) sont des cadres de modélisation répondant à ces critères. Pour les informations temporelles ou spatiales, les RCQ constituent un modèle de choix avec de nombreuses applications comme l’ordonnancement de tâches, la planification temporelle ou spatiale, les systèmes d’informations géographiques. Nos contributions visent à étudier les liens des RCQ vers les RCD et les formules propositionnelles, afin d’adapter les outils issus des divers domaines et de proposer de nouvelles approches. Tout d’abord, nous nous concentrons sur l’aspect structurel des RCQ, en adaptant la méthode de la composition faible dans les différents cadres. Nous exploitons ensuite les propriétés des classes traitables de certains formalismes qualitatifs, afin de définir une transformation vers la logique propositionnelle. En exploitant la transformation vers les RCD, nous proposons une méthode incomplète facilitant la preuve de l’incohérence des RCQ par la relaxation de la propriété de composition faible, puis nous complétons l’approche en exploitant les classes traitables. Enfin, ces études nous conduisent à proposer une nouvelle forme de substituabilité locale, dont les détections statique et dynamique permettent d’obtenir une amélioration algorithmique dans le cadre des RCD. / Modelling and solving constraints problems is a major domain in Artificial Intelligence. By the various natures of the constraints, different formalisms were proposed to express them in a simple andcompact way while guaranteeing the effectiveness of the associated solution tools. Propositional formulae, discrete constraint networks (DCNs), and qualitative constraint networks (QCNs) are the well known frameworks that guaranty these requirements. For temporal or space information, QCNs constitute a model of choice with many real world applications such as scheduling, temporal or spatial planning and geographic information systems. Our contributions aim at studying the links between QCNs, DCNs and propositional formulas, in order to adapt the tools developed in these fields and to propose new approaches. First of all, we focus on the structural aspects of QCNs, by transforming weak composition within the various frameworks. In order to define a transformation towards propositional logic we then exploit the properties of tractable classes of some qualitative formalism. Exploiting the transformation towards DCNs, we propose an incomplete method simplifying the proof of the inconsistency for QCNs by relaxing the weak composition property. Then, we propose a complete approach thanks to tractable classes. Finally, these studies lead us to propose a new form of local substitutability, whose static and dynamic detections significantly improve search algorithms for DCNs.
|
152 |
\"Um resolvedor SAT paralelo com BSP sobre uma grade\" / \"Um resolvedor SAT paralelo com BSP sobre uma grade\"Fernando Correa Lima 23 March 2007 (has links)
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
|
153 |
Effizientes Verifizieren co-NP-vollständiger Probleme am Beispiel zufälliger 4-SAT-Formeln und uniformer HypergraphenSchädlich, Frank 30 June 2004 (has links)
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.
|
154 |
Pseudo-Boolean Constraint Encodings for Conjunctive Normal Form and their ApplicationsSteinke, Peter 20 February 2020 (has links)
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.
|
155 |
Tracking Chemistry Self-Efficacy and Achievement in a Preparatory Chemistry CourseGarcia, Carmen Alicia 01 July 2010 (has links)
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.
|
156 |
Simulation of Viscosity-Stratified FlowCarlsson, Victor, Isaac, Philip, Adina, Persson January 2020 (has links)
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.
|
157 |
An Analysis of the Redesigned SAT-I Mathematics: Perceptions of Teachers, English Proficient Students, and English Language LearnersChen, Margaret January 2021 (has links)
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.
|
158 |
An exploration of classical SBP-SAT operators and their minimal sizeNilsson, Jesper January 2021 (has links)
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.
|
159 |
The Role of Bystanders and Enablers in Juvenile DelinquencyJaiyeola, Oluwatoyin January 2020 (has links)
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.
|
160 |
On Reverse Engineering of Encrypted High Level Synthesis DesignsJoshi, Manasi 02 November 2018 (has links)
No description available.
|
Page generated in 0.0385 seconds