Base littérale et certificat pour les formules booléennes quantifiées

Résumé : Nous étudions dans cet article une nouvelle forme normale, celle des bases littérales, pour les formules booléennes quantifiées (prénexes). Un des aspects majeurs d'une base littérale est que le certificat (qui permet de vérifier a posteriori qu'une décision positive sur une formule booléenne quantifiée est correcte ou non) en est un cas particulier. Notre principal résultat est un algorithme orienté recherche qui calcule un certificat associé à une formule booléenne quantifiée dans le cas où elle est valide. Un autre aspect majeur d'une base littérale est qu'elle peut être vue comme étant le résultat d'une compilation de la formule booléenne quantifiée qui respecte des propriétés d'optimalité en terme de construction de la solution et de minimalité en terme de modèles propositionnels de la matrice.
Type de document :
Communication dans un congrès
Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.307-316, 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00292680
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : mercredi 2 juillet 2008 - 13:54:35
Dernière modification le : mercredi 21 février 2018 - 15:48:03
Document(s) archivé(s) le : vendredi 28 mai 2010 - 23:05:09

Fichier

pages-307-316-article26.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00292680, version 1

Collections

Citation

Igor Stéphan, Benoit Da Mota. Base littérale et certificat pour les formules booléennes quantifiées. Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.307-316, 2008. 〈inria-00292680〉

Partager

Métriques

Consultations de la notice

104

Téléchargements de fichiers

71