The Algorithm Selection Problem is to select the most appropriate way for solving a problem given a choice of different ways. Some of the most prominent and successful applications come from Artificial Intelligence and in particular combinatorial search problems. Machine Learning has established itself as the de facto way of tackling the Algorithm Selection Problem. Yet even after a decade of intensive research, there are no established guidelines as to what kind of Machine Learning to use and how. This dissertation presents an overview of the field of Algorithm Selection and associated research and highlights the fundamental questions left open and problems facing practitioners. In a series of case studies, it underlines the difficulty of doing Algorithm Selection in practice and tackles issues related to this. The case studies apply Algorithm Selection techniques to new problem domains and show how to achieve significant performance improvements. Lazy learning in constraint solving and the implementation of the alldifferent constraint are the areas in which we improve on the performance of current state of the art systems. The case studies furthermore provide empirical evidence for the effectiveness of using the misclassification penalty as an input to Machine Learning. After having established the difficulty, we present an effective technique for reducing it. Machine Learning ensembles are a way of reducing the background knowledge and experimentation required from the researcher while increasing the robustness of the system. Ensembles do not only decrease the difficulty, but can also increase the performance of Algorithm Selection systems. They are used to much the same ends in Machine Learning itself. We finally tackle one of the great remaining challenges of Algorithm Selection -- which Machine Learning technique to use in practice. Through a large-scale empirical evaluation on diverse data taken from Algorithm Selection applications in the literature, we establish recommendations for Machine Learning algorithms that are likely to perform well in Algorithm Selection for combinatorial search problems. The recommendations are based on strong empirical evidence and additional statistical simulations. The research presented in this dissertation significantly reduces the knowledge threshold for researchers who want to perform Algorithm Selection in practice. It makes major contributions to the field of Algorithm Selection by investigating fundamental issues that have been largely ignored by the research community so far.

Service-oriented computing is a popular technology that facilitates the development of large-scale distributed systems. However, the modular composition and flexible coordination of such applications still remains challenging for the following reasons: 1) the services are provided as loosely coupled black boxes that only expose their interfaces to the environment; 2) interacting services are not usually known in advance: web services are dynamically chosen to fulfil certain roles and are often replaced by services with a similar functionality; 3) the nature of the service-based application is decentralised. Loose coupling of web services is often lost when it comes to the construction of an application from services. The reason is that the object-oriented paradigm, which is widely used in the implementation of web services, does not provide a mechanism for service interface self-tuning. As a result, it negatively impacts upon the interoperability of web services. In this dissertation we present a formal method for automatic service configuration in the presence of subtyping, polymorphism, and flow inheritance. This is a challenging problem. On the one hand, the interface description language must be flexible enough to maintain service compatibility in various contexts without any modification to the service itself. On the other hand, the composition of interfaces in a distributed environment must be provably consistent. Our method is based on constraint satisfaction and Boolean satisfiability. First, we define a language for specifying service interfaces in a generic form, which is compatible with a variety of contexts. The language provides support for parametric polymorphism, Boolean variables, which are used to control dependencies between any elements of interface collections, and flow inheritance using extensible records and variants. We implemented the method as a constraint satisfaction solver. In addition to this, we present a protocol for interface configuration. It specifies a sequence of steps that leads to the generation of context-specific service libraries from generic services. Furthermore, we developed a toolchain that performs a complete interface configuration for services written in C++. We integrated support for flexible interface objects (i.e. objects that can be transferred in the application along with their structural description). Although the protocol relies solely on interfaces and does not take behaviour concerns into account, it is capable of finding discrepancies between input and output interfaces for simple stateful services, which only perform message synchronisation. Two running examples (a three buyers use-case and an image processing application) are used along the way to illustrate our approach. Our results seem to be useful for service providers that run their services in the cloud. The reason is twofold. Firstly, interfaces and the code behind them can be generic as long as they are sufficiently configurable. No communication between service designers is necessary in order to ensure consistency in the design. Instead, the interface correspondence in the application is ensured by the constraint satisfaction algorithm, which we have already designed. Secondly, the configuration and compilation of every service are separated from the rest of the application. This prevents source code leaks in proprietary software which is running in the cloud.

Made available in DSpace on 2016-04-27T17:27:13Z (GMT). No. of bitstreams: 1 Carlos Roberto Teixeira Alves.pdf: 1331347 bytes, checksum: cebe03a83120937101a3595710844df2 (MD5) Previous issue date: 2015-12-14 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work aims to show the current treatment of the semantic notion of satisfiability to the logic of the first order, the relevant problems of Tarski's solution to define this notion - in this case, the use of infinite sequences to satisfy the formulas - and propose an alternative to circumvent this problem. The notion established by Tarski became, in discussions on the subject, standard solution and resulted in rich tools to work with the languages, in particular tools such as the Theory of Models. However, from a philosophical point of view, it is very important to broaden perspectives and look at the problem from a new dimension. Our proposal is to avoid the counterintuitive idea of using infinite sequences of objects to satisfy the finite formulas, knowing that these infinite sequences are composed almost entirely of 'superfluous terms', expendable in the process of satisfaction, but they should and are listed and indexed in the process. It would be interesting to solve the issue involving sequences without 'superfluous terms'. We propose a structure of first-order language that dispenses variables and constants. The notion of satisfaction in this case is distinct, which increases the possibilities and provides an alternative to the satisfaction of infinite sequences. In the end, we show how our solution can produce the satisfaction of formulas of a first-order language within a framework where satisfaction is interpreted according to certain specific criteria and can be performed by finite sequences, differing essentially from Tarski solution / Este trabalho tem por objetivo mostrar o tratamento atual da noção semântica de satisfatibilidade para as lógicas de primeira ordem, os problemas relevantes da solução de Tarski para definir essa noção no caso, o uso de sequências infinitas para a satisfação das fórmulas , e propor uma alternativa que contorne esse problema. A noção estabelecida por Tarski tornou-se, nas discussões a respeito do tema, a solução padrão e resultou em ferramentas ricas para operar com as linguagens, em especial ferramentas como a Teoria dos Modelos. No entanto, de um ponto de vista filosófico, é sadio ampliar as perspectivas e olhar o problema sob uma dimensão nova. Nossa proposta é superar a ideia contraintuitiva de elencarmos sequências infinitas de objetos para satisfação das formulas finitas, sabendo que essas sequências infinitas são compostas quase que totalmente de termos supérfluos , dispensáveis no processo de satisfação, mas que devem e são enumerados e indexados no processo. Seria interessante solucionar a questão envolvendo sequências sem termos supérfluos . Proporemos uma estrutura de linguagem de primeira ordem que dispensa variáveis e constantes. A noção de satisfação nesse caso é distinta, o que amplia as possibilidades e fornece uma alternativa à satisfação por sequências infinitas. No fim, mostraremos como nossa solução consegue produzir a satisfação de fórmulas de uma linguagem de primeira ordem dentro de uma estrutura interpretada onde a satisfação ocorre segundo certos critérios específicos e consegue ser realizada por sequências finitas, diferindo essencialmente da solução de Tarski

ASICs estruturados com leiautes regulares representam uma das soluções para a perda de rendimento de fabricação de circuitos integrados em tecnologias nanométricas causada pela distorção de fotolitografia. Um método de projeto de circuitos integrados ainda mais restritivo resulta em ASICs estruturados configuráveis apenas pelas camadas de vias, que são compostos pela repetição do mesmo modelo de bloco em todas as camadas do leiaute, exceto as camadas de vias. A escolha do modelo de bloco tem grande influência nas características do circuito final, criando a demanda por novas ferramentas de CAD que possam avaliar e comparar tais modelos em seus diversos aspectos. Esta tese descreve um ambiente de CAD baseado em SAT, capaz de avaliar o aspecto de capacidade lógica em padrões de blocos configuráveis por vias. O ambiente proposto é genérico, podendo tratar quaisquer padrões de bloco definido pelo usuário, e se comporta de maneira eficiente quando aplicado aos principais padrões já publicados na literatura. / Structured ASICs with regular layouts comprise a design-based solution for IC manufacturing yield loss in nanometer technologies caused by photolithography distortions. Via-configurable structured ASICs is even a more restrictive digital IC design method, based on the repetition of a block template comprising all layout layers except the vias one. The choice of such a design strategy impacts greatly the final circuit characteristics, arising the need for specific CAD tools to allow template evaluation and comparison in different aspects. This work presents a SAT-based CAD environment for evaluating the logical capacity aspect of via-configurable block templates. The proposed environment is able to support any user-defined template, and behaves efficiently when applied to block templates presented in related literature.

Formal verification techniques are growing increasingly vital for the development of safety-critical software and hardware in practice. Techniques such as requirements-based design and model checking for system verification have been successfully used to verify systems for air traffic control, airplane separation assurance, autopilots, CPU logic designs, life-support, medical equipment, and other functions that ensure human safety. Formal behavioral specifications written early in the system-design process and communicated across all design phases increase the efficiency, consistency, and quality of the system under development. We argue that to prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. We advocate for the adaptation of a new sanity check via satisfiability checking for property assurance. Our focus here is on specifications expressed in Linear Temporal Logic (LTL). We demonstrate that LTL satisfiability checking reduces to model checking and satisfiability checking for the specification, its complement, and a conjunction of all properties should be performed as a first step to LTL model checking. We report on an experimental investigation of LTL satisfiability checking. We introduce a large set of rigorous benchmarks to enable objective evaluation of LTL-to-automaton algorithms in terms of scalability, performance, correctness, and size of the automata produced. For explicit model checking, we use the Spin model checker; we tested all LTL-to-explicit automaton translation tools that were publicly available when we conducted our study. For symbolic model checking, we use CadenceSMV, NuSMV, and SAL-SMC for both LTL-to-symbolic automaton translation and to perform the satisfiability check. Our experiments result in two major findings. First, scalability, correctness, and other debilitating performance issues afflict most LTL translation tools. Second, for LTL satisfiability checking, the symbolic approach is clearly superior to the explicit approach. Ironically, the explicit approach to LTL-to-automata had been heavily studied while only one algorithm existed for LTL-to-symbolic automata. Since 1994, there had been essentially no new progress in encoding symbolic automata for BDD-based analysis. Therefore, we introduce a set of 30 symbolic automata encodings. The set consists of novel combinations of existing constructs, such as different LTL formula normal forms, with a novel transition-labeled symbolic automaton form, a new way to encode transitions, and new BDD variable orders based on algorithms for tree decomposition of graphs. An extensive set of experiments demonstrates that these encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking. Building upon these ideas, we return to the explicit automata domain and focus on the most common type of specifications used in industrial practice: safety properties. We show that we can exploit the inherent determinism of safety properties to create a set of 26 explicit automata encodings comprised of novel aspects including: state numbers versus state labels versus a state look-up table, finite versus infinite acceptance conditions, forward-looking versus backward-looking transition encodings, assignment-based versus BDD-based alphabet representation, state and transition minimization, edge abbreviation, trap-state elimination, and determinization either on-the-fly or up-front using the subset construction. We conduct an extensive experimental evaluation and identify an encoding that offers the best performance in explicit LTL model checking time and is constantly faster than the previous best explicit automaton encoding algorithm.

Στην εργασία αυτή ασχοληθήκαμε με το πρόβλημα της Πιθανοτικής Ικανοποιησιμότητας. Παρουσιάσαμε ανάλυση της πολυπλοκότητας του προβλήματος και το επιλύσαμε με την βοήθεια του λογισμικού πακέτου CPLEX. Περιγράψαμε προσεγγιστικούς αλγόριθμους για το πρόβλημα της Μέγιστης Ικανοποιησιμότητας που χρησιμοποιείται στην διαδικασία της Column Generation. Τέλος, πριγράψαμε το αντίστροφο πρόβλημα των συχνών στοιχειοσυνόλων και την σχέση του με το πρόβλημα της Μέγιστης Ικανοποιησιμότητας. / This thesis is about the problem of probabilistic satisfiability. We describe its computational complexity, we solve the problem using CPLEX, we discribe some approximations on Maximum Satisfiability. Finally, we describe the connection between the problem of Probabilistic Satisfiability and the inverse frequent itemset mining.

No description available.

This thesis is divided into two parts. In the first part we describe a new Monte Carlo algorithm for the consistent and unbiased estimation of multidimensional integrals and the efficient sampling from multidimensional densities. The algorithm is inspired by the classical splitting method and can be applied to general static simulation models. We provide examples from rare-event probability estimation, counting, optimization, and sampling, demonstrating that the proposed method can outperform existing Markov chain sampling methods in terms of convergence speed and accuracy. In the second part we present a new adaptive kernel density estimator based on linear diffusion processes. The proposed estimator builds on existing ideas for adaptive smoothing by incorporating information from a pilot density estimate. In addition, we propose a new plug-in bandwidth selection method that is free from the arbitrary normal reference rules used by existing methods. We present simulation examples in which the proposed approach outperforms existing methods in terms of accuracy and reliability.

In this thesis we study Boolean functions from three different perspectives. First, we study the complex- ity of Boolean minimization for several classes of formulas with polynomially solvable SAT, and formulate sufficient conditions for a class which cause the minimization problem to drop at least one level in the polyno- mial hierarchy. Second, we study a class of matched CNFs for which SAT is trivial but minimization remains Σp 2 complete. We prove that every matched CNF has at least one equivalent prime and irredundant CNF that is also matched. We use this fact to prove the main result of this part, namely that for every matched CNF all clause minimal equivalent CNFs are also matched. Third, we look at propagation completeness - the property of a CNF that says that for every partial assignment all entailed literals can be discovered by unit propagation. We can extend every CNF to be propagation complete by adding empowering impli- cates to it. The main result of this section is a the proof of coNP completeness of the recognition problem for propagation complete CNFs. We also show that there exist CNFs to which an exponential number of empowering implicates have to be added to make them propagation complete.

Le développement de circuits électroniques et de systèmes logiciels critiques pour le ferroviaire ou l’avionique, par exemple, demande à être systématiquement associé à un processus de vérification formelle permettant de garantir l’exhaustivité des tests. L’approche formelle la plus répandue dans l’industrie est le Model Checking. Le succès de son adoption provient de deux caractéristiques : (i) son aspect automatique, (ii) sa capacité à produire un témoin (un scénario rejouable) lorsqu’un comportement indésirable est détecté, ce qui fournit une grande aide aux concepteurs pour corriger le problème. Néanmoins, la complexité grandissante des systèmes à vérifier est un réel défi pour le passage à l’échelle des techniques existantes. Pour y remédier, différents algorithmes de model checking (e.g., parcours symbolique des états du système, interpolation), diverses méthodes complémentaires (e.g., abstraction,génération automatique d’invariants), et de multiples procédures de décision(e.g., diagramme de décision, solveur SMT) sont envisageables.Dans cette thèse, nous nous intéressons plus particulièrement à l’induction temporelle.Il s’agit d’un algorithme de model checking très utilisé dans l’industrie pour vérifier les systèmes critiques. C’est également l’algorithme principal de l’outil développé au sein de l’entreprise Safe River, entreprise dans laquelle cette thèse a été effectuée. Plus précisément, l’induction temporelle combine deux techniques :(i) BMC (Bounded Model Checking), une méthode très efficace pour la détection debugs dans un système (ii) k-induction, une méthode ajoutant un critère de terminaison à BMC lorsque le système n’admet pas de bug. Ces deux techniques génèrent des formules logiques propositionnelles pour lesquelles il faut en déterminer la satisfaisabilité.Pour se faire, nous utilisons un solveur SAT, c’est-à-dire une procédure de décision qui détermine si une telle formule admet une solution.L’originalité des travaux proposés dans cette thèse repose en grande partie sur la volonté de renforcer la collaboration entre le solveur SAT et le model checker.Nos efforts visent à accroître l’interconnexion de ces deux modules en exploitant la structure haut niveau du problème. Nous avons alors défini des méthodes profitant de la structure symétrique des formules. Cette structure apparaît lors du dépliage successif de la relation de transition, et nous permet de dupliquer les clauses ou encore de déplier les transitions dans différentes directions (i.e., avant ou arrière). Nous avons aussi pu instaurer une communication entre le solveur SAT et le model checker permettant de : (i) simplifier la représentation au niveau du model checker grâce à des informations déduites par le solveur, et (ii) aider le solveur lors de la résolution grâce aux simplifications effectuées sur la représentation haut niveau. Une autre contribution importante de cette thèse est l’expérimentation des algorithmes proposées. Cela se concrétise par l’implémentation d’un model checker prenant en entrée des modèles AIG (And-Inverter Graph) dans lequel nous avons pu évaluer l’efficacité de nos différentes méthodes. / The design of electronic circuits and safety-critical software systems in railway or avionic domains for instance, is usually associated with a formal verification process. More precisely, test methods for which it is hard to show completeness are combined with approaches that are complete by definition. Model Checking is one of those approaches and is probably the most prevalent in industry. Reasons of its success are mainly due to two characteristics, namely: (i) its fully automatic aspect, and (ii) its ability to produce a short execution trace of undesired behaviors, which is very helpful for designers to fix the issues. However, the increasing complexity of systems to be verified is a real challenge for the scalability of existing techniques. To tackle this challenge, different model checking algorithms (e.g., symbolic model checking, interpolation), various complementary methods (e.g., abstraction, automatic generation of invariants) and multiple decision procedures (e.g., decision diagram, SMT solver) can be considered. In this thesis, we particularly focus on temporal induction. It is a model checking algorithm widely used in the industry to check safety-critical systems. This is also the core algorithm of the tool developed within SafeRiver, company in which this thesis was carried out. More precisely, temporal induction consists of a combination of BMC (Bounded Model Checking) and k-induction. BMC is a very efficient bugfinding method. While k-induction adds a termination criterion to BMC when the system does not admit bugs. These two techniques generate formulas for which it is necessary to determine their satisfiability. To this end, we use a SAT solver as a decision procedure to determine whether a propositional formula has a solution. The main contribution of this thesis aims to strengthen the collaboration between the SAT solver and the model checker. The improvements proposed mainly focus on increasing the interconnections of these two modules by exploiting the high-level structure of the problem.We have therefore defined several methods taking advantage of the symmetrical structure of the formulas. This structure emerges during the successive unfolding of the transition relation, and allows us to duplicate clauses or even unroll the transitions in different directions (i.e., forward or backward). We also established a communication between the solver and the model checker, which has for purpose to: (i) simplify the model checker representation using the information inferred by the solver, and (ii) assist the solver during resolution with simplifications performed on the high-level representation. Another important contribution of this thesis is the empirical evaluation of the proposed algorithms on well-established benchmarks. This is achieved concretely via the implementation of a model checker taking AIG (And-Inverter Graph) as input, from which we were able to evaluate the effectiveness of our algorithms.