1 |
Polynomiální rovnice nad konečnými tělesy a algebraická kryptoanalýza / Polynomial equations over finite fields and algebraic cryptanalysisSeidl, Jan January 2014 (has links)
Title: Polynomial equations over finite fields and algebraic cryptanalysis Author: Jan Seidl Department: Department of Algebra Supervisor: doc. RNDr. David Stanovský, Ph.D., Department of Algebra Abstract: The present work deals with the procedure of algebraic crypta- nalysis, in which the problem of breaking cipher is at first converted to the problem of finding solutions to polynomial systems of equations and then the problem of finding a solution to this equation is converted to the SAT problem. The work specifically describes the methods that allow you to con- vert the problem of breaking cipher RC4 to the SAT problem. The individual methods were programmed in Mathematica programming language and then applied to RC4 with a word length of 2, 3. For finding of satisfiable evaluation of the resulting logical formula was used SAT-solver CryptoMiniSAT. In case of RC4 with word length 2 the solution was reached in the range from 0.09 to 0.34 second. In case of RC4 with word length 3 the solution was reached in the range from 1.10 to 1.23 second. Keywords: RC4, SAT, CryptoMiniSAT 1
|
2 |
Améliorer l'efficacité de l'algorithme CDCL : décompositions arborescentes de grandes instances, CDCL sans saut arrière et CDCL à ordre partielMonnet, Anthony Jean-Luc 08 1900 (has links) (PDF)
Cette thèse s'intéresse à l'amélioration des performances pratiques de l'algorithme CDCL (Conftict-Driven Clause Learning) pour la résolution du problème de satisfaisabilité des formules propositionnelles, ou problème SAT. Plus particulièrement, nous cherchons à diminuer la destruction de l'instanciation courante lors des étapes de saut arrière, qui peuvent occasionner la désinstanciation de nombreuses variables n'ayant aucun rapport direct avec le conflit à résoudre. Dans ce but, nous proposons trois approches différentes. La première est une amélioration de l'utilisabilité de la méthode déjà existante de décomposition implicite d'une instance SAT. Notre but principal est de permettre son application à des instances de plus grande taille possible, après avoir montré les limitations des implémentations existantes. Nous développons également deux variations de l'algorithme CDCL, le CDCL sans saut arrière et le CDCL à ordre partiel. Si le premier supprime totalement la notion de saut arrière en permettant la propagation des clauses unitaires à des niveaux de décision quelconques, le second rend le saut arrière plus sélectif, en désinstanciant uniquement les niveaux de décision qui dépendent du niveau de retour du saut arrière. Notre analyse est à la fois théorique, notamment par une analyse détaillée des propriétés de différentes variations des CDCL sans saut arrière et à ordre partiel, et pratique, puisque l'efficacité de nos contributions est évaluée en les implémentant comme modifications de solveurs SAT de l'état de l'art et en se servant de ces implémentations sur des instances SAT difficiles utilisées lors de compétitions internationales de solveurs.
______________________________________________________________________________
MOTS-CLÉS DE L’AUTEUR : problème SAT, satisfaisabilité, formules propositionnelles, CDCL, décomposition arborescente, retour arrière, ordre partiel.
|
3 |
A New SAT Encoding of Earley ParsingNeil, Tobias January 2015 (has links)
While the Boolean satisfiability problem (SAT) lies in NP, prodigious work in SAT solvers has allowed for its use in modeling a multitude of practical problems. Stating a problem in SAT can be cumbersome though and so the demand for SAT encodings arises, providing a means to formulate problems or parts of problems in a more intuitive environment. Several algorithms have been proposed in the past to encode context-free grammars as SAT formulae, allowing for the comprehensive construction of many interesting constraints such as at-most k constraints or such ones pertaining to language syntax. In 2011 a new algorithm was proposed, differing from previous ones in it being based on Earley parsing instead of CYK parsing. Although it performed well for interesting groups of grammars it was later found to behave incorrectly for certain inputs. This thesis discusses the flaws in said algorithm, presents a revision of it and argues for the altered algorithm's correctness. The alterations come with a price, however, and both the running time and output size complexities suffer more-than-quadratic blowup. Since no empirical tests have been performed as of yet, it is still unclear what impact this blowup will have on practical instances.
|
4 |
Scholastic aptitude test in mathematics as a predictor of student selection of algebraic versus geometric approaches to problem solving /Price, Richard Lionel January 1969 (has links)
No description available.
|
5 |
Optimisation booléenne multiobjectif : complexité sous contraintes compilées et résolution via SAT / Multiobjective boolean optimizationLonca, Emmanuel 26 June 2015 (has links)
L’aide à la décision a pour but d’assister un opérateur humain dans ses choix. La nécessité d’employer de telles techniques s’est imposée avec la volonté de traiter des problèmes dépendant d’une quantité de données toujours plus importante. L’intérêt de l’aide à la décision est encore plus manifeste lorsqu’on souhaite obtenir non pas une solution quelconque, mais une des meilleures solutions d’un problème combinatoire selon un critère donné. On passe alors d’un problème de décision (déterminer l’existence d’une solution) à un problème d’optimisation monocritère (déterminer une des meilleures solutions possibles selon un critère). Un décideur peut aussi souhaiter considérer plusieurs critères, et ainsi faire passer le problème de décision initial à un problème d’optimisation multicritère. La difficulté de ce type de problèmes provient du fait que les critères considérés sont généralement antagonistes, et qu’il n’existe donc pas de solution meilleure que les autres pour l’ensemble des critères. Dans ce cas, il s’agit plutôt de déterminer une solution qui offre un bon compromis entre les critères. Dans cette thèse, nous étudions dans un premier temps la complexité théorique de tâches d’optimisation complexes sur les langages de la logique propositionnelle, puis nous étudions leur résolution pratique via le recours à des logiciels bâtis pour résoudre de manière efficace en pratique des problèmes de décision combinatoires, les prouveurs SAT. / Decision aiding aims at helping a decision-maker to pick up a solution among several others. The usefulness of such approaches is as prominent as the size of the problems under consideration increases. The need of decision aiding techniques is salient when the problem does not just consist in deciding whether a solutions exists, but to find one of the best solutions according to a given criterion. In this case, the problem goes from a decision problem (decide whether a solution exists) to a single criterion optimization problem (find one of the best solutions according to a criterion). A decision-maker may even want to consider multiple criteria, which turns the initial decision problem into a multicriteria optimization problem. The main issue arising in such cases lies in the fact that the criteria under consideration are often antagonistic, which implies that there is no solution which is the best for each of the objectives. In this case, a good compromise solution is looked for. In this thesis, we first focus on the complexity of optimization requests based on a set of propositional languages. We then study the practical aspects of the resolution of such problems, using pieces of software designed for dealing with combinatorial decision problems, namely SAT solvers.
|
6 |
Numerical simulation of the linearised Korteweg-de Vries equation : Diploma work (15 HP) Uppsala University Division of scientific computingBahceci, Ertin January 2014 (has links)
The first main focus in the present project was to analyse the boundary treatment of the linearised Korteweg-de Vries equation. The second main focus was to derive a stable numerical solution using a high-order finite difference method. Since the model involved a third derivative in space, the numerical treatment of the boundaries was highly nontrivial. To aid the boundary treatment high-order accurate first and third derivative finite difference operators were employed. The boundaries are based on the summation-by-parts (SBP) framework, thereby guaranteeing linear stability. The boundary conditions were imposed using a penalty technique. A convergence study was performed where the derived numerical solution was compared with an analytical one. Fourth order accurate Runge-Kutta was used to time-integrate the numerical approximation. Measuring the rate of convergence, q, yielded q = 4 for 4th order accurate SBP-operators and q = 5.5 for 6th order accurate SBP-operators. Thus the convergence study proved the accuracy and stability of the numerical solution derived with the SBP-methodology.
|
7 |
Parallel SAT solvers and their application in automatic parallelization / SAT solvers paralelos e suas aplicações em paralelização automáticaSilveira, Jaime Kirch da January 2014 (has links)
Desde a diminuição da tendência de aumento na frequência de processadores, uma nova tendência surgiu para permitir que softwares tirem proveito de harwares mais rápidos: a paralelização. Contudo, diferente de aumentar a frequência de processadores, utilizar parallelização requer um tipo diferente de programação, a programação paralela, que é geralmente mais difícil que a programação sequencial comum. Neste contexto, a paralelização automática apareceu, permitindo que o software tire proveito do paralelismo sem a necessidade de programação paralela. Nós apresentamos aqui duas propostas: SAT-PaDdlinG e RePaSAT. SAT-PaDdlinG é um SAT Solver DPLL paralelo que roda em GPU, o que permite que RePaSAT utilize esse ambiente. RePaSAT é a nossa proposta de uma máquina paralela que utiliza o Problema SAT para paralelizar automaticamente código sequencial. Como uma GPU provê um ambiente barato e massivamente paralelo, SAT-PaDdlinG tem como objetivo prover esse paralelismo massivo a baixo custo para RePaSAT, como para qualquer outra ferramenta ou problema que utilize SAT Solvers. / Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization. However, different from increasing the frequency of processors, using parallelization requires a different kind of programming, parallel programming, which is usually harder than common sequential programming. In this context, automatic parallelization has arisen, allowing software to take advantage of parallelism without the need of parallel programming. We present here two proposals: SAT-PaDdlinG and RePaSAT. SAT-PaDdlinG is a parallel DPLL SAT Solver on GPU, which allows RePaSAT to use this environment. RePaSAT is our proposal of a parallel machine that uses the SAT Problem to automatically parallelize sequential code. Because GPU provides a cheap, massively parallel environment, SATPaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.
|
8 |
Parallel SAT solvers and their application in automatic parallelization / SAT solvers paralelos e suas aplicações em paralelização automáticaSilveira, Jaime Kirch da January 2014 (has links)
Desde a diminuição da tendência de aumento na frequência de processadores, uma nova tendência surgiu para permitir que softwares tirem proveito de harwares mais rápidos: a paralelização. Contudo, diferente de aumentar a frequência de processadores, utilizar parallelização requer um tipo diferente de programação, a programação paralela, que é geralmente mais difícil que a programação sequencial comum. Neste contexto, a paralelização automática apareceu, permitindo que o software tire proveito do paralelismo sem a necessidade de programação paralela. Nós apresentamos aqui duas propostas: SAT-PaDdlinG e RePaSAT. SAT-PaDdlinG é um SAT Solver DPLL paralelo que roda em GPU, o que permite que RePaSAT utilize esse ambiente. RePaSAT é a nossa proposta de uma máquina paralela que utiliza o Problema SAT para paralelizar automaticamente código sequencial. Como uma GPU provê um ambiente barato e massivamente paralelo, SAT-PaDdlinG tem como objetivo prover esse paralelismo massivo a baixo custo para RePaSAT, como para qualquer outra ferramenta ou problema que utilize SAT Solvers. / Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization. However, different from increasing the frequency of processors, using parallelization requires a different kind of programming, parallel programming, which is usually harder than common sequential programming. In this context, automatic parallelization has arisen, allowing software to take advantage of parallelism without the need of parallel programming. We present here two proposals: SAT-PaDdlinG and RePaSAT. SAT-PaDdlinG is a parallel DPLL SAT Solver on GPU, which allows RePaSAT to use this environment. RePaSAT is our proposal of a parallel machine that uses the SAT Problem to automatically parallelize sequential code. Because GPU provides a cheap, massively parallel environment, SATPaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.
|
9 |
Parallel SAT solvers and their application in automatic parallelization / SAT solvers paralelos e suas aplicações em paralelização automáticaSilveira, Jaime Kirch da January 2014 (has links)
Desde a diminuição da tendência de aumento na frequência de processadores, uma nova tendência surgiu para permitir que softwares tirem proveito de harwares mais rápidos: a paralelização. Contudo, diferente de aumentar a frequência de processadores, utilizar parallelização requer um tipo diferente de programação, a programação paralela, que é geralmente mais difícil que a programação sequencial comum. Neste contexto, a paralelização automática apareceu, permitindo que o software tire proveito do paralelismo sem a necessidade de programação paralela. Nós apresentamos aqui duas propostas: SAT-PaDdlinG e RePaSAT. SAT-PaDdlinG é um SAT Solver DPLL paralelo que roda em GPU, o que permite que RePaSAT utilize esse ambiente. RePaSAT é a nossa proposta de uma máquina paralela que utiliza o Problema SAT para paralelizar automaticamente código sequencial. Como uma GPU provê um ambiente barato e massivamente paralelo, SAT-PaDdlinG tem como objetivo prover esse paralelismo massivo a baixo custo para RePaSAT, como para qualquer outra ferramenta ou problema que utilize SAT Solvers. / Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization. However, different from increasing the frequency of processors, using parallelization requires a different kind of programming, parallel programming, which is usually harder than common sequential programming. In this context, automatic parallelization has arisen, allowing software to take advantage of parallelism without the need of parallel programming. We present here two proposals: SAT-PaDdlinG and RePaSAT. SAT-PaDdlinG is a parallel DPLL SAT Solver on GPU, which allows RePaSAT to use this environment. RePaSAT is our proposal of a parallel machine that uses the SAT Problem to automatically parallelize sequential code. Because GPU provides a cheap, massively parallel environment, SATPaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.
|
10 |
Análise da distribuição do número de operações de resolvedores SAT / Distribution\'s analysis of operations\'s number of SAT solversReis, Poliana Magalhães 28 February 2012 (has links)
No estudo da complexidade de problemas computacionais destacam-se duas classes conhecidas como P e NP. A questao P=NP e um dos maiores problemas nao resolvidos em Ciencia da Compu- tacao teorica e Matematica contemporanea. O problema SAT foi o primeiro problema reconhecido como NP-completo e consiste em verificar se uma determinada formula da logica proposicional clas- sica e ou nao satisfazivel. As implementacoes de algoritmos para resolver problemas SAT sao conhe- cidas como resolvedores SAT (SAT Solvers). Existem diversas aplicacoes em Ciencia da Computacao que podem ser realizadas com SAT Solvers e com outros resolvedores de problemas NP-completos que podem ser reduzidos ao SAT como por exemplo problemas de coloracao de grafos, problemas de agendamento e problemas de planejamento. Dentre os mais eficientes algoritmos para resolvedores de SAT estao Sato, Grasp, Chaff, MiniSat e Berkmin. O Algoritmo Chaff e baseado no Algoritmo DPLL o qual existe a mais de 40 anos e e a estrategia mais utilizada para os Sat Solvers. Essa dissertacao apresenta um estudo aprofundado do comportamento do zChaff (uma implementacao muito eficiente do Chaff) para saber o que esperar de suas execucoes em geral . / In the study of computational complexity stand out two classes known as P and NP. The question P = NP is one of the greatest unsolved problems in theoretical computer science and contemporary mathematics. The SAT problem was first problem recognized as NP-complete and consists to check whether a certain formula of classical propositional logic is satisfiable or not. The implementations of algorithms to solve SAT problems are known as SAT solvers. There are several applications in computer science that can be performed with SAT solvers and other solvers NP- complete problems can be reduced to SAT problems such as graph coloring, scheduling problems and planning problems. Among the most efficient algorithms for SAT solvers are Sato, Grasp, Chaf, MiniSat and Berkmin. The Chaff algorithm is based on the DPLL algorithm which there is more than 40 years and is the most used strategy for Sat Solvers. This dissertation presents a detailed study of the behavior of zChaff (a very efficient implementation of the Chaff) to know what to expect from their performance in general.
|
Page generated in 0.027 seconds