Cette thèse porte sur la résolution séquentielle et parallèle du problème de la satisfiabilité propositionnelle(SAT). Ce problème important sur le plan théorique admet de nombreuses applications qui vont de la vérification formelle de matériels et de logiciels à la cryptographie en passant par la planification et la bioinformatique. Plusieurs contributions sont apportées dans cette thèse. La première concerne l’étude et l’intégration des concepts d’intensification et de diversification dans les solveurs SAT parallèle de type portfolio. Notre seconde contribution exploite l’état courant de la recherche partiellement décrit par les récentes polarités des littéraux « progress saving », pour ajuster et diriger dynamiquement les solveurs associés aux différentes unités de calcul. Dans la troisième contribution, nous proposons des améliorations de la stratégie de réduction de labase des clauses apprises. Deux nouveaux critères, permettant d’identifier les clauses pertinentes pour la suite de la recherche, ont été proposés. Ces critères sont utilisés ensuite comme paramètre supplémentaire de diversification dans les solveurs de type portfolio. Finalement, nous présentons une nouvelle approche de type diviser pour régner où la division s’effectue par ajout de contraintes particulières. / In this thesis, we deal with the sequential and parallel resolution of the problem SAT. Despite of its complexity, the resolution of SAT problem is an excellent and competitive approach for solving thecombinatorial problems such as the formal verification of hardware and software, the cryptography, theplanning and the bioinfomatics. Several contribution are made in this thesis. The first contribution aims to find the compromise of diversification and intensification in the solver of type portfolio. In our second contribution, we propose to dynamically adjust the configuration of a core in a portfolio parallel sat solver when it is determined that another core performs similar work. In the third contribution, we improve the strategy of reduction of the base of learnt clauses, we construct a portfolio strategy of reduction in parallel solver. Finally, we present a new approach named "Virtual Control" which is to distribute the additional constraints to each core in a parallel solver and verify their consistency during search.

Cette thèse est dédiée à l'étude d'une large classe d'algorithmes, appelés algorithmes en arbre. En utilisant une représentation probabiliste appropriée, le comportement asymptotique de tels algorithmes est analysé. L'approche unifie les études faites sur ces algorithmes ainsi que simplifie et généralise certains résultats établis dans le domaine.

L'acquisition de modèles 3D des scènes réelles trouve son utilité dans de nombreuses applications pratiques, comme l'archivage numérique, les jeux vidéo, l'ingénierie, la publicité. Il existe principalement deux méthodes pour acquérir un modèle 3D: la reconstruction avec un scanner laser (méthode active) et la reconstruction à partir de plusieurs photographies d'une même scène prise dans des points de vues différentes (méthode passive). Si la méthode active permet d'acquérir des modèles avec une grande précision, il est cependant coûteux et difficile à mettre en place pour de grandes scènes extérieures. La méthode passive, ou la stéréo multi-vues est en revanche plus flexible, facile à mettre en oeuvre et surtout moins coûteuse que la méthode active. Cette thèse s'attaque au problème de la reconstruction de stéréo multi-vues à grande échelle et précise pour les scènes extérieures. Nous améliorons des méthodes précédentes et les assemblons pour créer une chaîne de stéréo multi-vues efficace tirant parti de l'accélération de cartes graphiques. La chaîne produit des maillages de qualité à partir d'images de haute résolution, ce qui permet d'atteindre les meilleurs scores dans de nombreuses évaluations. Aux plus grandes échelles, nous développons d'une part des techniques de type diviser-pour-régner pour reconstruire des morceaux partiaux de la scène. D'autre part, pour combiner ces résultats séparés, nous créons une nouvelle méthode qui fusionne rapidement des centaines de maillages. Nous réussissons à reconstruire de beaux maillages urbains et des monuments historiques précis à partir de grandes collections d'images (environ 1600 images de 5M Pixel) / Acquisition of 3D model of real objects and scenes is indispensable and useful in many practical applications, such as digital archives, game and entertainment industries, engineering, advertisement. There are 2 main methods for 3D acquisition : laser-based reconstruction (active method) and image-based reconstruction from multiple images of the scene in different points of view (passive method). While laser-based reconstruction achieves high accuracy, it is complex, expensive and difficult to set up for large-scale outdoor reconstruction. Image-based, or multi-view stereo methods are more versatile, easier, faster and cheaper. By the time we begin this thesis, most multi-view methods could handle only low resolution images under controlled environment. This thesis targets multi-view stereo both both in large scale and high accuracy issues. We significantly improve some previous methods and combine them into a remarkably effective multi-view pipeline with GPU acceleration. From high-resolution images, we produce highly complete and accurate meshes that achieve best scores in many international recognized benchmarks. Aiming even larger scale, on one hand, we develop Divide and Conquer approaches in order to reconstruct many small parts of a big scene. On the other hand, to combine separate partial results, we create a new merging method, which can merge automatically and quickly hundreds of meshes. With all these components, we are successful to reconstruct highly accurate water-tight meshes for cities and historical monuments from large collections of high-resolution images (around 1600 images of 5 M Pixel images)

Ce manuscrit de thèse développe certains aspects autour de trois thèmes généraux, sur la représentation arborescente des familles d'ensembles, les décompositions de graphes, et les algorithmes de graphes. Les thèmes abordés vont de la combinatoire théorique à l'algorithmique en bio-informatique, en passant par plusieurs décompositions de graphes et aussi par l'optimisation combinatoire.<br /><br />La première moitié du manuscrit développe deux études. D'abord, afin d'estimer le nombre de familles d'ensembles satisfaisant certains axiomes de clôture, de nouveaux outils et techniques pour obtenir des représentations arborescentes de celles-ci ont été développés. Puis, l'étude se poursuit avec une des applications des propriétés ci-dessus : celle concernant les décompositions de graphes.<br /><br />La deuxième moitié du manuscrit est consacrée aux applications des décompositions de graphes dans l'algorithmique de graphes. Trois problèmes algorithmiques seront à l'étude.<br />Dans chacun des trois, il est montré pourquoi et comment on peut appliquer l'idée de la décomposition de graphes pour résoudre le problème posé de manière efficace.<br />Il est également montré comment appliquer les trois solutions proposées pour résoudre trois autres problèmes d'algorithmique de graphes.

L'acquisition de modèles 3D des scènes réelles trouve son utilité dans de nombreuses applications pratiques, comme l'archivage numérique, les jeux vid eo, l'ingénierie, la publicité. Il existe principalement deux méthodes pour acqu érir un modèle 3D: la reconstruction avec un scanner laser (méthode active) et la reconstruction à partir de plusieurs photographies d'une même scène prise dans des points de vues différents (méthode passive). La méthode passive, ou la stéréo multi-vues est en revanche plus flexible, facile à mettre en oeuvre avec une grande précision, et surtout moins couteuse que la méthode active. Cette thèse s'attaque au problème de la reconstruction de stereo multi-vues à grande échelle . Nous améliorons des méthodes précédentes et les assemblons pour créer une chaine de stereo multi-vues efficace tirant parti de l'accélération des cartes graphiques. La chaîne produit des maillages de qualité à partir d'images de haute résolution, ce qui permet d'atteindre les meilleurs scores dans de nombreuses évaluations. Aux plus grandes échelles, nous développons d'une part des techniques de type diviser-pour-régner pour reconstruire des morceaux partiaux de la scène. D'autre part, pour combiner ces résultats séparés, nous créons une nouvelle méthode qui fusionne rapidement des centaines de maillages. Nous réussissons à reconstruire de beaux maillages urbains et des monuments historiques précis à partir de grandes collections d'images (environ 1600 images de 5M Pixel).

Les algorithmes MCMC sont difficiles à mettre à l'échelle, car ils doivent balayer l'ensemble des données à chaque itération, ce qui interdit leurs applications dans de grands paramètres de données. En gros, tous les algorithmes MCMC évolutifs peuvent être divisés en deux catégories: les méthodes de partage et de conquête et les méthodes de sous-échantillonnage. Le but de ce projet est de réduire le temps de calcul induit par des fonctions complexes ou à grande efficacité. / MCMC algorithms are difficult to scale, since they need to sweep over the whole data set at each iteration, which prohibits their applications in big data settings. Roughly speaking, all scalable MCMC algorithms can be divided into two categories: divide-and-conquer methods and subsampling methods. The aim of this project is to reduce the computing time induced by complex or largelikelihood functions.