De la validité des formules booléennes quantifiées - étude de complexité et exploitation de classes

De
Publié par

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 ...
Publié le : jeudi 1 mars 2012
Lecture(s) : 44
Nombre de pages : 79
Voir plus Voir moins
Delavalidit´edefsroumelbsoo´leeesnnanqu´tiseeer0250/183
Delavalidite´desformulesboole´ennesquanti´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´edArtois,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/38Dleditivalaanqu´tieel´esnnelumoobsede´rofsudtcoineeIstnor
23/8
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´eiInes
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´looitnauqsentsIee´ioctduron
dilae´tiDvaleudortnIsnoitcroumedfsoo´lelbsesqueenn´eeanti2/
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
eDlumrobsee´loennevaladiliedt´foesitnodocuntisquaIntr´ees33/8
De´nition(QBF) UneQBFest une expression de la formeΠ
QBF´de:foontinileelrm
Q1X1. . .QnXn.Φ,(n0)
IQi(0in) un quantificateur existentielou universelIX1. . .Xnensembles de variables propositionnelles IΦ une formule propositionnelle sur ces variables
(¬y1∨ ¬y2)(y2∨ ¬x)]
[(y1y2)(¬y2x)
xy1,y2.
Exemple
8
Validite´duneQBF
Existencedunestrate´giegagnantedansunjeucontrelanature()
43/ntroeesIionductitidalavelDbsooumelfsroe´edti´quannnesl´ee
xy1,y2.
Exemple
8
Validit´eduneQBF Existencedunestrate´giegagnantedansunjeucontrelanature()
>
y2 ¬y1
x
(¬y1∨ ¬y2)(y2///¬//x/)]
[(y1y2/)///(¬//y//2/////x//)
4/3avalDele´edditiumelfsroionoosbeel´esnnanqu´itIseeortntcud
dit´valiformedeseDal´eintuaodtrInesloobseluqsennee´/483
Existencedunestrat´egiegagnantedansunjeucontrelanature()
>
Validite´duneQBF
x y2 ¬y1
>
(¬y1∨ ¬y2)/(///y/2//////¬//x//)]
¬y2 y1
[(y1y2)(¬y2///x/)
xy1,y2.
Exemple
tiucon
dateunnsucjetronartsge´tageinangBFExistenceduneVnladitie´dnuQentsIee´ioctduronnee´looitnauqsedesfit´elesbormuDladileva83/4
6≡
xy1,y2. [(y1y2)(¬y2x)(¬y1∨ ¬y2)(y2∨ ¬x)]
Exemple
y1xy2. [(y1y2)(¬y2x)(¬y1∨ ¬y2)(y2∨ ¬x)]
y1
x ∗ ¬y2 ⊥ >
x y2¬y2 ¬y1y1 > >
)e(uratanel
udoroitcn
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´itnauqseDedfstie´ladileva
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.