This work deals with the PSO technique (Particle Swarm Optimization), which is capable to solve complex problems. This technique can be used for solving complex combinatorial problems (the traveling salesman problem, the tasks of knapsack), design of integrated circuits and antennas, in fields such as biomedicine, robotics, artificial intelligence or finance. Although the PSO algorithm is very efficient, the time required to seek out appropriate solutions for real problems often makes the task intractable. The goal of this work is to accelerate the execution time of this algorithm by the usage of Graphics processors (GPU), which offers higher computing potential while preserving the favorable price and size. The boolean satisfiability problem (SAT) was chosen to verify and benchmark the implementation. As the SAT problem belongs to the class of the NP-complete problems, any reduction of the solution time may broaden the class of tractable problems and bring us new interesting knowledge.

No description available.

Dans cette thèse, nous nous intéressons à la résolution du problème de la satisfiabilité propositionnelle (SAT). Ce problème fondamental en théorie de la complexité est aujourd'hui utilisé dans de nombreux domaines comme la planification, la bio-informatique, la vérification de matériels et de logiciels. En dépit d'énormes progrès observés ces dernières années dans la résolution pratique du problème SAT, il existe encore une forte demande d'algorithmes efficaces pouvant permettre de résoudre les problèmes difficiles. C'est dans ce contexte que se situent les différentes contributions apportées par cette thèse. Ces contributions s'attellent principalement autour de deux composants clés des solveurs SAT : l'apprentissage de clauses et les heuristiques de choix de variables de branchement. Premièrement, nous proposons une méthode de résolution permettant d'exploiter les fonctions booléennes cachées généralement introduites lors de la phase d'encodage CNF pour réduire la taille des clauses apprises au cours de la recherche. Ensuite, nous proposons une approche de résolution basée sur le principe d'intensification qui indique les variables sur lesquelles le solveur devrait brancher prioritairement à chaque redémarrage. Ce principe permet ainsi au solveur de diriger la recherche sur la sous-formule booléenne la plus contraignante et de tirer profit du travail de recherche déjà accompli en évitant d'explorer le même sous-espace de recherche plusieurs fois. Dans une troisième contribution, nous proposons un nouveau schéma d'apprentissage de clauses qui permet de dériver une classe particulière de clauses Bi-Assertives et nous montrons que leur exploitation améliore significativement les performances des solveurs SAT CDCL issus de l'état de l'art. Finalement, nous nous sommes intéressés aux principales stratégies de gestion de la base de clauses apprises utilisées dans la littérature. En effet, partant de deux stratégies de réduction simples : élimination des clauses de manière aléatoire et celle utilisant la taille des clauses comme critère pour juger la qualité d'une clause apprise, et motiver par les résultats obtenus à partir de ces stratégies, nous proposons plusieurs nouvelles stratégies efficaces qui combinent le maintien de clauses courtes (de taille bornée par k), tout en supprimant aléatoirement les clauses de longueurs supérieures à k. Ces nouvelles stratégies nous permettent d'identifier les clauses les plus pertinentes pour le processus de recherche. / In this thesis, we focus on propositional satisfiability problem (SAT). This fundamental problem in complexity theory is now used in many application domains such as planning, bioinformatic, hardware and software verification. Despite enormous progress observed in recent years in practical SAT solving, there is still a strong demand of efficient algorithms that can help to solve hard problems. Our contributions fit in this context. We focus on improving two of the key components of SAT solvers: clause learning and variable ordering heuristics. First, we propose a resolution method that allows to exploit hidden Boolean functions generally introduced during the encoding phase CNF to reduce the size of clauses learned during the search. Then, we propose an resolution approach based on the intensification principle that circumscribe the variables on which the solver should branch in priority at each restart. This principle allows the solver to direct the search to the most constrained sub-formula and takes advantage of the previous search to avoid exploring the same part of the search space several times. In a third contribution, we propose a new clause learning scheme that allows to derive a particular Bi-Asserting clauses and we show that their exploitation significantly improves the performance of the state-of-the art CDCL SAT solvers. Finally, we were interested to the main learned clauses database reduction strategies used in the literature. Indeed, starting from two simple strategies : random and size-bounded reduction strategies, and motivated by the results obtained from these strategies, we proposed several new effective ones that combine maintaing short clauses (of size bounded by k), while deleting randomly clauses of size greater than k. Several other efficient variants are proposed. These new strategies allow us to identify the most important learned clauses for the search process.

The goal of this Master's Thesis is finding a SAT solving heuristic by the application of an evolutionary algorithm. This thesis surveys various approaches used in SAT solving and some variants of evolutionary algorithms that are relevant to this topic. Afterwards the implementation of a linear genetic programming system that searches for a suitable heuristic for SAT problem instances is described, together with the implementation of a custom SAT solver which expoloits the output of the genetic program. Finally, the achieved results are summarized.

Malgré sa complexité de résolution, le problème de SATisfaisabilité est une excellente et compétitive approche pour résoudre un large éventail de problèmes. Cela génère une forte demande pour une résolution de SAT haute performance de la part des industriels. Au fil du temps, de nombreuses approches et optimisations différentes ont été développées pour résoudre le problème plus efficacement. Ces innovations ont été faites sans prendre en compte le développement des micro processeurs actuels qui voient le nombre de leur cœurs de calcul augmenter. Cette thèse présente un nouveau type d'algorithme parallèle basé sur une forte collaboration où un processus riche est en charge de l'évaluation de l'arbre de recherche et où des processus pauvres fournissent des informations partielles ou globales, heuristiques ou logiques afin de simplifier la tâche du riche. Pour concrétiser ce solveur et le rendre efficace, nous avons étendu la notion de chemin de guidage à celle d'arbre de guidage. L'arbre de recherche est totalement partagé en mémoire centrale et tous les processeurs peuvent y travailler en même temps. Ce nouveau solveur est appelé MTSS pour Multi-Threaded SAT Solver. De plus, nous avons implémenté une tâche pour les processus riche et pauvres qui leur permet d'exécuter un solveur SAT externe, et cela, avec ou sans échange de lemmes afin de paralléliser tous types de solveurs (dédiés aux formules industrielles ou aléatoires). Ce nouvel environnement facilite la parallélisation des futures implémentations pour SAT. Quelques exemples et expérimentations, avec ou sans échange de lemmes, de parallélisation de solveurs externes sont présentées, mais aussi des résultats sur les performances de MTSS. Il est intéressant de noter que certaines accélérations sont super linéaires.

This study examines the effectiveness of traditional admissions criteria, including prior GPA, SAT, GRE, and TOEFL in predicting undergraduate and graduate academic success for American and international students at a large public university in the southwestern United States. Included are the admissions and enrollment data for 25,017 undergraduate American, 509 undergraduate international, 5,421 graduate American, and 1,733 graduate international students enrolled between 2005 to 2009.Person product-moment correlation, multiple regression, and user-determined stepwise regression were applied to the data. Results show high school GPA is the most predictive of first-year college GPA for both undergraduate American and international students. SAT has a medium correlation with first-year college GPA for American students and a large correlation for international students. High school GPA and SAT together explain one fourth of the variance in first-year college GPA for American students and over one half of the variance for international students. TOEFL has a medium correlation with first-year GPA for undergraduate international students but is not a significant predictor of first-year GPA when SAT is included in multiple regression. Unlike the results for undergraduate students, the traditional admissions criteria (undergraduate GPA and GRE) for graduate admissions explain a small portion of variance in first-year graduate GPA. Undergraduate GPA, GRE Verbal, and Quantitative together explain 6.3% of variance in first-year graduate GPA for American students and 3.1% for international students. The GRE Subject Tests are the best predictor of first-year graduate GPA for students who had taken the GRE Subject Tests. TOEFL has a small correlation with first-year graduate GPA for international students, and it is not a significant predictor of graduate GPA when GRE-Verbal is included. These findings have implications for undergraduate and graduate admissions, standardized admissions tests, university curriculum, and students' academic success.

A finite difference based solution method is derived for the velocity-pressure formulation of the two-dimensional incompressible Navier-Stokes equations. The method is proven stable using the energy method, facilitated by SBP operators, for characteristic and Dirichlet boundary condition implemented using the SAT technique. The numerical experiments show the utility of high-order finite difference methods as well as emphasize the problem of pressure boundary conditions. Furthermore, we demonstrate that a discretely divergence free solution can be obtained by use of the projection method.

Testing constraints for real-time systems are usually verified through the satisfiability of propositional formulae. In this paper, we propose an alternative where the verification of timing constraints can be done by counting the number of truth assignments instead of boolean satisfiability. This number can also tell us how “far away” is a given specification from satisfying its safety assertion. Furthermore, specifications and safety assertions are often modified in an incremental fashion, where problematic bugs are fixed one at a time. To support this development, we propose an incremental algorithm for counting satisfiability. Our proposed incremental algorithm is optimal as no unnecessary nodes are created during each counting. This works for the class of path RTL. To illustrate this application, we show how incremental satisfiability counting can be applied to a well-known rail-road crossing example, particularly when its specification is still being refined. / Singapore-MIT Alliance (SMA)

The VLSI CAD flow encompasses an abundance of critical NP-complete and PSPACE-complete problems. Instead of developing a dedicated algorithm for each, the trend during the last decade has been to encode them in formal languages, such as Boolean satisfiability (SAT) and quantified Boolean formulas (QBFs), and focus academic resources on improving SAT and QBF solvers. The significant progress of these solvers has validated this strategy. This dissertation contributes to the further advancement of formal techniques in CAD. Today, the verification and debugging of increasingly complex RTL designs can consume up to 70% of the VLSI design cycle. In particular, RTL debug is a manual, resource-intensive task in the industry. The first contribution of this thesis is an in-depth examination of the factors affecting the theoretical computational complexity of debugging. It is established that most variations of the debugging problem are NP-complete. Automated debugging tools return all potential error sources in the RTL, called solutions, that can explain a given failing error trace. Finding each solution requires a separate call to a formal engine, which is computationally expensive. The second contribution of this dissertation comprises techniques for reducing the number of such iterations, by leveraging dominance relationships between RTL blocks to imply solutions. Extensive experiments on industrial designs show a three-fold reduction in the number of formal engine calls due to solution implications, resulting in a 1.64x overall speed-up. The third contribution aims to advance the state-of-the-art of QBF solvers, whose progress has not been as impressive as that of SAT solvers. We present a framework for using complete dominators to preprocess and reduce QBFs with an inherent circuit structure, which is common in encodings of PSPACE-complete CAD problems. Experiments show that three modern QBF solvers together solve 55% of preprocessed QBF instances, compared to none without preprocessing. The final contribution consists of a series of QBF encodings for evaluating the reconfigurability of partially programmable circuits (PPCs). The metrics of fault tolerance, design error tolerance and engineering change coverage are defined for PPCs and encoded using QBFs. These formulations along with experimental results demonstrate the theoretical and practical appropriateness of QBFs for dealing with reconfigurability.

The size and complexity of modern VLSI computer chips are growing at a rapid pace. Functional debugging is increasingly becoming a bottleneck in the design flow where it can take up to 60% of the total verification time. Scaling existing automated debugging tools is necessary in order to continue along this path of rapid growth and innovation in the semiconductor industry. This thesis aims to scale automated debugging techniques with two contributions. The first contribution introduces a succinct memory model for automated design debugging that dramatically lowers the memory requirements for the debugging problem. The second contribution presents a scalable SAT-based design debugging algorithm that uses a mathematical technique called interpolation to divide the debugging problem into multiple parts across time which greatly reduces the peak memory requirements of the debugging problem. Extensive experiments on real designs demonstrate the benefit of this work.