Recent research has shown that it is often preferable to encode real-world problems as propositional satisfiability (SAT) problems and then solve using a general purpose SAT solver. However, much of the valuable information and structure of these realistic problems is flattened out and hidden inside the corresponding Conjunctive Normal Form (CNF) encodings of the SAT domain. Recently, systematic SAT solvers have been progressively improved and are now able to solve many highly structured practical problems containing millions of clauses. In contrast, state-of-the-art Stochastic Local Search (SLS) solvers still have difficulty in solving structured problems, apparently because they are unable to exploit hidden structure as well as the systematic solvers. In this thesis, we study and evaluate different ways to effectively recognise, model and efficiently exploit useful structures hidden in realistic problems. A summary of the main contributions is as follows: 1. We first investigate an off-line processing phase that applies resolution-based pre-processors to input formulas before running SLS solvers on these problems. We report an extensive empirical examination of the impact of SAT pre-processing on the performance of contemporary SLS techniques. It emerges that while all the solvers examined do indeed benefit from pre-processing, the effects of different pre-processors are far from uniform across solvers and across problems. Our results suggest that SLS solvers need to be equipped with multiple pre-processors if they are ever to match the performance of systematic solvers on highly structured problems. [Part of this study was published at the AAAI-05 conference]. 2. We then look at potential approaches to bridging the gap between SAT and constraint satisfaction problem (CSP) formalisms. One approach has been to develop a many-valued SAT formalism (MV-SAT) as an intermediate paradigm between SAT and CSP, and then to translate existing highly efficient SAT solvers to the MV-SAT domain. In this study, we follow a different route, developing SAT solvers that can automatically recognise CSP structure hidden in SAT encodings. This allows us to look more closely at how constraint weighting can be implemented in the SAT and CSP domains. Our experimental results show that a SAT-based mechanism to handle weights, together with a CSP-based method to instantiate variables, is superior to other combinations of SAT and CSP-based approaches. In addition, SLS solvers based on this many-valued weighting approach outperform other existing approaches to handle many-valued CSP structures. [Part of this study was published at the AAAI-05 conference]. 3. Finally, we propose and evaluate six different schemes to encode temporal reasoning problems, in particular the Interval Algebra (IA) networks, into SAT CNF formulas. We then empirically examine the performance of local search as well as systematic solvers on the new temporal SAT representations, in comparison with solvers that operate on native IA representations. Our empirical results show that zChaff (a state-of-the-art complete SAT solver) together with the best IA-to-SAT encoding scheme, can solve temporal problems significantly faster than existing IA solvers working on the equivalent native IA networks. [Part of this study was published at the CP-05 workshop].

The study of Stochastic Local Search (SLS) algorithms is becoming more pivotal these days, due to their vast number of applications in decision making. Prior to the implementation of algorithmic knowledge for decision making, many decisions were made based on manual calculation, on the fly, or even based on guts feeling. Nowadays, such an approach is more rarely seen, especially when the decisions that need to be made are high-risk, cost intensive, or time-consuming. The increasingly often used SLS algorithms are one of the options available to assist the decision making process these days.The work discussed in this thesis concerns the study of SLS algorithms for solving the Quadratic Assignment Problem (QAP), a prominent combinatorial optimization problem, which until today is very hard to solve. Our interest is to study the behavior and performance of SLS algorithms for solving QAP instances of different characteristics, such as size, sparsity, and structure. In this study, we have also proposed new variants of SLS algorithms, inspired by existing, well-performing SLS algorithms for solving the QAP. The new variants of SLS algorithms are then further extended for solving the bi-objective QAP (bQAP).One main focus in this study is to see how the performance of algorithms scales with instance size. We have considered instances that are much larger than the ones usually used in the studies of algorithms for solving the QAP. By understanding how the algorithms perform when the instance size changes, we might be able to solve other problems effectively by considering the similarity in their characteristics to the ones of the QAP, or by seeing common trends in the relative performance of the various available SLS methods. For single objective QAP instances we found that the structure and size of instances do have a significant impact on the performance of SLS algorithms. For example, comparisons between Tabu Search (TS) and Simulated Annealing (SA) on instances with randomly generated matrices show that the overall performance of TS is better than SA, irrespective the size of instances considered. The results on a class of structured instances however show that TS performs well on small-sized instances, while on the larger ones, SA shows better results. In another experiment, Hierarchical Iterated Local Search (HILS) has shown very good results compared to several Iterated Local Search (ILS) variants. This experiment was done on a class of structured instances of size from 100 to 500. An extensive experiment on a class of structured instances of size 30 to 300 using tuned parameter settings shows that population based algorithms perform very well on most of the instance classes considered. SA however, shows very good performance especially on large-sized instances with low sparsity level. For the bQAP, the correlation between the flow matrices does have a strong effect that determines the performance of algorithms for solving them. Hybrid Simulated Annealing (HSA) clearly outperforms Hybrid Iterative Improvement (HII). When compared to Multi Objective Ant Colony Optimization (MOACO) and Strength Pareto Evolutionary Algorithm 2 (SPEA2), HSA shows very good performance, where HSA outperforms MOACO and SPEA2, especially on instances of large size, thus, offering a better scaling behavior. Based the results obtained in this study, it is possible to come up with a general idea on the suitability of SLS algorithms for solving instances with a certain characteristic. Given an unknown QAP instance, one can guess the most suitable algorithm for solving it depending on the type, size, and sparsity of the instance, while for a bQAP instance the most suitable algorithm can be guessed based on its size and correlation between the flow matrices. / Doctorat en Sciences de l'ingénieur et technologie / info:eu-repo/semantics/nonPublished

Dans cette thèse nous développons de nouvelles techniques pour résoudre les problèmes d'optimisation multi-critère. Ces problèmes se posent naturellement dans de nombreux domaines d'application (sinon tous) où les choix sont évalués selon différents critères conflictuels (coûts et performance par exemple). Contrairement au cas de l'optimisation classique, de tels problèmes n'admettent pas en général un optimum unique mais un ensemble de solutions incomparables, aussi connu comme le front de Pareto, qui représente les meilleurs compromis possibles entre les objectifs conflictuels. La contribution majeure de la thèse est le développement d'algorithmes pour trouver ou approximer ces solutions de Pareto pour les problèmes combinatoires difficiles. Plusieurs problèmes de ce type se posent naturellement lors du processus de placement et d'ordonnancement d'une application logicielle sur une architecture multi-coeur comme P2012, qui est actuellement développé par STMicroelectronics. / In this thesis we develop new techniques for solving multi-criteria optimization problems. Such problems arise naturally in many (if not all) application domains where choices are evaluated according to two or more conflicting criteria such as price vs. performance. Unlike ordinary optimization, such problems typically do not admit a unique optimum but a set of incomparable solutions, also known as the Pareto Front, which represent the best possible trade-offs between the conflicting goals. The major contribution of the thesis is the development of algorithms for finding or approximating these Pareto solutions for hard combinatorial problems that arise naturally in the process of mapping and scheduling application software on multi-core architectures such as P2012 which is currently being developed by ST Microelectronics.