Extraire des Certificats des Formules Booléennes Quantifiées

Résumé : En donnant des moyens d'exprimer l'alternation de quantificateurs existentiels et universels, les langages quantifiés permettent de poser formellement des questions dont la réponse est une stratégie. Par exemple, on peut encoder les règles d'un jeu comme un ensemble de contraintes, puis demander l'existence d'une stratégie gagnante (ou au moins nonperdante) pour ce jeu. Dans le cas de formules booléennes quantifiées, une telle stratégie, si elle existe, est représentée par un certificat de satisfiabilité, qui est une représentation compacte d'un des modèles de la formule et qui peut être utilisé pour donner une preuve de satisfiabilité indépendante du solveur. Etant donnée la nature intrinsèque des formules quantifiées, de tels certificats demandent beaucoup de soin pour être extraits efficacement, représentés de façon compacte et pour que l'on puisse aisément leur poser des requêtes. Nous montrons comment résoudre ces problèmes.
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

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

https://hal.inria.fr/inria-00085806
Contributeur : Laurent Henocque <>
Soumis le : vendredi 14 juillet 2006 - 15:10:13
Dernière modification le : mercredi 29 novembre 2017 - 10:20:11
Document(s) archivé(s) le : lundi 5 avril 2010 - 22:20:55

Fichier

Identifiants

  • HAL Id : inria-00085806, version 1

Collections

Citation

Marco Benedetti. Extraire des Certificats 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-00085806〉

Partager

Métriques

Consultations de la notice

128

Téléchargements de fichiers

86