La représentation des connaissances et les problèmes d’inférence associés restent à l’heure actuelle une problématique riche et centrale en informatique et plus précisément en intelligence artificielle. Dans ce cadre, la logique propositionnelle permet d’allier puissance d’expression et efficacité. Il reste que, tant que P est différent de NP, la déduction en logique propositionnelle ne peut admettre de solutions à la fois générales et efficaces. Dans cette thèse, nous adressons le problème de satisfiabilité et proposons de nouvelles classes d’instances pouvant être résolues de manière polynomiale.La découverte de nouvelles classes polynomiales pour SAT est à la fois importante d’un point de vue théorique et pratique. En effet, on peut espérer les exploiter efficacement au sein de solveurs SAT. Dans cette thèse, nous proposons d’étendre deux fragments polynomiaux de SAT à l’aide de la propagation unitaire tout en s’assurant que ces fragments demeurent reconnus et résolus de manière polynomiale. Le premier résultat de cette thèse concerne la classe Quad. Nous avons établi certaines propriétés de cette classe d’instances et avons étendu cette dernière de manière à s’abstraire de l’ordre imposé sur les littéraux. Le fragment obtenu en remplaçant cet ordre par différents ordres sur les clauses, conserve lamême complexité dans le pire cas. Nous avons également étudié l’impact de la résolution bornée et de la redondance par propagation unitaire sur cette classe. La seconde contribution concerne la classe polynomiale proposée par Tovey. La propagation unitaire est une nouvelle fois utilisée pour étendre cette classe. Nous comparons le nouveau fragment polynomial obtenu à deux autres classes basées également sur la propagation unitaire : Quad et UP-Horn. Nousapportons également une réponse à une question ouverte au sujet des connexions de ces classes. Nous montrons que UP-Horn et d’autres classes basées sur la propagation unitaire sont strictement incluses dans S Quad qui représente l’union de toutes les classes Quad obtenues par l’exploitation de tous les ordres sur les clauses possibles. / Knowledge representation and reasoning is a key issue in computer science and more particularly in artificial intelligence. In this respect, propositional logic is a representation formalism that is a good trade-off between the opposite computational efficiency and expressiveness criteria. However, unless P = NP, deduction in propositional logic is not polynomial in the worst case. So, in this thesis we propose new extensions of tractable classes of the propositional satisfiability problem. Tractable fragments of SAT play a role in the implementation of the most efficient current SAT solvers, many of thesetractable classes use the linear time unit propagation (UP) inference rule. We attempt to extend two of currently-known polynomial fragments of SAT thanks to UP in such a way that the fragments can still be recognized and solved in polynomial time. A first result focuses on Quad fragments: we establish some properties of Quad fragments and extend these fragments and exhibit promising variants. The extension is obtained by allowing Quad fixed total orderings of clauses to be accompanied with specific additional separate orderings of maximal sub-clauses. The resulting fragments extend Quad without degrading its worst-case complexity. Also, we investigate how bounded resolution and redundancy through unit propagation can play a role in this respect. The second contribution on tractable subclasses of SAT concerns extensions of one well-known Tovey’s polynomial fragment so that they also include instances that can be simplified using UP. Then, we compare two existing polynomial fragments based on UP: namely, Quad and UP-Horn. We also answer an open question about the connections between these two classes: we show that UP-Horn and some other UP-based variants are strict subclasses of S Quad, where S Quad is the union of all Quad classes obtained by investigating all possible orderings of clauses.

L’importance des problèmes CSP, WCSP et #CSP est reflétée par la part considérable des travaux, théoriques et pratiques, dont ils font l’objet en intelligence artificielle et bien au-delà. Leur difficulté est telle qu’ils appartiennent respectivement aux classes NP-complet, NP-difficile et #P-complet. Aussi, les méthodes qui permettent de résoudre efficacement leurs instances ont une complexité en temps exponentielle. Les travaux de recherche de cette thèse se focalisent sur les méthodes de résolution exploitant la notion de décomposition arborescente. Ces méthodes ont suscité un vif intérêt de la part de la communauté scientifique du fait qu’elles soient capables de résoudre en temps polynomial certaines classes d’instances. Cependant, en pratique, elles n’ont pas encore montré toute leur efficacité vu la qualité de la décomposition employée ne prenant en compte qu’un critère purement structurel, sa largeur. Premièrement, nous proposons un nouveau cadre général de calcul de décompositions qui a la vertu de calculer des décompositions qui capturent des paramètres plus pertinents à l’égard de la résolution que la seule largeur de la décomposition. Ensuite, nous proposons une exploitation dynamique de la décomposition pendant la résolution pour les problèmes (W)CSP. Le changement de la décomposition pendant la résolution vise à adapter la décomposition selon la nature de l’instance. Finalement, nous proposons un nouvel algorithme de comptage qui exploite la décomposition d’une façon différente de celle des méthodes standards afin d’éviter des calculs inutiles.L’ensemble des contributions ont été évaluées et validées expérimentalement. / The importance of CSP, WCSP and #CSP problems is reflected by the considerableamount of theoretical and practical work of which they are subject in artificial intelligenceand far beyond. Their difficulty is such that they belong respectively to the NP-complete,NP-hard and #P-complete classes. Hence, the methods that are able to solve efficientlytheir instances have a complexity in exponential time. The research works of this thesisfocus on the solving methods exploiting the notion of tree-decomposition. These methodshave aroused a keen interest from the scientific community because they are able to solvesome classes of instances in polynomial time. Nevertheless, in practice, they have notshown yet their full efficiency given the quality of the used decomposition that takes onlyinto account a purely structural criterion, its width. First, we propose a new generic framework for computing decompositions which has the virtue of computing decompositionsthat capture more relevant parameters in the context of solving than the width. Then,we propose a dynamic exploitation of the decomposition during the solving for (W)CSPproblems. The modification of the decomposition during the solving aims to adapt the decomposition to the nature of the instance. Finally, we propose a new counting algorithmthat exploits the decomposition in a different way than standard methods in order toavoid unnecessary computations. All the contributions have been evaluated and validatedexperimentally.