De la validité des formules booléennes quantifiées - étude de complexité et exploitation de classes
79
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
79
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
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 ...
Voir
Publié par
Langue
Français
Delavalidite´desformulesboole´ennesquantifi´ees ´etudedecomplexit´eetexploitationdeclassestraitables in d’ eurqbf au se un prouv
Encadrants : Sylvie Coste-Marquis Daniel Le Berre PierreMarquis(Directeurdeth`ese)
FlorianteLbeom CRIL, CNRS FRE 2499 Universit´ed’Artois,Lens
13d´ecemb
Exploitation de classes traitables au sein d’un prouveurqbf Algorithmique Classes polynomiales Qbfl L’heuristique Δ Re´sultatsexpe´rimentaux
Conclusion et perspectives
Complexite´deqbfpour certains fragments propositionnels Pr´esentationdesfragments Apercu des preuves ¸ Re´sultatsdecomplexit´e Un cas polynomial
Introduction
2/38Dleditivalaanqufi´tieel´esnnelumoobsede´rofsudtcoineeIstnor
Conclusion et perspectives
Exploitation de classes traitables au sein d’un prouveurqbf Algorithmique Classes polynomiales Qbfl L’heuristique Δ Re´sultatsexpe´rimentaux
Introduction
Complexite´deqbfpour certains fragments propositionnels Pr´esentationdesfragments Aperc¸udespreuves Re´sultatsdecomplexite´ Un cas polynomial
luseofmre´neoblovaliDelaedesdit´dortitcunosqnentua´eifiInes
Introduction
Conclusion et perspectives
Complexite´deqbfpour certains fragments propositionnels Pre´sentationdesfragments Ap ¸u des preuves erc R´esultatsdecomplexite´ Un cas polynomial
Exploitation de classes traitables au sein d’un prouveurqbf Algorithmique Classes polynomiales Qbfl L’heuristique Δ R´esultatsexpe´rimentaux
382/Dladilevadesfit´elesbormunnee´looitnauqsentsIeefi´ioctduron
Exploitation de classes traitables au sein d’un prouveurqbf Algorithmique Classes polynomiales Qbfl L’heuristique Δ Re´sultatsexpe´rimentaux
38
Introduction
Conclusion et perspectives
Complexite´deqbfpour certains fragments propositionnels Pr´esentationdesfragments Aper¸cudespreuves Re´sultatsdecomplexite ´ Un cas polynomial
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
(¬y1∨ ¬y2)∧(y2∨ ¬x)]
[(y1∨y2)∧(¬y2∨x)∧
∀x∃y1,y2.
Exemple
8
Validite´d’uneQBF
Existenced’unestrate´giegagnantedansunjeucontrelanature(∀)
43/ntroeesIionductitidalavelDbsooumelfsroe´edtifi´quannnesl´ee
∀x∃y1,y2.
Exemple
8
Validit´ed’uneQBF Existenced’unestrate´giegagnantedansunjeucontrelanature(∀)
>
y2 ¬y1
x
(¬y1∨ ¬y2)∧(y2/∨//¬//x/)]
[(y1∨y2/)∧///(¬//y//2//∨///x//)∧
4/3avalDele´edditiumelfsroionoosbeel´esnnanqu´fiitIseeortntcud
Existenced’unestrat´egiegagnantedansunjeucontrelanature(∀)
>
Validite´d’uneQBF
x y2 ¬y1
>
(¬y1∨ ¬y2)/∧(///y/2///∨///¬//x//)]
¬y2 y1
[(y1∨y2)∧(¬y2/∨//x/)∧
∀x∃y1,y2.
Exemple
tiucon
6≡
∀x∃y1,y2. [(y1∨y2)∧(¬y2∨x)∧ (¬y1∨ ¬y2)∧(y2∨ ¬x)]
Exemple
∃y1∀x∃y2. [(y1∨y2)∧(¬y2∨x)∧ (¬y1∨ ¬y2)∧(y2∨ ¬x)]
y1
x ∗ ¬y2 ⊥ >
x y2¬y2 ¬y1y1 > >
∀)e(uratanel
QBF
I I
I
Ge´n´eralisationdesat Probl`emePSPACE-completcanonique [Stockmeyer & Meyer 1973] Nombreuses applications en IA : planification, raisonnement nonmonotone,inf´erenceparaconsistante,abduction,etc
probl`qb emef
Le
83/5nneel´oosblemuortnIsee´fiitnauqseDedfstie´ladileva
