Η παρούσα διπλωµατική εργασία ασχολείται με το θέμα των Αλγορίθμων Επίλυσης Προβληµάτων SAT. Η εργασία αυτή εκπονήθηκε στα πλαίσια του Εργαστηρίου Ενσύρµατης Επικοινωνίας του Τµήματος Ηλεκτρολόγων Μηχανικών και Τεχνολογίας Υπολογιστών της Πολυτεχνικής Σχολής του Πανεπιστηµίου Πατρών. Σκοπός της είναι η δημιουργία ενός Προσομοιωτή των αλγορίθμων αυτών, ο οποίος να μπορεί να προσπελαστεί από οποιονδήποτε μέσω του διαδικτύου. Αρχικά έγινε µία εισαγωγή στο αντικείμενο της Τεχνητής Νοημοσύνης και πιο συγκεκριµένα στην Προτασιακή Λογική, ενώ δόθηκε και το απαραίτητο υπόβαθρο για να κατανοηθεί το πρόβληµμα και οι τεχνικές λύσης του. Τέλος, επιλέχθηκε να γίνει η υλοποίηση του Προσωμοιωτή σε Java. / This diploma dissertation deals with SAT solvers, algorithms for the Boolean satisfiability problem. It was produced in the Wire Communications Laboratory of the Electrical and Computer Engineering Department of the University of Patras. Its aim is to create a simulator for these algorithms, accessible to anyone via the Internet. An introduction to the field of Artificial Intelligence and more specifically to Propositional Calculus was given as well as the necessary groundwork to understand the problem and its solution approaches. The simulation implementation was developed in Java

The thesis studies classes of Boolean formulae for which the well-known satisfiability problem is solvable in polynomially bounded time. It focusses on classes based on unit resolution; it describe classes of unit refutation complete formulae, unit propagation complete formulae and focuses on the class of SLUR formulae. It presents properties of SLUR formulae as well as the recently obtained results. The main result is the coNP-completness of membership testing. Finally, several hierarchies are built over the SLUR class and their properties and mutual relations are studied. Powered by TCPDF (www.tcpdf.org)

This dissertation shows that the bounded property verification of hardware Register Transfer Level (RTL) designs can be efficiently performed by precise abstract interpretation of a software representation of the RTL. The first part of this dissertation presents a novel framework for RTL verification using native software analyzers. To this end, we first present a translation of the hardware circuit expressed in Verilog RTL into the software in C called the software netlist. We then present the application of native software analyzers based on SAT/SMT-based decision procedures as well as abstraction-based techniques such as abstract interpretation for the formal verification of the software netlist design generated from the hardware RTL. In particular, we show that the path-based symbolic execution techniques, commonly used for automatic test case generation in system softwares, are also effective for proving bounded safety as well as detecting bugs in the software netlist designs. Furthermore, by means of experiments, we show that abstract interpretation techniques, commonly used for static program analysis, can also be used for bounded as well as unbounded safety property verification of the software netlist designs. However, the analysis using abstract interpretation shows high degree of imprecision on our benchmarks which is handled by manually guiding the analysis with various trace partitioning directives. The second part of this dissertation presents a new theoretical framework and a practical instantiation for automatically refining the precision of abstract interpretation using Conflict Driven Clause Learning (CDCL)-style analysis. The theoretical contribution is the abstract interpretation framework that generalizes CDCL to precise safety verification for automatic transformer refinement called Abstract Conflict Driven Learning for Safety (ACDLS). The practical contribution instantiates ACDLS over a template polyhedra abstract domain for bounded safety verification of the software netlist designs. We experimentally show that ACDLS is more efficient than a SAT-based analysis as well as sufficiently more precise than a commercial abstract interpreter.

The purpose of the project: The aim of this project was to finish the current BOM-list that already existed so it could be sent to X-ponent. When that was done it got possible to identify the non X-ponent products from other suppliers. These products had to be order by the needs to build walls, roof, and etc. When all the products were on place on the BOM-list the next goal was to send it back to X-ponent so they could buy them and then start to build different car-riages/boards by knowing who to call. The last step was to plan a delivery based on the most effective way by identify the risks. Make sure that the existing BOM-list is finished with the most suitable tools/ equip-ment’s and how to strategically buy them from X-ponent. How can X-ponent buy the non X-ponent products effective from the suppliers? How will these assembled products arrive effective from X-ponent to Husmutterns facil-ity?  How will these products be financed?Sum: A plan for the purchaser on Husmuttern AB so he/she just have to call X-ponent only once and to tell them a thought date for the products to be on place.Method: To achieve with these tasks, the author had to do a literature study on lean and six sigma tools. The comparison that was done between Husmuttern AB and XX gave a clear im-age about how respective companies purchasing process are. When these studies were done it became easier to handle these tasks, sush as fill in the rest on the BOM-list, knowing how transport the goods effective and also know what to take up on the attended meetings with the suppliers and to communicate through email and phone.Study results: The result for this project was to fill the required equipment’s/tools for the company that is thought to be purchased, considering the best products for these types of car-riage/boards. When all the tools/equipment’s were covered and finished the result was how to strategically buy them from this supplier (X-ponent). The author had to find the best logistics company to deliver these products and therefore was the delivery time estimated and founded based on Google maps estimated time to travel from Phils to X-ponent and then to Husmuttern AB:s facility. To transport the goods from X-ponents facility to the truck was estimated based on earlier experience out of the seller on X-ponent and CEO on husmuttern. The total price for each product from X-ponent:The exact price exkl moms:1 Instruction carriage/board: XXkr2 Tool/equipment carriages/boards: XXkr1 Charging carriage/boards: XXkr1 Unloading carriage: XXkr1 Unrolling stand: XXkr16 Pallet carriages: XXkrThe estimated price for the fixtures:1 Roof fixture: XXkr1 Wall fixture: XXkr1 Inner wall/inner roof fixture: XXkr1 Floor fixture: XXkr1 Corner fixture: XXkrThe estimated delivery price for the total transport: XXkrA total estimated price for the whole process: XXkr excl VATRecommendations: When the facility is on place and is producing the houses, it is important that the staff on the company evaluate the products that was bought, so if they know if any changes will be done or not. This will also help them to save money so they do not have to buy same tools/equipment over and over again. If you see it from another perspective, it will make4 (67)it possible for Husmuttern to tell X-ponent that the products they bought is not good as they thought and that will help X-ponent to fix the coming problems, and maybe make a discount to other Husmuttern facilities that probably be established in the coming future.It is also very im-portant that the company always looks what the market has to tell, and be very aware what the costumers needs in the coming future.

Made available in DSpace on 2015-03-13T17:08:23Z (GMT). No. of bitstreams: 1 PatriciaRAO.pdf: 5281930 bytes, checksum: 67be620244094cfb2196749d05935973 (MD5) Previous issue date: 2009-05-13 / Conselho Nacional de Desenvolvimento Cient?fico e Tecnol?gico / The study area is located on the Brazilian Continental Shelf adjacent to Cear? State, inserted in the submerged Potiguar Basin. This area was submitted to extensional efforts during Upper Cretaceous, associated to the begining of the rifting that resulted in African and South American Continent separation. The main goal of this research was to better understand the sedimentary and geomorphological characteristics of the continental shelf adjacent to Fortim, Aracati and Icapu? (Cear? State). The used data base included geophysical (sides scan sonar and bathymetry studies) and sedimentological survey, associated to satellite image processing and interpretation. Inferences about suspended material and longshore drift was possible using satellite images, and differente bedforms were characterized such as: different kinds of dunes (longitudinal, cross and oblique), bioclastic banks, paleochannels, flat and rock bottom. The researched area comprehended about 2509,13 km2, where 6 different sedimentary facies, based on sediment composition and texture, could be recognized, such as: Bioclastic Sand, Siliciclastic Sand, Biosiliciclastic Sand, Bioclastic gravel, Biosiliciclastic sand with granule and gravel, and Silicibioclastic sand with granule and gravel. The integration of bathymetric, satellite image, side scan sonar and sedimentological data allow us a better characterization of this continental shelf area, as to advance in the knowledge of the continental shelf of the state of Ceara, a very important area to the oil industry because of its potential exploration and e exploitation, and to environmental survey as well / A ?rea em estudo compreende a Plataforma Continental Cearense inserida no contexto tect?nico e sedimentar da Bacia Potiguar, por??o submersa. Regi?o formada por esfor?os extensionais durante o Cret?ceo Inferior, associados ao in?cio do rifteamento que resultaria na separa??o das placas sul-americana e africana. Objetivando contribuir para um maior conhecimento das caracter?sticas sedimentol?gicas e geomorfol?gicas da plataforma continental adjacente aos munic?pios de Fortim, Aracati e Icapu? (CE). Foram realizado coleta, interpreta??o e integra??o de dados do sonar de varredura lateral, imagem de sat?lite, batimetria e amostras de sedimentos superficiais. Infer?ncias quanto ao material em suspens?o e deriva litor?nea foram obtidas a partir do processsamento digital de imagens (PDI), enquanto a caracteriza??o das fei??es do fundo marinho, tais como: dunas longitudinais, dunas transversais e dunas obliquas, bancos de sedimentos biocl?sticos, paleocanais submersos, leito plano e fundo rochoso foram obtidas a partir da integra??o de dados batim?tricos sonogr?ficos e PDI. Quanto a sedimentologia, com base na composi??o e textura, foram identificados na ?rea em estudo 6 f?cies sedimentares, abrangendo uma ?rea total de 2509,13 Km2, sendo elas: Areias Biocl?sticas, Areia Silicicl?stica, Areias Biosilicicl?sticas, Areia Cascalhosa Biocl?stica, Areia Cascalhosa Biosilicicl?stica e Areias Cascalhosas Silicibiocl?sticas; al?m de rochas praiais (beachrocks) e fundo rochoso. A integra??o entre os dados batim?tricos, PDI, sonogr?ficos e sedimentol?gicos, mostrou-se apropriada para a caracteriza??o morfol?gica e sedimentol?gica da Plataforma Continental da ?rea em estudo, desta forma avan?ando no conhecimento da Plataforma Continental Cearense, regi?o de interesse para a ind?stria do petr?leo tanto no ponto de vista da explota??o e explora??o de hidrocarbonetos, como tamb?m ambiental

Made available in DSpace on 2014-12-17T15:14:52Z (GMT). No. of bitstreams: 1 CristianACA_TESE.pdf: 1637371 bytes, checksum: 286a3a156c7aca7fdba8233b49b7891f (MD5) Previous issue date: 2010-12-02 / A rota??o estelar ? um dos mais importantes observ?veis da evolu??o estelar. Neste sentido, o sat?lite CoRoT representa uma oportunidade ?nica de medir os per?odos rotacionais para uma amostra de estrelas estatisticamente robusta, oferecendo dados absolutamente necess?rios para o estudo da rota??o e seu papel na evolu??o estelar. Para conseguir isto, um passo fundamental ? a caracteriza??o f?sica e qu?mica das estrelas observadas pelo CoRoT, especificamente devido ao fato de que o c?lculo de per?odos rotacionais confi?veis ? um trabalho dif?cil sem a ajuda dos par?metros estelares. Desta forma, foi elaborado um importante seguimento observacional das estrelas nos campos do CoRoT do anticentro LRa01 e do centro LRc01, permitindo a correta identifica??o dos per?odos que reflitam a modula??o rotacional. Nesta tese de doutorado s?o apresentados os resultados de tal seguimento. Par?metros f?sicos e qu?micos, tais como temperatura efetiva Teff , gravidade superficial log(g), velocidade de microturbul?ncia Vmic, abund?ncia de ferro [Fe/H], velocidade de rota??o projetada Vsin(i), e abund?ncia de l?tio A(Li) s?o apresentados para uma amostra de 116 estrelas dos campos CoRoT. Elas se encontram em diferentes est?gios evolutivos, desde a sequ?ncia principal (SP) at? o ramo das gigantes vermelhas (GV). As observa??es foram feitas utilizando os espectr?grafos UVES (VLT) e HYDRA (CTIO). Para a deriva??o de tais par?metros foram utilizados o programa TurboSpectrum e os modelos de atmosfera de MARCS. Paralelamente, velocidades rotacionais Vsin(i) foram obtidas a partir do ajuste dos perfis observados e sint?ticos das linhas de ferro e por meio de uma calibra??o de fun??o de correla??o cruzada (CCF). Per?odos rotacionais Prot para 77 estrelas da amostra foram obtidos a partir das curvas de luz do sat?lite CoRoT. Extensas tabelas destes par?metros e seus respectivos erros s?o apresentadas. Foram encontradas diferen?as nas distribui??es de Teff , [Fe/H] e est?gios evolutivos entre os diferentes campos do CoRoT, indicando poss?veis efeitos de sele??o na amostra, assim como a exist?ncia de diferentes popula??es estelares do disco Gal?ctico. Por outro lado, o comportamento rotacional e as abund?ncias de l?tio n?o apresentam diferen?as entre estrelas de par?metros f?sicos similares, mas que pertencem a diferentes campos do CoRoT. A partir da an?lise de temperaturas, foi encontrada uma maior extin??o por avermelhamento para estrelas do CoRoT localizadas no campo LRc01, assim como um gradiente deste valor em fun??o da dist?ncia. Os resultados mostram que as abund?ncias de l?tio, as velocidades de rota??o e os per?odos rotacionais apresentam o mesmo comportamento descrito na literatura. Por outro lado, ? apresentada pela primeira vez a rela??o que existe entre o l?tio e o per?odo de rota??o em diferentes est?gios evolutivos, mostrando, tal como era esperado, que ambas as grandezas possuem uma anticorrela??o. Tamb?m ? apresentada a evolu??o simult?nea da rota??o e do l?tio, e foram calculadas rela??es que permitem obter valores m?dios de A(Li) como fun??o da temperatura efetiva e do per?odo rotacional. Os dados apresentados nesta tese de doutorado representam um importante ponto de partida para serem utilizados como uma amostra de calibra??o para diferentes programas no contexto da miss?o do sat?lite CoRoT, uma vez que a lista de estrelas aqui analisadas s?o parte das mais brilhantes que comp?em o campo Exo do CoRoT

The purposes of this study were to investigate the impact of the following factors on the decline of average SAT scores between 1952 and 1981: (1) changes in composition of population of the SAT takers after 1963, (2) aggregate technological and social changes related to the scores in the years following 1970, and (3) selected economic factors in the period 1952 through 1981. Two models were used to test the hypotheses of this study. The dependent variables of each model were the SAT Verbal and Math scores. The independent variables of the study were two intervention variables that represented changes following 1963 and after 1970. Also, three economic variables were subjected to principal component analysis. These were changes in unemployment, Consumer Price Index (CPI), and real Gross National Product (GNP). The results were two factors: (1) Economic Instability (combination of unemployment and CPI), and (2) Economic Growth. These two factors were used as independent variables in addition to the interventions of 1963 and 1970. The interaction of these variables were calculated. The Box-Jenkins technique was used to generate residuals which were white noise (free from the confounding of autoregression, moving average, and trend or stochastic drift). Finally, hierarchical multilinear regression technique was used to analyze the white noise data of the study.

Cette thèse porte sur la résolution séquentielle et parallèle du problème de la satisfiabilité propositionnelle(SAT). Ce problème important sur le plan théorique admet de nombreuses applications qui vont de la vérification formelle de matériels et de logiciels à la cryptographie en passant par la planification et la bioinformatique. Plusieurs contributions sont apportées dans cette thèse. La première concerne l’étude et l’intégration des concepts d’intensification et de diversification dans les solveurs SAT parallèle de type portfolio. Notre seconde contribution exploite l’état courant de la recherche partiellement décrit par les récentes polarités des littéraux « progress saving », pour ajuster et diriger dynamiquement les solveurs associés aux différentes unités de calcul. Dans la troisième contribution, nous proposons des améliorations de la stratégie de réduction de labase des clauses apprises. Deux nouveaux critères, permettant d’identifier les clauses pertinentes pour la suite de la recherche, ont été proposés. Ces critères sont utilisés ensuite comme paramètre supplémentaire de diversification dans les solveurs de type portfolio. Finalement, nous présentons une nouvelle approche de type diviser pour régner où la division s’effectue par ajout de contraintes particulières. / In this thesis, we deal with the sequential and parallel resolution of the problem SAT. Despite of its complexity, the resolution of SAT problem is an excellent and competitive approach for solving thecombinatorial problems such as the formal verification of hardware and software, the cryptography, theplanning and the bioinfomatics. Several contribution are made in this thesis. The first contribution aims to find the compromise of diversification and intensification in the solver of type portfolio. In our second contribution, we propose to dynamically adjust the configuration of a core in a portfolio parallel sat solver when it is determined that another core performs similar work. In the third contribution, we improve the strategy of reduction of the base of learnt clauses, we construct a portfolio strategy of reduction in parallel solver. Finally, we present a new approach named "Virtual Control" which is to distribute the additional constraints to each core in a parallel solver and verify their consistency during search.

Cette thèse présente différentes techniques permettant de résoudre le problème de satisfaction de formule booléenes utilisant le parallélisme et du calcul distribué. Dans le but de fournir une explication la plus complète possible, une présentation détaillée de l'algorithme CDCL est effectuée, suivi d'un état de l'art. De ce point de départ, deux pistes sont explorées. La première est une amélioration d'un algorithme de type portfolio, permettant d'échanger plus d'informations sans perte d'efficacité. La seconde est une bibliothèque de fonctions avec son interface de programmation permettant de créer facilement des solveurs SAT distribués. / This thesis presents different technique to solve the Boolean satisfiability problem using parallel and distributed architectures. In order to provide a complete explanation, a careful presentation of the CDCL algorithm is made, followed by the state of the art in this domain. Once presented, two propositions are made. The first one is an improvement on a portfolio algorithm, allowing to exchange more data without loosing efficiency. The second is a complete library with its API allowing to easily create distributed SAT solver.

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.