De la validite des formules booleennes quanti eesDe la validite des formules booleennes quantieesetude de complexite et exploitation de classes traitablesau sein d’un prouveur qbfFlorian LetombeCRIL, CNRS FRE 2499Universite d’Artois, LensEncadrants :Sylvie Coste-MarquisDaniel Le BerrePierre Marquis (Directeur de these)13 decembre 20051/38De la validite des formules booleennes quanti eesIntroductionIntroductionComplexite de qbf pour certains fragments propositionnelsPresentation des fragmentsApercu des preuvesResultats de complexiteUn cas polynomialExploitation de classes traitables au sein d’un prouveur qbfAlgorithmiqueClasses polynomialesQb L’heuristique Resultats experimentauxConclusion et perspectives2/38De la validite des formules booleennes quanti eesIntroductionIntroductionComplexite de qbf pour certains fragments propositionnelsPresentation des fragmentsApercu des preuvesResultats de complexiteUn cas polynomialExploitation de classes traitables au sein d’un prouveur qbfAlgorithmiqueClasses polynomialesQb L’heuristique Resultats experimentauxConclusion et perspectives2/38De la validite des formules booleennes quanti eesIntroductionIntroductionComplexite de qbf pour certains fragments propositionnelsPresentation des fragmentsApercu des preuvesResultats de complexiteUn cas polynomialExploitation de classes traitables au sein d’un prouveur qbfAlgorithmiqueClasses ...
De´finition(QBF) UneQBFest une expression de la formeΠ
QBF´dfie:foontinileelrm
Q1X1. . .QnXn.Φ,(n≥0)
IQi(0≤i≤n) un quantificateur existentiel∃ou universel∀ IX1. . .Xnensembles de variables propositionnelles IΦ une formule propositionnelle sur ces variables
Ge´n´eralisationdesat Probl`emePSPACE-completcanonique [Stockmeyer & Meyer 1973] Nombreuses applications en IA : planification, raisonnement nonmonotone,inf´erenceparaconsistante,abduction,etc