Projecto de uma caixa de velocidades eléctrica por meio da variação do número de pólos para motores em disco de rotor em alumínio e em materiais supercondutores de alta temperatura (SAT)

Nesta dissertação apresenta-se um motor em disco polifásico inovador bem como uma estratégia de controlo com base no método de variação de velocidade por comutação do número de pares de pólos. A configuração das bobinas aliada à escolha das correntes e tensões que se injectam nas bobinas dos estatores, permite comutar electronicamente o número de pólos do motor entre 2, 4 6 e 8 pólos, conseguindo-se controlar a característica binário/velocidade do motor. O motor em disco possui a bobinagem feita em cobre com dois semi-estatores, em que quando utiliza o rotor em alumínio (com condutividade diferente de zero) comporta-se como um motor de indução convencional. Quando se substitui o rotor em alumínio por um constituído por um supercondutor de alta temperatura (SAT), o dispositivo comporta-se como um motor de histerese. O princípio de funcionamento do motor em disco convencional é baseado na indução de força electromotrizes no rotor e, consequentemente, uma vez que o alumínio é bom condutor eléctrico, correntes eléctricas induzidas, originadas por haver um campo magnético variável que é criado pelos semi-estatores. O comportamento deste tipo de motores, no que diz respeito a principais características (como o binário/velocidade para os diferentes números de pares de pólos), circuito equivalente de Steinmetz, entre outras teorias associadas é já conhecido há bastante tempo. O princípio de funcionamento do motor SAT é diferente do apresentado anteriormente, funciona com base na dinâmica de vórtices e devido ao facto de aparecer o fenómeno de ancoragem de fluxo (flux pinning) nos supercondutores de alta temperatura. Como o campo magnético varia, então o disco roda. Este motor tem um princípio de funcionamento muito mais complexo que o motor de indução sendo a obtenção do modelo do motor SAT complicada. A obtenção do modelo do motor SAT não é abordado nesta dissertação. Os comportamentos e modos de operação do motor com disco de alumínio e em materiais SAT são simulados através de um programa comercial de elementos finitos, nesta dissertação, sendo a supercondutividade simulada com base na relação entre o campo eléctrico e a densidade de corrente pela lei da potenciação (E-J power law). Com as simulações pretende-se comparar o rendimento electromecânico de ambos os motores.

An approximation algorithm for #k-SAT

"Vegeu el resum a l'inici del document del fitxer adjunt"

Disseny, implementació i avaluació d'algorismes Max-SAT multivaluats

La finalitat d'aquest projecte és definir el problema Max-SAT amb codificació multiavaluada, implementar algorismes exactes de resolució del problema i construir un generador aleatori de problemes que permeti avaluar aquests algorismes.

SAT Modulo Linear Arithmetic for Solving Polynomial

Polynomial constraint solving plays a prominent role in several areas of hardware and software analysis and verification, e.g., termination proving, program invariant generation and hybrid system verification, to name a few. In this paper we propose a new method for solving non-linear constraints based on encoding the problem into an SMT problem considering only linear arithmetic. Unlike other existing methods, our method focuses on proving satisfiability of the constraints rather than on proving unsatisfiability, which is more relevant in several applications as we illustrate with several examples. Nevertheless, we also present new techniques based on the analysis of unsatisfiable cores that allow one to efficiently prove unsatisfiability too for a broad class of problems. The power of our approach is demonstrated by means of extensive experiments comparing our prototype with state-of-the-art tools on benchmarks taken both from the academic and the industrial world.

An efficient solver for weighted Max-SAT

We present a new branch and bound algorithm for weighted Max-SAT, called Lazy which incorporates original data structures and inference rules, as well as a lower bound of better quality. We provide experimental evidence that our solver is very competitive and outperforms some of the best performing Max-SAT and weighted Max-SAT solvers on a wide range of instances.

Generating hard SAT/CSP instances using expander graphs

In this paper we provide a new method to generate hard k-SAT instances. We incrementally construct a high girth bipartite incidence graph of the k-SAT instance. Having high girth assures high expansion for the graph, and high expansion implies high resolution width. We have extended this approach to generate hard n-ary CSP instances and we have also adapted this idea to increase the expansion of the system of linear equations used to generate XORSAT instances, being able to produce harder satisfiable instances than former generators.

Edge matching puzzles as hard SAT/CSP benchmarks

Recently, edge matching puzzles, an NP-complete problem, have rececived, thanks to money-prized contests, considerable attention from wide audiences. We consider these competitions not only a challenge for SAT/CSP solving techniques but also as an opportunity to showcase the advances in the SAT/CSP community to a general audience. This paper studies the NP-complete problem of edge matching puzzles focusing on providing generation models of problem instances of variable hardness and on its resolution through the application of SAT and CSP techniques. From the generation side, we also identify the phase transition phenomena for each model. As solving methods, we employ both; SAT solvers through the translation to a SAT formula, and two ad-hoc CSP solvers we have developed, with different levels of consistency, employing several generic and specialized heuristics. Finally, we conducted an extensive experimental investigation to identify the hardest generation models and the best performing solving techniques.

A Write-Based Solver for SAT Modulo the Theory of Arrays

The extensional theory of arrays is one of the most important ones for applications of SAT Modulo Theories (SMT) to hardware and software verification. Here we present a new T-solver for arrays in the context of the DPLL(T) approach to SMT. The main characteristics of our solver are: (i) no translation of writes into reads is needed, (ii) there is no axiom instantiation, and (iii) the T-solver interacts with the Boolean engine by asking to split on equality literals between indices. As far as we know, this is the first accurate description of an array solver integrated in a state-of-the-art SMT solver and, unlike most state-of-the-art solvers, it is not based on a lazy instantiation of the array axioms. Moreover, it is very competitive in practice, specially on problems that require heavy reasoning on array literals

Parallelization of SAT on Reconfigurable Hardware

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.

Cracking the SAT. U.S. and World history subject tests.

Scholastic Aptitude Test (SAT) se trata de una prueba estandarizada usada frecuentemente para valorar los conocimientos adquiridos durante la enseñanza secundaria por los estudiantes que deseen acceder a una educación superior en EE.UU. Esta publicación proporciona la información y las estrategias necesarias para maximizar la puntuación de la prueba del SAT en historia. Enseña a pensar como los redactores de la prueba, y a practicar con la materia que se pondrá en el examen para poder estudiar con mayor eficacia. Se hace una revisión de las épocas históricas que van a aparecer en la prueba y facilita con explicaciones detalladas técnicas para aplicar los conocimientos aprendidos en resolver cuestiones específicas complicadas. Incluye cuatro ensayos prácticos con preguntas de opción múltiple de una hora de duración cada una: dos pruebas de historia de Estados Unidos desde la aprobación de la Constitución hasta la actualidad, y dos pruebas para historia universal.

Cracking the SAT. Biology E, M subject test.

Scholastic Aptitude Test (SAT) se trata de una prueba estandarizada usada frecuentemente para valorar los conocimientos adquiridos durante la enseñanza secundaria por los estudiantes que deseen acceder a una educación superior en EE.UU. Esta publicación proporciona la información y las estrategias necesarias para maximizar la puntuación de la prueba del SAT en biología. Enseña a pensar como los redactores de la prueba, y a practicar con la materia que se pondrá en el examen para poder estudiar con mayor eficacia. Se hace una revisión de los conceptos principales de la biología que van a aparecer en la prueba y facilita, con explicaciones detalladas, estrategias para aplicar los conocimientos aprendidos en resolver cuestiones específicas complicadas. Incluye dos ensayos prácticos de una hora de duración con preguntas de opción múltiple.

Cracking the SAT. Literature subject test.

Scholastic Aptitude Test (SAT) se trata de una prueba estandarizada usada frecuentemente para valorar los conocimientos adquiridos durante la enseñanza secundaria por los estudiantes que deseen acceder a una educación superior en EE.UU. Esta publicación ,proporciona la información y las estrategias necesarias para desarrollar la capacidad de comprender y analizar textos literarios seleccionados de prosa, poesía y teatro escritos en inglés, para maximizar la puntuación de la prueba del SAT en literatura. Enseña a pensar como los redactores de la prueba, y a practicar con la materia que se pondrá en el examen para poder estudiar con mayor eficacia. Se hace una revisión de los conceptos principales de la literatura que van a aparecer en la prueba y facilita con explicaciones detalladas técnicas para aplicar los conocimientos aprendidos en resolver cuestiones específicas complicadas. Incluye cuatro ensayos prácticos de una hora de duración cada uno con preguntas de opción múltiple que se centran en conocimientos básicos de términos literarios.

Cracking the SAT. Math 1 and 2 subject tests.

Scholastic Aptitude Test (SAT) se trata de una prueba estandarizada usada frecuentemente para valorar los conocimientos adquiridos durante la enseñanza secundaria por los estudiantes que deseen acceder a una educación superior en EE.UU. Esta publicación proporciona la información y las estrategias necesarias para maximizar la puntuación de la prueba del SAT en matemáticas. Enseña a pensar como los redactores de la prueba, y a practicar con la materia que se pondrá en el examen para poder estudiar con mayor eficacia. Se hace una revisión de los conceptos principales desde el álgebra básica a la geometría, trigonometría y la estadística que van a aparecer en la prueba y facilita con explicaciones detalladas estrategias para aplicar los conocimientos aprendidos en resolver cuestiones específicas complicadas. Incluye cuatro ensayos prácticos con cincuenta preguntas de selección múltiple de una hora de duración cada uno.

Cracking the SAT. Physics subject test.

Scholastic Aptitude Test (SAT) se trata de una prueba estandarizada usada frecuentemente para valorar los conocimientos adquiridos durante la enseñanza secundaria por los estudiantes que deseen acceder a una educación superior en EE.UU. Esta publicación proporciona la información y las estrategias necesarias para maximizar la puntuación de la prueba del SAT en física. Enseña a pensar como los redactores de la prueba, y a practicar con la materia que se pondrá en el examen para poder estudiar con mayor eficacia. Se hace una revisión de los conceptos principales de la física que van a aparecer en la prueba y facilita, con explicaciones detalladas estrategias para aplicar los conocimientos aprendidos en resolver cuestiones específicas complicadas. Incluye dos ensayos prácticos con setenta y cinco preguntas de opción múltiple, con una hora de duración para cada uno.