Autour de SAT : le calcul d'impliquants P-restreints, algorithmes et applications

Our work concernes two major problems in propositional logic : the satisfiability of a boolean formula (SAT problem) and the computation of its prime implicants/implicates. The first one is widely studied in the Artificial Intelligence community and some recent results show that SAT algorithms can be used efficiently to solve problems in domains where specialized algorithms were used (planning or diagno- sis for example). The second one is very important because it characterizes abductive reasoning (im- plicate framework). We propose to modify a SAT algorithm (the Davis and Putnam procedure) to com- pute formulas used by Assumption-based Truth Maintenance Systems. We formalize our method in terms of prime P-restricted implicants : the intersection between a model and a consistent set of liter- als. Then we apply our formalization in two examples of non-monotonic reasoning: Closed World Rea- soning and Argumentation. We introduce preference relations between P-restricted implicants. For example, in diagnosis, minimal cardinality explanations are sufficient. If other informations are avail- able (fault probabilities for each component for instance), most probable explanations are preferred. We take two examples of such preference relations in argumentation. Finally, we show that qualitative decision theory in a logical framework can also be modeled with P-restricted implicants.Les travaux présentés concernent les deux problèmes fondamentaux de la logique propositionnelle : la satisfiabilité d'une formule logique (problème SAT) et la détermination de ses impliquants/impliqués premiers. Le premier problème est largement étudié par la communauté IA et les progrès récents sont si importants que l'on utilise actuellement des algorithmes de résolution de SAT pour traiter des pro- blèmes dans des domaines jusqu'alors réservés à des prouveurs spécialisés (planification ou diagnos- tic par exemple). Le second est très important car il caractérise le raisonnement abductif (notion d’impliqué). Nous proposons de modifier une méthode de résolution de SAT (la procédure de Davis et Putnam) afin de produire des formules utilisées par des outils comme l'ATMS. Nous avons formalisé cette méthode par la notion d’impliquant P-restreint premier : intuitivement, il s’agit de l’intersection d’un modèle avec un ensemble consistant de littéraux. Nous utilisons ensuite cette notion dans le cadre du raisonnement non monotone : en raisonnement en monde clos (Closed World Reasoning) et dans le cadre de l'argumentation. Nous avons étendu notre formalisation afin d’utiliser différentes rela- tions de préférence entre impliquants P-restreints (notion d’impliquant P-restreint préféré). Dans le cadre du diagnostic, on cherchera souvent les explications mettant en cause le plus petit nombre de composants. Si l'on dispose de connaissances exogènes (des probabilités de panne pour chaque composant par exemple), on souhaite obtenir le diagnostic de panne le plus probable. Dans le cadre de l’argumentation, nous donnons deux exemples de ces relations de préférence. Ces travaux s'éloi- gnent du domaine de la satisfaction pour rejoindre les travaux sur l'optimisation. Nous montrons enfin dans le cadre de l'approche logique de la décision qualitative comment profiter de certaines particula- rités de notre méthode de calcul d’impliquant P-restreint pour calculer des décisions optimales