I [Mattson, Journal of Scientific Computing 51.3 (2012), s. 650–682] konstruerades partialsummeringsoperatorer för finita differensapproximationer av andraderivator med variabla koefficienter. Vi tillämpar framgångsrikt dessa operatorer på vågekvationen i två dimensioner med diskontinuerliga koefficienter, utan särskild behandling av diskontinuiteten. Närmare bestämt undersöks (i) operatorernas fel och konvergensordning relativt ”korrekt” hantering av diskontinuiteter genom blockuppdelning med kopplingstermer; (ii) ifall mycket komplicerade koefficienter orsakar instabilitet eller icke-fysikaliska fel. Vi visar att hoppet i våghastighet i simuleringen sker ett antal punkter ifrån hoppet i koefficienter, där antalet punkter beror på operatorernas ordning och storleken av hoppet i koefficienter. I (i) får dessa två faktorer plus blockets form och antalet punkter en stor påverkan på både storleken av felet, samt metodens konvergensordning som varierar från ca 1–2,5. Annars sker i både (i) och (ii) inget större icke-fysikaliskt fel eller instabilitet, vilket gör denna relativt enkla metod tillämpningsbar på komplexa verklighetsbaserade problem.

[pt] A teoria dos Jogos Combinatórios é o estudo de jogos com informação completa. Isso é, todos os jogadores conhecem todos os possíveis movimentos, além disso, temos que não há sorte ou a habilidade de realizar um movimento, então, em teoria jogar perfeitamente é possível. Exemplos de jogos assim são jogo da velha, xadrez, damas, Nim... a lista continua. Nessa dissertação focamos no jogo Maker-Breaker. Ele tem dois jogadores que sequencialmente escolhem um vértice de um hipergrafo. O objetivo de Maker é escolher todos os vértices de uma aresta e o objetivo de Breaker é prevenir isso. Para entender em quais tipos de hipergrafos Maker ou Breaker ganha e quais são as estratégias de vitória utilizamos SAT, probabilidade, teoria dos grafos em geral e mais. / [en] The theory of Combinatorial Games is the study of games with perfect information. This means that all players have knowledge of all possible moves, also there isn t luck or skill to perform a move, so, in theory perfect play is possible. Examples of games like these are tic-tac-toe, chess, checkers, Nim... the list goes on. In this dissertation we focus on the Maker-Breaker game. It has two players that pick a vertex from a hypergraph. The goal of Maker is to claim all vertices of an edge and the goal of Breaker is to prevent it. To understand in which types of hypergraphs does Maker or Breaker win and what are the winning strategies, we make use of SAT, Probability, general Graph Theory and more.

No description available.

Quoique très difficile à résoudre, le problème de satisfiabilité Booléenne (SAT) est fréquemment utilisé lors de la modélisation d’applications industrielles. À cet effet, les deux dernières décennies ont vu une progression fulgurante des outils conçus pour trouver des solutions à ce problème NP-complet. Deux grandes avenues générales ont été explorées afin de produire ces outils, notamment l’approche logicielle et matérielle. Afin de raffiner et améliorer ces solveurs, de nombreuses techniques et heuristiques ont été proposées par la communauté de recherche. Le but final de ces outils a été de résoudre des problèmes de taille industrielle, ce qui a été plus ou moins accompli par les solveurs de nature logicielle. Initialement, le but de l’utilisation du matériel reconfigurable a été de produire des solveurs pouvant trouver des solutions plus rapidement que leurs homologues logiciels. Cependant, le niveau de sophistication de ces derniers a augmenté de telle manière qu’ils restent le meilleur choix pour résoudre SAT. Toutefois, les solveurs modernes logiciels n’arrivent toujours pas a trouver des solutions de manière efficace à certaines instances SAT. Le but principal de ce mémoire est d’explorer la résolution du problème SAT dans le contexte du matériel reconfigurable en vue de caractériser les ingrédients nécessaires d’un solveur SAT efficace qui puise sa puissance de calcul dans le parallélisme conféré par une plateforme FPGA. Le prototype parallèle implémenté dans ce travail est capable de se mesurer, en termes de vitesse d’exécution à d’autres solveurs (matériels et logiciels), et ce sans utiliser aucune heuristique. Nous montrons donc que notre approche matérielle présente une option prometteuse vers la résolution d’instances industrielles larges qui sont difficilement abordées par une approche logicielle. / Though very difficult to solve, the Boolean satisfiability problem (SAT) is extensively used to model various real-world applications and problems. Over the past two decades, researchers have tried to provide tools that are used, to a certain degree, to find solutions to the Boolean satisfiability problem. The nature of these tools is broadly divided in software and reconfigurable hardware solvers. In addition, the main algorithms used to solve this problem have also been complemented with heuristics of various levels of sophistication to help overcome some of the NP-hardness of the problem. The end goal of these tools has been to provide solutions to industrial-sized problems of enormous size. Initially, reconfigurable hardware tools provided a promising avenue to accelerating SAT solving over traditional software based solutions. However, the level of sophistication of software solvers overcame their hardware counterparts, which remained limited to smaller problem instances. Even so, modern state-of-the-art software solvers still fail unpredictably on some instances. The main focus of this thesis is to explore solving SAT on reconfigurable hardware in order to gain an understanding of what would be essential ingredients to add (and discard) to a very efficient hardware SAT solver that obtains its processing power from the raw parallelism of an FPGA platform. The parallel prototype solver that was implemented in this work has been found to be comparable with other hardware and software solvers in terms of execution speed even though no heuristics or other helping techniques were implemented. We thus show that our approach provides a very promising avenue to solving large, industrial SAT instances that might be difficult to handle by software solvers.

Nous avons étudié dans cette thèse une approche discrète de la synthèse de contrôleurs pour les systèmes hybrides permettant la manipulation de dynamiques non-linéaires : les états sont regroupés dans une partition finie au prix d'une sur-approximation non déterministe de la relation de transition. Nous avons développé des algorithmes permettant de réduire l'explosion du nombre d'états due à la discrétisation en exploitant des propriétés des systèmes ODE. Ces algorithmes sont basés sur une approche hiérarchique du problème de la synthèse en le résolvant pour des sous problèmes et en utilisant ces résultats pour réduire l'espace d'états global. Nous avons aussi combiné des objectifs de vivacité et de sécurité pour s'approcher d'une stabilisation. Des résultats implémentés sur un prototype viennent montrer l'intérêt de cette approche.Pour la vérification, nous avons étudié le problème du model checking d'automates temporisés basé sur la résolution SAT. Nous avons exploré des solutions alternatives pour le codage des réductions SAT basées sur des exécutions parallèles de transitions indépendantes. Alors qu'une telle optimisation a déjà été étudiée pour les systèmes discrets, une approche intuitive pour les automates temporisés serait de considérer que des transitions en parallèle ont lieu au même instant (synchrones). Toutefois il est possible de relâcher cette condition et nous avons montré trois sémantiques différentes pour les séquences temporisées avec des transitions parallèles. Nous montrons la correction des sémantiques et décrivons des résultats expérimentaux réalisés avec notre prototype. / We consider a discretization based approach to controller synthesis of hybrid systems that allows to handle non-linear dynamics. In such an approach, states are grouped together in a finite index partition at the price of a non-deterministic over approximation of the transition relation. The main contribution of this work is a technique to reduce the state explosion generated by the discretization: exploiting structural properties of ODE systems, we propose a hierarchical approach to the synthesis problem by solving it first for sub problems and using the results for state space reduction in the full problem. A secondary contribution concerns combined safety and liveness control objectives that approximate stabilization. Results implemented on a prototype show the benefit of this approach. For the verification, we study the model checking problem of timed automata based on SAT solving. Our work investigates alternative possibilities for coding the SAT reductions that are based on parallel executions of independent transitions. While such an optimization has been studied for discrete systems, its transposition to timed automata poses the question of what it means for timed transitions to be executed “in parallel”. The most obvious interpretation is that the transitions in parallel take place at the same time (synchronously). However, it is possible to relax this condition. On the whole, we define and analyse three different semantics of timed sequences with parallel transitions. We prove the correctness of the proposed semantics and report experimental results with a prototype implementation.

As serino-proteases autotransportadoras de Enterobacteriaceae (SPATE) constituem uma família de proteases secretadas pelo sistema de secreção do tipo V, cujos genes foram estudados em Escherichia coli intestinal e extra-intestinal. Sat é uma SPATE citotóxica de 107 kDa, cujo gene foi identificado pela primeira vez em UPEC isolada da urina de um paciente com pielonefrite. A maioria dos estudos envolvendo Sat foram realizados em células renais e da bexiga, embora seu gene seja encontrado em DAEC, EAEC e, mais recentemente, em amostras bacterianas isoladas de septicemia neonatal e meningite. Os objetivos deste trabalho foram: i) purificar Sat; ii) determinar a ação da Sat purificada em diferentes tipos celulares e iii) caracterizar o papel de Sat na infecção in vitro por EAEC. Desta foram, a presença de Sat nos sobrenadantes do cultivo das cepas EAEC CV323 e DEC/Sat, isoladas de diarreia, foi confirmada por LC-MS/MS. Sat foi purificada da cultura de DEC/Sat+ e utilizada para a obtenção de anticorpos anti-Sat em coelho. O efeito citotóxico de Sat purificada foi investigado em células derivadas do endotélio (HUVEC) e do sistema urinário (Y1, LLC-PK1 e HEK-293) e gastrointestinal (Caco-2). Os parâmetros citotóxicos analisados foram: o descolamento celular e alterações na morfologia, permeabilidade e metabolismo mitocondrial das células. Para investigar o papel de Sat na infecção por EAEC, células Y-1 foram infectadas com EAEC CV323 e DEC/Sat+ na presença ou ausência de PMSF (inibidor de serino-protease) e anticorpos anti-Sat. Os parâmetros de citotoxicidade analisados nas culturas infectadas foram descolamento celular e alteração na morfologia. Os resultados demonstraram que: i) Sat é secretada por EAEC CV323 e DEC/Sat+ e, em ambas as cepas, há duas mutações em resíduos de aminoácidos que não interferiram na atividade enzimática; ii) as células do endotélio são mais sensíveis à Sat do que as células derivadas do trato urinário, sendo a linhagem gastrointestinal a mais resistente; iii) Sat secretada por EAEC CV323 durante a infecção induziu intenso dano celular, o qual, em presença de anticorpos anti-Sat e PMSF foi reduzido em cerca de 80 a 90%, respectivamente. Este é o primeiro trabalho que demonstra a expressão de Sat pela EAEC e a ação da toxina em células endoteliais sugerindo que o papel de Sat possa ser mais amplo na patogenia do que o proposto até o momento. / The serine protease autotransporters of Enterobacteriaceae (SPATEs) constitute a family of proteases secreted by the type V secretion system whose genes have been studied in intestinal and extra intestinal Escherichia coli. Sat is a 107 kDa cytotoxic SPATE and its gene was first identified in UPEC isolated from the urine of a patient with pyelonephritis. Most studies involving Sat were performed in renal and bladder cells, although the gene encoding Sat is encountered in other strains of E. coli such as DAEC, EAEC and more recently, in bacterial samples isolated from neonatal septicemia and meningitis. The objectives of this work were: i) purify Sat; ii) to determine the action of Sat in different types of cells and iii) to characterize in vitro the role of Sat in EAEC infection. Accordingly, the presence of Sat in the culture supernatant of EAEC CV323 and DEC/Sat+ derived from diarrhea was confirmed by LCMS/MS. Sat was purified from the culture of DEC/Sat+ and utilized to produce rabbit antibodies anti-Sat. The cytotoxic effect of Sat was investigated in cells derived from the endothelium (HUVEC) and the urinary (Y1, LLC-PK1, HEK-293) and gastrointestinal (Caco-2) systems. The cytotoxic parameters analyzed were cellular detachment and alterations in the morphology, permeability and mitochondrial metabolism of the cells. To investigate the role of Sat in EAEC infection, Y-1 cells were incubated with EAEC CV323 and DEC/Sat+ in the presence or absence of PMSF (a serine protease inhibitor) and rabbit antibodies anti-Sat. The parameters analyzed were cellular detachment and alteration in the morphology of the cells. The results demonstrated that: i) Sat is secreted by EAEC CV323 and DEC/Sat + and in both strains there are two mutations in amino acid residues that did not interfere with enzymatic activity; ii) endothelium cells are more sensitive to the Sat effect than the cells derived from urinary tract system, being the gastrointestinal cell lineage the most resistant one; iii) Sat secreted by EAEC CV323 during infection induced intense cellular damage which in the presence of anti-Sat antibodies and PMSF was reduced in about 80 to 90%, respectively. This is the first work demonstrating the expression of Sat by EAEC and the action of the toxin on endothelial cells suggesting that the role of Sat may be broader in pathogenesis than has been proposed so far.

Dans cette thèse nous développons de nouvelles techniques pour résoudre les problèmes d'optimisation multi-critère. Ces problèmes se posent naturellement dans de nombreux domaines d'application (sinon tous) où les choix sont évalués selon différents critères conflictuels (coûts et performance par exemple). Contrairement au cas de l'optimisation classique, de tels problèmes n'admettent pas en général un optimum unique mais un ensemble de solutions incomparables, aussi connu comme le front de Pareto, qui représente les meilleurs compromis possibles entre les objectifs conflictuels. La contribution majeure de la thèse est le développement d'algorithmes pour trouver ou approximer ces solutions de Pareto pour les problèmes combinatoires difficiles. Plusieurs problèmes de ce type se posent naturellement lors du processus de placement et d'ordonnancement d'une application logicielle sur une architecture multi-coeur comme P2012, qui est actuellement développé par STMicroelectronics. / In this thesis we develop new techniques for solving multi-criteria optimization problems. Such problems arise naturally in many (if not all) application domains where choices are evaluated according to two or more conflicting criteria such as price vs. performance. Unlike ordinary optimization, such problems typically do not admit a unique optimum but a set of incomparable solutions, also known as the Pareto Front, which represent the best possible trade-offs between the conflicting goals. The major contribution of the thesis is the development of algorithms for finding or approximating these Pareto solutions for hard combinatorial problems that arise naturally in the process of mapping and scheduling application software on multi-core architectures such as P2012 which is currently being developed by ST Microelectronics.

Este trabalho estuda o problema da Satisfazibilidade Probabilística (PSAT), revendo a sua solução via programação linear, além de propor novos algoritmos para resolvê-lo através da redução ao SAT. Construímos uma redução polinomial do PSAT para o SAT, chamada de Redução Canônica, codificando operações da aritmética racional em bits, como variáveis lógicas. Analisamos a complexidade computacional dessa redução e propomos uma Redução Canônica de Precisão Limitada para contornar tal complexidade. Apresentamos uma Redução de Turing do PSAT ao SAT, baseada no algoritmo Simplex e na Forma Normal Atômica que introduzimos. Sugerimos modificações em tal redução em busca de eficiência computacional. Por fim, implementamos essas reduções a m de investigar o perl de complexidade do PSAT, observamos o fenômeno de transição de fase e discutimos as condições para sua detecção. / This work studies the Probabilistic Satisfiability problem (PSAT), reviewing its solution through linear programming, and proposing new algorithms to solve it. We construct a polynomial many-to-one reduction from PSAT to SAT, called Canonical Reduction, codifying rational arithmetic operations into bits, as logical variables. We analyze the computational complexity of this reduction and we propose a Limited Precision Canonical Reduction to reduce such complexity. We present a Turing Reduction from PSAT to SAT, based on the Simplex algorithm and the Atomic Normal Form we introduced. We suggest modifications in such reduction looking for computational eficiency. Finally, we implement these reductions in order to investigate the complexity profile of PSAT, the phase transition phenomenom is observed and the conditions for its detection are discussed.

No description available.

Quoique très difficile à résoudre, le problème de satisfiabilité Booléenne (SAT) est fréquemment utilisé lors de la modélisation d’applications industrielles. À cet effet, les deux dernières décennies ont vu une progression fulgurante des outils conçus pour trouver des solutions à ce problème NP-complet. Deux grandes avenues générales ont été explorées afin de produire ces outils, notamment l’approche logicielle et matérielle. Afin de raffiner et améliorer ces solveurs, de nombreuses techniques et heuristiques ont été proposées par la communauté de recherche. Le but final de ces outils a été de résoudre des problèmes de taille industrielle, ce qui a été plus ou moins accompli par les solveurs de nature logicielle. Initialement, le but de l’utilisation du matériel reconfigurable a été de produire des solveurs pouvant trouver des solutions plus rapidement que leurs homologues logiciels. Cependant, le niveau de sophistication de ces derniers a augmenté de telle manière qu’ils restent le meilleur choix pour résoudre SAT. Toutefois, les solveurs modernes logiciels n’arrivent toujours pas a trouver des solutions de manière efficace à certaines instances SAT. Le but principal de ce mémoire est d’explorer la résolution du problème SAT dans le contexte du matériel reconfigurable en vue de caractériser les ingrédients nécessaires d’un solveur SAT efficace qui puise sa puissance de calcul dans le parallélisme conféré par une plateforme FPGA. Le prototype parallèle implémenté dans ce travail est capable de se mesurer, en termes de vitesse d’exécution à d’autres solveurs (matériels et logiciels), et ce sans utiliser aucune heuristique. Nous montrons donc que notre approche matérielle présente une option prometteuse vers la résolution d’instances industrielles larges qui sont difficilement abordées par une approche logicielle. / Though very difficult to solve, the Boolean satisfiability problem (SAT) is extensively used to model various real-world applications and problems. Over the past two decades, researchers have tried to provide tools that are used, to a certain degree, to find solutions to the Boolean satisfiability problem. The nature of these tools is broadly divided in software and reconfigurable hardware solvers. In addition, the main algorithms used to solve this problem have also been complemented with heuristics of various levels of sophistication to help overcome some of the NP-hardness of the problem. The end goal of these tools has been to provide solutions to industrial-sized problems of enormous size. Initially, reconfigurable hardware tools provided a promising avenue to accelerating SAT solving over traditional software based solutions. However, the level of sophistication of software solvers overcame their hardware counterparts, which remained limited to smaller problem instances. Even so, modern state-of-the-art software solvers still fail unpredictably on some instances. The main focus of this thesis is to explore solving SAT on reconfigurable hardware in order to gain an understanding of what would be essential ingredients to add (and discard) to a very efficient hardware SAT solver that obtains its processing power from the raw parallelism of an FPGA platform. The parallel prototype solver that was implemented in this work has been found to be comparable with other hardware and software solvers in terms of execution speed even though no heuristics or other helping techniques were implemented. We thus show that our approach provides a very promising avenue to solving large, industrial SAT instances that might be difficult to handle by software solvers.