Deux Fragments Polynomiaux Complets pour le problème de la validité des Formules Booléennes Quantifiées

Résumé : Dans cet article nous mettons en évidence deux fragments polynomiaux complets OCNF< et ODNF< qui constituent respectivement des sous ensembles des formules propositionnelles CNF et DNF. Chacun de ces fragments permet l'élimination des quantifications en un temps polynomial comme une loi interne sur le fragment. Grace à cette propriété le problème de la validité des formules Booléennes quantifiées peut être décidé en temps polynomial lorsque la matrice de l'instance traitée appartient à l'un des deux fragments considérés. Sur le plan pratique, nous montrons que contrairement à ce qui se passe pour des formules issues d'autres classes polynomiales pour SAT, comme celle des formules Horn CNF ou plus généralement des formules Horn renommables CNF, les prouveurs QBF existants exhibent empiriquement un comportement polynomial sur les instances OCNF< quantifiées.
Type de document :
Communication dans un congrès
Deuxièmes Journées Francophones de Programmation par Contraintes (JFPC06), 2006, Nîmes - Ecole des Mines d'Alès / France, 2006
Liste complète des métadonnées

https://hal.inria.fr/inria-00085779
Contributeur : Laurent Henocque <>
Soumis le : vendredi 14 juillet 2006 - 10:08:00
Dernière modification le : jeudi 11 janvier 2018 - 06:19:28
Document(s) archivé(s) le : lundi 5 avril 2010 - 22:02:31

Fichier

Identifiants

  • HAL Id : inria-00085779, version 1

Collections

Citation

Florian Letombe. Deux Fragments Polynomiaux Complets pour le problème de la validité des Formules Booléennes Quantifiées. Deuxièmes Journées Francophones de Programmation par Contraintes (JFPC06), 2006, Nîmes - Ecole des Mines d'Alès / France, 2006. 〈inria-00085779〉

Partager

Métriques

Consultations de la notice

101

Téléchargements de fichiers

34