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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/inria-00292680
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Submitted on : Wednesday, July 2, 2008 - 1:54:35 PM
Last modification on : Friday, May 10, 2019 - 12:50:14 PM
Long-term archiving on : Friday, May 28, 2010 - 11:05:09 PM

File

pages-307-316-article26.pdf
Files produced by the author(s)

Identifiers

  • 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. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, LINA - Université de Nantes - Ecole des Mines de Nantes, Jun 2008, Nantes, France. pp.307-316. ⟨inria-00292680⟩

Share

Metrics

Record views

123

Files downloads

301