Return to search

Formules booléennes quantifiées : transformations formelles et calculs parallèles

De nombreux problèmes d'intelligence artificielle et de vérification formelle se ramènent à un test de validité d'une formule booléenne quantifiée (QBF). Mais, pour effectuer ce test les solveurs QBF actuels ont besoin d'une formule sous une forme syntaxique restrictive, comme la forme normale conjonctive ou la forme normale de négation. L'objectif de notre travail est donc de s'affranchir de ces contraintes syntaxiques fortes de manière à utiliser le langage des QBF dans toute son expressivité et nous traitons ce sujet de manière formelle et calculatoire. Notre première contribution est un ensemble d'équivalences et d'algorithmes qui permettent de traiter un motif particulier, les résultats intermédiaires. Ce motif apporte une alternative efficace en espace et en temps de résolution, à la suppression naïve des biimplications et des ou-exclusifs lors de la mise sous forme prénexe. Il offre également de nouvelles possibilités de transformations dans différents fragments du langage QBF. Notre deuxième contribution est d'ordre calculatoire et a pour but d'exploiter la puissance des architectures de calcul parallèles afin de traiter des QBF sans restriction syntaxique. Nous élaborons donc une architecture innovante pour la parallélisation du problème de validité des QBF. Son originalité réside dans son architecture dite de « parallélisation syntaxique » par opposition aux architectures de parallélisation basée sur la sémantique des quantificateurs.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00578083
Date03 December 2010
CreatorsDa Mota, Benoit
PublisherUniversité d'Angers
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0019 seconds