Tractable QBF by Knowledge Compilation
Type de document :
Communication dans un congrès avec actes
Titre :
Tractable QBF by Knowledge Compilation
Auteur(s) :
Capelli, Florent [Auteur]
Linking Dynamic Data [LINKS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Mengel, Stefan [Auteur]
Centre de Recherche en Informatique de Lens [CRIL]

Linking Dynamic Data [LINKS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Mengel, Stefan [Auteur]
Centre de Recherche en Informatique de Lens [CRIL]
Titre de la manifestation scientifique :
36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)
Ville :
Berlin
Pays :
Allemagne
Date de début de la manifestation scientifique :
2019-03-13
Discipline(s) HAL :
Informatique [cs]/Complexité [cs.CC]
Résumé en anglais : [en]
We generalize many results concerning the tractability of SAT and #SAT on bounded treewidth CNF-formula in the context of Quantified Boolean Formulas (QBF). To this end, we start by studying the notion of width for OBDD ...
Lire la suite >We generalize many results concerning the tractability of SAT and #SAT on bounded treewidth CNF-formula in the context of Quantified Boolean Formulas (QBF). To this end, we start by studying the notion of width for OBDD and observe that the blow up in size while existentially or universally projecting a block of variables in an OBDD only affects its width. We then generalize this notion of width to the more general representation of structured (deterministic) DNNF and give a similar algorithm to existentially or universally project a block of variables. Using a well-known algorithm transforming bounded treewidth CNF formula into deterministic DNNF, we are able to generalize this connection to quantified CNF which gives us as a byproduct that one can count the number of models of a bounded treewidth and bounded quantifier alternation quantified CNF in FPT time. We also give an extensive study of bounded width d-DNNF and proves the optimality of several of our results.Lire moins >
Lire la suite >We generalize many results concerning the tractability of SAT and #SAT on bounded treewidth CNF-formula in the context of Quantified Boolean Formulas (QBF). To this end, we start by studying the notion of width for OBDD and observe that the blow up in size while existentially or universally projecting a block of variables in an OBDD only affects its width. We then generalize this notion of width to the more general representation of structured (deterministic) DNNF and give a similar algorithm to existentially or universally project a block of variables. Using a well-known algorithm transforming bounded treewidth CNF formula into deterministic DNNF, we are able to generalize this connection to quantified CNF which gives us as a byproduct that one can count the number of models of a bounded treewidth and bounded quantifier alternation quantified CNF in FPT time. We also give an extensive study of bounded width d-DNNF and proves the optimality of several of our results.Lire moins >
Langue :
Anglais
Comité de lecture :
Oui
Audience :
Internationale
Vulgarisation :
Non
Collections :
Source :
Fichiers
- http://arxiv.org/pdf/1807.04263
- Accès libre
- Accéder au document
- 1807.04263
- Accès libre
- Accéder au document