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.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00578083 |
| Date | 03 December 2010 |
| Creators | Da Mota, Benoit |
| Publisher | Université d'Angers |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0022 seconds