Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/inria-00085806
Contributor : Laurent Henocque <>
Submitted on : Friday, July 14, 2006 - 3:10:13 PM
Last modification on : Thursday, February 7, 2019 - 4:48:30 PM
Long-term archiving on: : Monday, April 5, 2010 - 10:20:55 PM

File

Identifiers

  • 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. ⟨inria-00085806⟩

Share

Metrics

Record views

174

Files downloads

187