The thesis addresses the 'algorithm configuration problem,' focusing on optimizing algorithm parameters to enhance performance across various domains, such as electricity auctions, production, and transportation. Efficiently solving multiple instances of the same optimization problem is crucial, and the algorithms' performance is significantly influenced by their parameter settings. Research into algorithm configuration has grown substantially over the past two decades, with techniques such as ParamILS, SMAC, and racing algorithms emerging to find optimal parameter configurations. These methods often use a 'one-size-fits-all' approach, which may not be effective for heterogeneous problem instances requiring different configurations. Therefore, the first research question (RQ1) investigates how to mathematically define and formulate the multi-objective, instance-specific algorithm configuration problem. An advanced approach is 'instance-specific configuration,' which optimizes parameters based on the unique features of each problem instance. This leads to the second research question (RQ2): assessing the current state of research in algorithm configuration, identifying research gaps, and structuring the field. The thesis proposes a new framework called MO-SMAC that integrates multiple objectives and instance features into the algorithm configuration process. This framework aims to move beyond generic solutions by providing tailored configurations for each instance. A case study involving the Capacitated Vehicle Routing Problem (CVRP) and Genetic Algorithms (GAs) explores this approach. This leads to the third research question (RQ3): applying the generic configuration formulation to a concrete case study and defining the corresponding instance and configuration spaces. The thesis also emphasizes the need for a systematic experimental methodology. The fourth research question (RQ4) addresses this by proposing a Design of Experiments (DoE) approach to identify the most influential configuration parameters and their interactions with instance features. RQ5 specifically investigates the most influential factors in the algorithm configuration process and examines whether interactions exist between these factors. The DoE methodology aims to systematically assess the impact of individual parameters and instance features on algorithm performance, using screening to identify significant factors, ranking to determine their importance, and exploring interactions. Another key focus is understanding the trade-offs between competing performance objectives (RQ6), such as solution quality versus runtime. This question explores how specific configuration parameters impact these trade-offs and provides insights into balancing multiple objectives to achieve optimal performance for specific problem instances. RQ7 examines the benefits of incorporating instance features into the algorithm configuration process. It seeks to determine whether considering these features leads to better-performing configurations by tailoring them to each instance's unique characteristics, thereby improving performance and robustness compared to generalized approaches. Finally, RQ8 explores the generalizability of results from offline training and assesses how well various configurators perform in online scenarios. It investigates whether configurations optimized offline can maintain their effectiveness when applied to new, unseen instances, addressing the need for unbiased evaluation and emphasizing the importance of generalizability to prevent overfitting and overspecialization. In conclusion, the thesis aims to develop a multi-objective, instance-specific algorithm configuration framework that balances competing performance goals and leverages instance features for improved results. It challenges the 'one-size-fits-all' approach by offering tailored configurations for specific problem instances and highlights the need for systematic experimentation to understand trade-offs and ensure generalizability in the configuration process.:List of Figures List of Tables List of Abbreviations List of Symbols I Problem description 1 Introduction 2 The multi-objective instance-specific algorithm configuration problem 2.1 Formal statement 2.2 Excursus: possible algorithm performance metrics 2.3 Conclusion 3 Literature review 3.1 Algorithm selection 3.2 Parameter tuning and parameter control 3.2.1 Non-iterative parameter-tuning strategies 3.2.2 Iterative parameter-tuning strategies 3.2.3 Parameter control strategies 3.3 Gaining insights into instance hardness and algorithm performance 3.4 Benchmark generation 3.5 Conclusion II Case study 4 Case study 4.1 Formal statement of the optimization problem 4.2 The CVRP instance feature space F 4.3 The GA configuration space Θ 4.4 Conclusion 5 Experimental planning 5.1 Design of experiments 5.1.1 Practical methodology for DoE 5.1.2 Experimental designs 5.2 Instance space 5.2.1 Starting from a state-of-the-art benchmark set 5.2.2 Investigated instance features 5.2.3 Instance generation 5.3 Configuration space 5.4 Conclusion III Instance-oblivious algorithm configuration 6 Generalist 6.1 General methodology 6.2 Non-parametric tests 6.2.1 Single-objective ranking 6.2.2 Multi-objective ranking 6.3 Surrogate models 6.3.1 Linear regression 6.3.2 Shrinkage methods 6.3.3 Regression trees 6.4 Conclusion 7 Experiment: generalist 7.1 Planning 7.1.1 Instance space 7.1.2 Configuration space 7.2 Designing 7.2.1 Instance space 7.2.2 Configuration space 7.3 Conducting 7.4 Analyzing: non-parametric statistics 7.4.1 Single-objective parameter level rankings 7.4.2 Multi-objective rankings of configuration 7.5 Analyzing: Surrogate models 7.5.1 Data pre-processing 7.5.2 Performance metrics 7.5.3 Linear forward regression 7.5.4 Shrinkage 7.5.5 Regression tree 7.5.6 Pareto fronts 7.6 Evaluation 7.7 Conclusion IV Instance-specific algorithm configuration 8 Specialist 8.1 Bayesian optimization 8.2 Multi-Objective Instance-Specific Model-based algorithm configuration 8.2.1 General outline 8.2.2 Clustering 8.2.3 Acquisition function: expected hypervolume improvement 8.2.4 Candidate selection 8.2.5 Intensification 8.3 Surrogate models 8.3.1 Random forest 8.3.2 Gaussian process regression 8.4 Conclusion 9 Experiment: specialist 9.1 Planning 9.1.1 Initialization phase 9.1.2 Improvement phase 9.2 Designing 9.3 Conducting 9.4 Analyzing 9.4.1 Performance metrics 9.4.2 Surrogate models 9.5 Evaluation 9.6 Conclusion V Conclusion 10 Conclusion Bibliography

La génération de stratégies pour les solveurs en Satisfiabilité Modulo des Théories (SMT) nécessite des outils théoriques et pratiques qui permettent aux utilisateurs d’exercer un contrôle stratégique sur les aspects heuristiques fondamentaux des solveurs de SMT, tout en garantissant leur performance. Nous nous intéressons dans cette thèse au solveur Z3 , l’un des plus efficaces lors des compétitions SMT (SMT-COMP). Dans les solveurs SMT, la définition d’une stratégie repose sur un ensemble de composants et paramètres pouvant être agencés et configurés afin de guider la recherche d’une preuve de (in)satisfiabilité d’une instance donnée. Dans cette thèse, nous abordons ce défi en définissant un cadre pour la génération autonome de stratégies pour Z3, c’est-à-dire un algorithme qui permet de construire automatiquement des stratégies sans faire appel à des connaissances d’expertes. Ce cadre général utilise une approche évolutionnaire (programmation génétique), incluant un système à base de règles. Ces règles formalisent la modification de stratégies par des principes de réécriture, les algorithmes évolutionnaires servant de moteur pour les appliquer. Cette couche intermédiaire permettra d’appliquer n’importe quel algorithme ou opérateur sans qu’il soit nécessaire de modifier sa structure, afin d’introduire de nouvelles informations sur les stratégies. Des expérimentations sont menées sur les jeux classiques de la compétition SMT-COMP. / The Strategy Challenge in Satisfiability Modulo Theories (SMT) claims to build theoretical and practical tools allowing users to exert strategic control over core heuristic aspects of high-performance SMT solvers. In this work, we focus in Z3 Theorem Prover: one of the most efficient SMT solver according to the SMT Competition, SMT-COMP. In SMT solvers, the definition of a strategy relies on a set of tools that can be scheduled and configured in order to guide the search for a (un)satisfiability proof of a given instance. In this thesis, we address the Strategy Challenge in SMT defining a framework for the autonomous generation of strategies in Z3, i.e. a practical system to automatically generate SMT strategies without the use of expert knowledge. This framework is applied through an incremental evolutionary approach starting from basic algorithms to more complex genetic constructions. This framework formalise strategies modification as rewriting rules, where algorithms acts as enginess to apply them. This intermediate layer, will allow apply any algorithm or operator with no need to being structurally modified, in order to introduce new information in strategies. Validation is done through experiments on classic benchmarks of the SMT-COMP.