A wide range of problems can be formalized as a set of constraints that need to be satisfied. In fact, such a model is called a constraint satisfaction problem (CSP). Another way to represent a problem is to express it as a formula in propositional logic, or, in other words, a Boolean satisfiability problem (SAT). In the quest to find efficient algorithms for solving instances of CSP and SAT specialised software has been developed. It is, however, not clear when should we choose a SAT-solver over a constraint solver (and vice versa). CSP-solvers are known for their domain-specific reasoning, whereas SAT-solvers are considered to be remarkably fast on Boolean instances. In this thesis we tackle these issues by investigating the connections between CSP and SAT. In order to answer the question why SAT-solvers are so efficient on certain classes of CSP instances, we first present the various ways one can encode a CSP instance into SAT. Next, we show that with some encodings SAT-solvers simulate the effects of enforcing a form of local consistency, called k-consistency, in expected polynomial-time. Thus SAT-solvers are able to solve CSP instances of bounded-width structure efficiently in contrast to conventional constraint solvers. By considering the various ways one can encode CSP domains into SAT, we give theoretical reasons for choosing a particular SAT encoding for several important classes of CSP instances. In particular, we show that with this encoding many problem instances that can be solved in polynomial-time will still be easily solvable once they are translated into SAT. Furthermore, we show that this is not true for several other encodings. Finally, we compare the various ways one can use a SAT-solver to solve the classical problem of the pigeonhole principle. We perform both theoretical and empirical comparison of the various encodings. We conclude that none of the known encodings for the classical representation of the problem will result in an efficiently-solvable SAT instance. Thus in this case constraint solvers are a much better choice.

With the growing complexity of modern VLSI designs, design errors become increasingly common. Design debugging today emerges as a bottleneck in the design flow, consuming up to 30% of the overall design effort. Unfortunately, design debugging is still a predominantly manual process in the industry. To tackle this problem, we enhance existing automated debugging tools and extend their applications to different design domains. The first contribution improves the performance of automated design debugging tools by using structural circuit properties, namely dominance relationships and non-solution implications. Overall, a 42% average reduction in solving run-time demonstrates the efficacy of this approach. The second contribution presents an automated debugging methodology for clock-gating design. Using clock-gating properties, we optimize existing debugging techniques to localizes and rectifies the design errors introduced by clock-gating implementations. Experiments show a 6% average reduction in debugging time and 80% of the power-savings retained.

With the growing complexity of modern VLSI designs, design errors become increasingly common. Design debugging today emerges as a bottleneck in the design flow, consuming up to 30% of the overall design effort. Unfortunately, design debugging is still a predominantly manual process in the industry. To tackle this problem, we enhance existing automated debugging tools and extend their applications to different design domains. The first contribution improves the performance of automated design debugging tools by using structural circuit properties, namely dominance relationships and non-solution implications. Overall, a 42% average reduction in solving run-time demonstrates the efficacy of this approach. The second contribution presents an automated debugging methodology for clock-gating design. Using clock-gating properties, we optimize existing debugging techniques to localizes and rectifies the design errors introduced by clock-gating implementations. Experiments show a 6% average reduction in debugging time and 80% of the power-savings retained.

A cryptographic protocol is a structured exchange of messages protected by means of cryptographic algorithms. Computer security in general relies heavily on these protocols and algorithms; in turn, these rely absolutely on smaller components called primitives. As technology advances, computers have reached a cost and a degree of miniaturisation conducive to their proliferation throughout society in the form of software-controlled network-enabled things. As these things find their way into environments where security is critical, their protection ultimately relies on primitives; if a primitive fails, all security solutions (protocols, policies, etc.) that are built on top of it are likely to offer no security at all. Lightweight symmetric-key primitives, in particular, will play a critical role.The security of protocols is frequently verified using formal and automated methods. Concerning algorithms and public-key primitives, formal proofs are often used, although they are somewhat error prone and current efforts aim to automate them. On the other hand, symmetric-key primitives are still currently analysed in a rather ad-hoc manner. Since their security is only guaranteed by the test-of-time, they traditionally have a built-in security margin. Despite being paramount to the security of embedded devices, lightweight primitives appear to have a smaller security margin and researchers would greatly benefit from automated tools in order to strengthen tests-of-time.In their seminal work back in 2000, Massacci and Marraro proposed to formulate primitives in propositional logic and to use SAT solvers to automatically verify their properties. At that time, SAT solvers were quite different from what they have become today; the continuous improvement of their performance makes them an even better choice for a verification back-end. The performance of SAT solvers improved so much that starting around 2006, some cryptanalysts started to use them, but mostly in order to speedup their attacks. This thesis introduces the framework CryptoSAT and shows its advantages for the purpose of verification. / La sécurité informatique repose en majeure partie sur des mécanismes cryptographiques, qui à leur tour dépendent de composants encore plus fondamentaux appelés primitives ;si une primitive échoue, toute la sécurité qui en dépend est vouée à l'échec. Les ordinateurs ont atteint un coût et un degré de miniaturisation propices à leur prolifération sous forme de systèmes embarqués (ou enfouis) qui offrent généralement peu de ressources calculatoires, notamment dans des environnements où la sécurité est primordiale. Leur sécurité repose donc lourdement sur les primitives dites à clé symétrique, puisque ce sont celles qui sont le mieux adaptées aux ressources limitées dont disposent les systèmes embarqués. Il n'est pas mathématiquement prouvé que les primitives à clé symétrique soient dépourvues de failles de sécurité, contrairement à tous les autres mécanismes cryptographiques :alors que la protection qu'offre la cryptographie peut, en général, être prouvée de façon formelle (dans un modèle limité) et parfois au moyen de méthodes automatisées qui laissent peu de place à l'erreur, la protection qu'offrent les primitives à clé symétrique n'est garantie que par “l'épreuve du temps”, c.-à-d. par la résistance (durable) de ces primitives face aux attaques conçues par la communauté des chercheurs en cryptologie. Pour compenser l'absence de garanties formelles, ces primitives sont traditionnellement pourvues d'une “marge de sécurité”, c.-à-d. de calculs supplémentaires, juste au cas où, dont le coût est difficile à justifier lorsque les ressources calculatoires sont rares.Afin de pallier à l'insuffisance de l'épreuve du temps et à la diminution des marges de sécurité, cette thèse revient sur les travaux de Massacci et Marraro qui, en 2000, avaient proposé de formuler les primitives en logique propositionnelle de sorte que leurs propriétés puissent être vérifiées automatiquement au moyen d'algorithmes SAT. A cette époque, les algorithmes SAT étaient très différents de ce qu'ils sont devenus aujourd'hui ;l'amélioration de leur performance, continuelle au fil des années, en fait un choix encore plus judicieux comme moteur de vérification. Dans le cadre de cette thèse, une méthode a été développée pour permettre à un cryptologue de facilement vérifier les propriétés d'une primitive à clé symétrique de façon formelle et automatique à l'aide d'algorithmes SAT, tout en lui permettant de faire abstraction de la logique propositionnelle. L'utilité de la méthode a ensuite été mise en évidence en obtenant des réponses formelles à des questions, posées dans la littérature en cryptanalyse, concernant des failles potentielles tant au niveau de la conception qu'au niveau de la mise en oeuvre de certaines primitives. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

The Boolean satisfiability (SAT) problem is central to many applications involving the verification and optimization of digital systems. These combinatorial problems are typically solved by using a decision-based approach, however the lengthy compute time of SAT can make it prohibitively impractical for some applications. We discuss how the underlying physical characteristics of various technologies affect the practicality of SAT solvers. Power dissipation and other physical limitations are increasingly restricting the improvement in performance of conventional software on CPUs. We use heterogeneous computing to maximize the strengths of different underlying technologies as well as different computing architectures. In this thesis, we present a custom hardware architecture for accelerating the common computation within a SAT solver. Algorithms and data structures must be fundamentally redesigned in order to maximize the strengths of customized computing. Generalizable optimizations are proposed to maximize the throughput, minimize communication latencies, and aggressively compact the memory. We tightly integrate as well as jointly optimize the hardware accelerator and the software host. Our fully implemented system is significantly faster than pure software on real-life SAT problems. Due to our insights and optimizations, we are able to benchmark SAT in uncharted territory. / Thesis / Doctor of Philosophy (PhD)

Boolean Satisfiability (SAT) is a fundamental NP-complete problem of determining whether there exists an assignment of variables which makes a Boolean formula evaluate to True. SAT is a convenient representation for many naturally occurring optimization and decisions problems such as planning and circuit verification. SAT is most commonly solved by a form of backtracking search which systematically explores the space of possible variable assignments. We show that the order in which variable polarities are assigned can have a significant impact on the performance of backtracking algorithms. We present several ways of transforming SAT instances into non-linear objective functions and describe three value-ordering methods based on iterative optimization techniques. We implement and test these heuristics in the widely-recognized MiniSAT framework. The first approach determines polarities by applying Newton's Method to a sparse system of non-linear objective functions whose roots correspond to the satisfying assignments of the propositional formula. The second approach determines polarities by minimizing an objective function corresponding to the number of clauses conflicting with each assignment. The third approach determines preferred polarities by performing stochastic gradient descent on objective functions sampled from a family of continuous potentials. The heuristics are evaluated on a set of standard benchmarks including random, crafted and industrial problems. We compare our results to five existing heuristics, and show that MiniSAT equipped with our heuristics often outperforms state-of-the-art SAT solvers.

In the quest to understand cell behavior and cure genetic diseases such as cancer, the fundamental approach being taken is undergoing a gradual change. It is becoming more acceptable to view these diseases as an engineering problem, and systems engineering approaches are being deployed to tackle genetic diseases. In this light, we believe that logic synthesis techniques can play a very important role. Several techniques from the field of logic synthesis can be adapted to assist in the arguably huge effort of modeling cell behavior, inferring biological networks, and controlling genetic diseases. Genes interact with other genes in a Gene Regulatory Network (GRN) and can be modeled as a Boolean Network (BN) or equivalently as a Finite State Machine (FSM). As the expression of genes deter- mine cell behavior, important problems include (i) inferring the GRN from observed gene expression data from biological measurements, and (ii) using the inferred GRN to explain how genetic diseases occur and determine the ”best” therapy towards treatment of disease. We report results on the application of logic synthesis techniques that we have developed to address both these problems. In the first technique, we present Boolean Satisfiability (SAT) based approaches to infer the predictor (logical support) of each gene that regulates melanoma, using gene expression data from patients who are suffering from the disease. From the output of such a tool, biologists can construct targeted experiments to understand the logic functions that regulate a particular target gene. Our second technique builds upon the first, in which we use a logic synthesis technique; implemented using SAT, to determine gene regulating functions for predictors and gene expression data. This technique determines a BN (or family of BNs) to describe the GRN and is validated on a synthetic network and the p53 network. The first two techniques assume binary valued gene expression data. In the third technique, we utilize continuous (analog) expression data, and present an algorithm to infer and rank predictors using modified Zhegalkin polynomials. We demonstrate our method to rank predictors for genes in the mutated mammalian and melanoma networks. The final technique assumes that the GRN is known, and uses weighted partial Max-SAT (WPMS) towards cancer therapy. In this technique, the GRN is assumed to be known. Cancer is modeled using a stuck-at fault model, and ATPG techniques are used to characterize genes leading to cancer and select drugs to treat cancer. To steer the GRN state towards a desirable healthy state, the optimal selection of drugs is formulated using WPMS. Our techniques can be used to find a set of drugs with the least side-effects, and is demonstrated in the context of growth factor pathways for colon cancer.

In this thesis, we have considered two important problems, Boolean satisfiability (SAT) and derivative free optimization in the context of large scale quantum computers. In the first part, we survey well known classical techniques for solving satisfiability. We compute the approximate time it would take to solve SAT instances using quantum techniques and compare it with state-of-the heart classical heuristics employed annually in SAT competitions. In the second part of the thesis, we consider a few classically well known algorithms for derivative free optimization which are ubiquitously employed in engineering problems. We propose a quantum speedup to this classical algorithm by using techniques of the quantum minimum finding algorithm. In the third part of the thesis, we consider practical applications in the fields of bio-informatics, petroleum refineries and civil engineering which involve solving either satisfiability or derivative free optimization. We investigate if using known quantum techniques to speedup these algorithms directly translate to the benefit of industries which invest in technology to solve these problems. In the last section, we propose a few open problems which we feel are immediate hurdles, either from an algorithmic or architecture perspective to getting a convincing speedup for the practical problems considered.

Boolean Satisfiability (SAT) is a fundamental NP-complete problem of determining whether there exists an assignment of variables which makes a Boolean formula evaluate to True. SAT is a convenient representation for many naturally occurring optimization and decisions problems such as planning and circuit verification. SAT is most commonly solved by a form of backtracking search which systematically explores the space of possible variable assignments. We show that the order in which variable polarities are assigned can have a significant impact on the performance of backtracking algorithms. We present several ways of transforming SAT instances into non-linear objective functions and describe three value-ordering methods based on iterative optimization techniques. We implement and test these heuristics in the widely-recognized MiniSAT framework. The first approach determines polarities by applying Newton's Method to a sparse system of non-linear objective functions whose roots correspond to the satisfying assignments of the propositional formula. The second approach determines polarities by minimizing an objective function corresponding to the number of clauses conflicting with each assignment. The third approach determines preferred polarities by performing stochastic gradient descent on objective functions sampled from a family of continuous potentials. The heuristics are evaluated on a set of standard benchmarks including random, crafted and industrial problems. We compare our results to five existing heuristics, and show that MiniSAT equipped with our heuristics often outperforms state-of-the-art SAT solvers.

The memory cells used in modern field programmable gate arrays (FPGAs) are highly susceptible to single event upsets (SEUs). The typical mitigation strategy in the industry is some form of hardware redundancy in the form of duplication with comparison (DWC) or triple modular redundancy (TMR). While this strategy is highly effective in masking out the effect of faults, it incurs a large hardware cost. In this thesis, we explore a different approach to hardware redundancy. The core idea of our approach is to exploit the conflict-driven clause learning (CDCL) mechanism in modern Boolean satisfiability (SAT) solvers to provide us with invariants which can be realized as hardware checkers. Furthermore, we develop the algorithms required to select a subset of these invariants to be included as part of a checker circuit. This checker circuit then augments the original FPGA design. We find which look-up table (LUT) memory cells are sensitive to bitflips, then we automatically generate a checker circuit consisting of hardware invariants targeted towards those faults. We aim to reach 100% coverage of sensitizable faults. After extensive experimentation, we conclude that this approach is not competitive with DWC with respect to hardware area. However, we demonstrate that many bitflips will have reduced a detection latency compared to DWC. / Thesis / Master of Applied Science (MASc)