Satisfiabilité propositionnelle et raisonnement par contraintes : modèles et algorithmes

• Main Author: Lagniez, Jean-Marie
• Other Authors: Artois
• Language: fr
• Published: 2011
• Subjects: Satisfiabilité propositionnelle; Problèmes de satisfaction de contraintes; Résolution parallèle; Hybridation
• Online Access: http://www.theses.fr/2011ARTO0404/document

La thèse porte sur la résolution des problèmes de satisfiabilité propositionnelle (SAT) et des problèmesde satisfaction de contraintes (CSP). Ces deux modèles déclaratifs sont largement utilisés pour résoudredes problèmes combinatoires de première importance comme la vérification formelle de matérielset de logiciels, la bioinformatique, la cryptographie, la planification et l’ordonnancement de tâches.Plusieurs contributions sont apportées dans cette thèse. Elles vont de la proposition de schémas d’hybridationdes méthodes complètes et incomplètes, répondant ainsi à un challenge ouvert depuis 1998, àla résolution parallèle sur architecture multi-coeurs, en passant par l’amélioration des stratégies de résolution.Cette dernière contribution a été primée à la dernière conférence internationale du domaine (prixdu meilleur papier). Ce travail de thèse a donné lieu à plusieurs outils (open sources) de résolution desproblèmes SAT et CSP, compétitifs au niveau international. === This thesis deals with propositional satisfiability (SAT) and constraint satisfaction problems(CSP). These two declarative models are widely used for solving several combinatorial problems (e.g.formal verification of hardware and software, bioinformatics, cryptography, planning, scheduling, etc.).The first contribution of this thesis concerns the proposition of hybridization schemes of complete andincomplete methods, giving rise to an original answer to a well-known challenge open since 1998. Secondly,a new and efficient multi-core parallel approach is proposed. In the third contribution, a novelapproach for improving clause learning management database is designed. This contribution allows spatialcomplexity reduction of the resolution-based component of SAT solvers while maintaining relevantconstraints. This contribution was awarded at the last international SAT conference (best paper award).This work has led to several open sources solving tools for both propositional satisfiability and constraintssatisfaction problems.