111 |
Satisfiability and Optimization in Periodic Traffic Flow ProblemsGroßmann, Peter 25 October 2016 (has links)
Automatically calculating periodic timetables in public railway transport systems is an NP-complete problem – namely the Periodic Event Scheduling Problem (PESP). The original model is restricted to basic periodic timetabling. Extending the model by decisional transport networks with flows induces new possibilities in the timetabling and planning process. Subsequently, the given flexibility results in a generic model extension of PESP that can be applied in subsets of the timetabling process. The successful utilization of this approach is presented for distinct chain paths, duplicated chain paths and non-connected flow graphs that represent integration of routing and timetabling, planning of periodic rail freight train paths and track allocation, respectively. Furthermore, the encoding of this generic model into a binary propositional formula is introduced and the appropriate usage of several techniques like SAT solving and MaxSAT to calculate and optimize the corresponding instances will be presented accordingly. Computational results for real-world scenarios suggest the practical impact and give promising perspectives for further scientific research.
|
112 |
Booleovské techniky v reprezentaci znalostí / Boolean techniques in Knowledge representationChromý, Miloš January 2020 (has links)
Title: Boolean techniques in Knowledge representation Author: Miloš Chromý Department: Department of Theoretical Computer Science and Mathematical Logic Supervisor: Doc. RNDr. Ondřej Čepek, Ph.D., Department of Theoretical Com- puter Science and Mathematical Logic Abstract: In this thesis we will investigate switch-list representations of Boolean function and we will explore the biclique satisfiable formulas. Given a truth table representation of a Boolean function f the switch-list rep- resentation of f is a list of Boolean vectors from the truth table which have a different function value than the preceding Boolean vector in the truth table. We include this type of representation in the Knowledge Compilation Map [Dar- wiche and Marquis, 2002] and argue that switch-lists may in certain situations constitute a reasonable choice for a target language in knowledge compilation. First, we compare switch-list representations with a number of standard repre- sentations (such as CNF, DNF, and OBDD) with respect to their relative suc- cinctness. As a by-product of this analysis we also give a short proof of a long standing open question from [Darwiche and Marquis, 2002], namely the incom- parability of MODS (models) and PI (prime implicates) representations. Next, using the succinctness result between...
|
113 |
Logic Encryption of Sequential CircuitsThulasi Raman, Sudheer Ram 01 August 2019 (has links)
No description available.
|
114 |
[en] COMPLIANCE REASONING ON LEGAL NORMS: A LOGIC-BASED APPROACH / [pt] RACIOCÍNIO DE COMPLIANCE SOBRE NORMAS LEGAIS: UMA ABORDAGEM BASEADA EM LÓGICAFERNANDO ANTONIO DANTAS GOMES PINTO 02 July 2024 (has links)
[pt] Garantir que uma base de conhecimento com atos da administração
pública contenha apenas fatos em conformidade com sua legislação torna-se
um desafio para qualquer gestor público. Para isso, dado o grande volume
de dados gerados por empresas públicas, faz-se necessário o emprego de
recursos tecnológicos que auxiliem o processo de análise de conformidade
destes atos. Este trabalho apresenta uma arquitetura computacional capaz de
extrair informações publicados dos diários oficiais e então serializá-los em duas
bases de conhecimento: triplas RDF/XML de fatos e triplas de RDF/XML de
regras formalizadas em lógica iALC, uma lógica de descrição intuicionista.
Para garantir a consistência desta base de conhecimento, foi desenvolvido
um SAT Solver para iALC em forma de tableau semântico intuicionista.
Uma extensão do tableau intuicionista de primeira ordem apresentado por
Fitting (1969). Este SAT Solver faz parte de um módulo que além de gerar
modelos e contra-exemplos para as regras formalizadas em iALC, também
gera um código preliminar de consultas em SPARQL. Esta abordagem permite
inferir e certificar a qualidade dos dados disponíveis na base de conhecimento
RDF/XML de fatos. Para garantir a qualidade do nosso SAT Solver, fizemos
a prova de soundness das suas regras. Para garantir a qualidade da nossa
abordagem lógica, construímos um conjunto de 21 Questões de Competência e
aplicamos à nossa ferramenta. Os resultados deste estudo de caso mostraram
a eficácia e eficiência da nossa abordagem. / [en] Ensuring that a knowledge base with public administration acts contains
only facts in accordance with its legislation becomes a challenge for any
public manager. To achieve this, given the large volume of data generated by
public companies, it is necessary to apply technological resources that assist
in the process of analyzing the compliance of these acts. This work presents
a computational architecture capable of extracting information published in
official gazettes and then serializing it into two knowledge bases, RDF/XML
triples of facts and RDF/XML triples of rules formalized in iALC logic, an
intuitionistic description logic. To ensure the consistency of this knowledge
base, a SAT Solver for iALC was developed in the form of an intuitionistic
semantic tableau. An extension of the first-order intuitionist tableau presented
by Fitting (1960). This SAT Solver is part of a module that generates models
and counter-examples for rules formalized in iALC and generates a preliminary
query code in SPARQL. This approach allows infer and certify the quality of
the data available in the RDF/XML knowledge base of facts. To guarantee the
quality of our SAT Solver, we carry out the soundness proof of its rules. To
ensure the quality of our logical approach, we built a set of 21 Competency
Questions and applied our tool. The results of this case study showed our
approach s effectiveness and efficiency.
|
115 |
Comparison of the shock arrival times for Earth-directed ICMEs provided by the WSA-Enlil+Cone model and in-situ observations at L1: A Case StudyWerner, Anita Linnéa Elisabeth January 2016 (has links)
A case study which examines the agreement between prediction and data is performed for three, complex interplanetary shocks which were detected at the Sun-Earth Lagrange point L1 and induced moderate to intense geomagnetic storms. We use model output from previous runs of the coupled coronal-heliosphere WSA-Enlil+Cone model, available through the Community Coordinated Modeling Center (CCMC), and in-situ data from the OMNI data set. Code written in MATLAB is used to compare the model output with the in-situ measurements of the interplanetary magnetic field as well as the density, speed and temperature of the solar wind. In addition, the difference between the predicted and actual shock arrival time is computed and regions of potential temperature depression are identified. A considerable discrepancy is found between data and model for the studied events. The main reason is deemed to be an inadequate representation of the ambient solar wind as well as the complex interactions between interplanetary coronal mass ejections and corotating interaction regions. We suggest future steps to be taken for the further development of the model as well as for the general understanding of space weather and the Sun-Earth connection. / Denna fallstudie undersöker överensstämmelsen mellan modell och data för tre interplanetära chockvågor, som kunde detekteras vid jordens Lagrangepunkt 1, och som orsakade geomagnetiska stormar av måttlig till kraftig styrka. Vi använder oss av tidigare genomförda körningar av den sammansatta WSA-Enlil+Cone modellen, som avbildar fortplantningen av temporära störningar med ursprung i solens korona, såsom koronamassutkastningar, ut i heliosfären. Modellen gjordes tillgänglig av Community Coordinated Modeling Center (CCMC) och datan inhämtades från OMNI. Kod skriven i MATLAB nyttjades för att göra en jämförelse mellan modell och faktiska mätningar av det interplanetära magnetfältet samt solvindens hastighet, densitet och temperatur. Utöver detta, beräknas också skillnaden mellan förväntad och faktisk ankomsttid av respektive interplanetär chock, och tidsperioder med en temperatursänkning utöver det normala identifieras. Vi finner en omfattande avvikelse mellan modell och data, i synnerhet för de fall där på varandra följande koronamassutkastningar förväntas interagera eller rent av slås ihop samt för uppskattningen av den omgivande solvindens egenskaper och det interplanetära fältet under pågående geomagnetisk störning. Interaktionen mellan koronamassutkastningar och närliggande ko-roterande interaktionsregioner har ej heller återskapats väl av modellen ifråga. Slutligen ger vi förslag på möjliga, framtida åtgärder som kan bör tas i åtanke vid konstruerandet av framtida versioner av nämnda modell, liksom för den allmänna förståelsen för rymdvädrets inverkan på Jorden.
|
116 |
Temporal logic encodings for SAT-based bounded model checkingSheridan, Daniel January 2006 (has links)
Since its introduction in 1999, bounded model checking (BMC) has quickly become a serious and indispensable tool for the formal verification of hardware designs and, more recently, software. By leveraging propositional satisfiability (SAT) solvers, BMC overcomes some of the shortcomings of more conventional model checking methods. In model checking we automatically verify whether a state transition system (STS) describing a design has some property, commonly expressed in linear temporal logic (LTL). BMC is the restriction to only checking the looping and non-looping runs of the system that have bounded descriptions. The conventional BMC approach is to translate the STS runs and LTL formulae into propositional logic and then conjunctive normal form (CNF). This CNF expression is then checked by a SAT solver. In this thesis we study the effect on the performance of BMC of changing the translation to propositional logic. One novelty is to use a normal form for LTL which originates in resolution theorem provers. We introduce the normal form conversion early on in the encoding process and examine the simplifications that it brings to the generation of propositional logic. We further enhance the encoding by specialising the normal form to take advantage of the types of runs peculiar to BMC. We also improve the conversion from propositional logic to CNF. We investigate the behaviour of the new encodings by a series of detailed experimental comparisons using both hand-crafted and industrial benchmarks from a variety of sources. These reveal that the new normal form based encodings can reduce the solving time by a half in most cases, and up to an order of magnitude in some cases, the size of the improvement corresponding to the complexity of the LTL expression. We also compare our method to the popular automata-based methods for model checking and BMC.
|
117 |
A Study of the Effect of School-Sponsored, Extra-Curricular Activities on High School Students' Cumulative Grade Point Average, SAT Score, ACT Score, and Core Curriculum Grade Point AverageMiranda, Janet Young 08 1900 (has links)
This study investigated the effect of school-sponsored, extra-curricular activities on academic achievement for students at a private school in north central Texas. Students selected for this study were graduates from the classes of 1996, 1997, 1998, 1999, and 2000. With a minimum participation of two years during grades nine through twelve, students were categorized into subgroups of activities. After eliminating students who participated in more than one of the extra-curricular activities of music, drama, visual arts, and athletics, three hundred sixty-one students were represented. The identity of students was encoded and information was recorded for gender, school-sponsored, extra- curricular activities, cumulative grade point averages, SAT Scores, ACT Scores, and cumulative grade point averages in core curriculum subjects. A two-way ANOVA test with a two-by-five factorial design was completed for research questions one through four. A one-way ANOVA with a one-by-five factorial design was completed for research question five. When a significant F was found, Scheffe and LSD post hoc tests were completed to determine pair wise interaction. Statistical differences did exist when comparing school-sponsored, extra-curricular activities and cumulative grade point averages with musicians having a significantly higher cumulative grade point average, SAT scores, and ACT scores than athletes. A significant difference was found among the activity subgroups regarding the cumulative grade point averages in the core curriculum subjects of foreign language, history/English (an interdisciplinary subject at the studied school), mathematics, and science with musicians scoring significantly higher than athletes in all subjects. It is recommended that further studies be conducted to investigate the impact of activities on student achievement. Studies might include larger and different populations, the impact of participation at a younger age, and the impact of other activities on student achievement.
|
118 |
The INDEPENDENT SET Decision Problem is NP-completeBristow, Andrew, IV 18 August 2011 (has links)
In the 1970's computer scientists developed the theory of computational complexity. Some problems seemed hard-to-compute, while others were easy. It turned out that many of the hard problems were equally hard in a way that could be precisely specified. They became known as the NP-complete problems. The SATISFIABILITY problem (SAT) was the first problem to be proved NP-complete in 1971. Since then numerous other hard-to-solve problems have been proved to be in NP-complete. In this paper we will examine the problem of how to find a maximum independent set of vertices for a graph. This problem is known as Maximum Independent Set (MIS) for a graph. The corresponding decision problem for MIS is the question, given an integer K, is there a independent set with at least K vertices? This decision problem is INDEPENDENT SET (IS). The intention of this paper is to show through polynomial transformation that IS is in the set of NP-complete Problems. We intend to show that 3SAT is NP-complete and then using this fact, that IS is NP-complete.
|
119 |
Bridging the Gap: Why Many High School Writers Are Not Successful In College Composition ClassesPark, Amy Stutzman 01 January 2006 (has links)
It may be useful to identify this so-called gap that seems to plague first-year college writers before attempting to discover why it exists. In order to identify the gap, I want to define these writers who are leaving high school and finding difficulty in college composition classes. Patricia Bizzell defines basic writers as "those who are least well prepared for college" (Bizzell "What Happens When Basic Writers Come to College?" 294). I'd like to broaden her definition of basic writers and use the term "inexperienced writers" as the field now defines them. In order to fully understand why most college freshman writers are not successful, I will outline the type of thinking and reasoning that students are expected to display when they get to college, and thus the new world view Bizzell discusses in her article. Since Piaget's theory takes us only through the formal operational stage that he claims children may reach when they are 11 or 12 years old, I had to turn to two studies that detail the thinking strategies of late adolescents and adults. William Perry conducted a study in the 1950's and 1960's on the intellectual and ethical development of college students through a series of interviews with undergraduate men. He outlines three world views, or cognitive and ethical developmental stages through which undergraduates pass during their postsecondary education: Dualism, Relativism, and Commitment in Relativism. Perry's model details how students, as they move through the levels, make sense of the information, opinions, and theories confronting them in a college classroom (Perry 57-134). I use William Perry's concept of cultural exploration as Patricia Bizzell interprets it through her article ["What Happens When Basic Writers Come to College?"] to explore the demands of college composition classes. I am using Bizzell's interpretation because she outlines how Perry's model meshes with writing instruction, and writing is the central focus of my thesis. I examine how students are asked to think and relate to their own culture in both two and four-year institutions using Perry's world view stages not so much as a strict guideline, but as a framework for student cognitive development. After determining how the writing curriculum of three different Virginia post-secondary institutions -- Virginia Commonwealth University, University of Richmond, and J. Sargeant Reynolds Community College -- engage with Perry's scheme, I use the model to interpret how two major writing assessments, the Virginia Standard of Learning (SOL) and the SAT essay, coincide with post-secondary philosophy. Finally, I examine how an international curriculum, the International Baccalaureate (IB), corresponds with Perry's scheme and affects writing instruction at the high school level. By analyzing these secondary assessments and curricular program, I move closer to answering why the gap continues to exist.
|
120 |
\"Um resolvedor SAT paralelo com BSP sobre uma grade\" / \"Um resolvedor SAT paralelo com BSP sobre uma grade\"Lima, Fernando Correa 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
|
Page generated in 0.0148 seconds