Une nouvelle architecture parallèle pour le problème de validité des QBF

Résumé : Dans ce papier, nous présentons une nouvelle architecture parallèle ouverte pour répondre à différents problèmes portant sur les formules booléennes quantifiées, dont la validité. La principale caractéristique de notre approche est qu'elle est basée sur un découpage syntaxique de la formule pour le traitement de sous-formules indépendantes. Elle est liée au choix de traiter des formules booléennes quantifiées sans restriction syntaxique, comme la forme prénexe ou la forme normale conjonctive. Dans ce cadre parallèle général ouvert, nous sommes capables d'introduire différents oracles, sous la forme d'algorithmes séquentiels pour l'élimination de quantificateurs. Nous présentons nos premières expérimentations en instanciant un unique oracle et en rapportons les résultats.
Type de document :
Communication dans un congrès
JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.113-122, 2010
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00520314
Contributeur : Christophe Lecoutre <>
Soumis le : mercredi 22 septembre 2010 - 19:13:54
Dernière modification le : mercredi 21 février 2018 - 15:48:03
Document(s) archivé(s) le : jeudi 25 octobre 2012 - 11:21:55

Fichier

igor.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : inria-00520314, version 1

Collections

Citation

Benoit Da Mota, Pascal Nicolas, Igor Stéphan. Une nouvelle architecture parallèle pour le problème de validité des QBF. JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.113-122, 2010. 〈inria-00520314〉

Partager

Métriques

Consultations de la notice

148

Téléchargements de fichiers

141