This HTML5 document contains 33 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Subject Item

n2:id

rdf:type

frbr:Work rdac:C10001

marcrel:ths

n13:id

skos:altLabel

Constraint hypothesis, an explanation of UP heuristic success in the resolution of boolean satisfiability problems

dc:subject

Fonctions booléennes Informatique expérimentale Intelligence artificielle Résolution de problème NP Thèses et écrits académiques Procédure DPL Arbre recherche binaire Problème SAT Contraintes (mécanique) Problème NP complet Heuristique SAT

skos:prefLabel

Hypothèse de contrainte, une explication de la réussite de l'heuristique UP dans la résolution des problèmes de satisfiabilité des expressions booléennes

dcterms:language

n10:fra

dcterms:subject

n16:id n17:id n18:id n19:id n20:id n22:id n23:id

dc:title

Hypothèse de contrainte, une explication de la réussite de l'heuristique UP dans la résolution des problèmes de satisfiabilité des expressions booléennes

marcrel:dgg

n14:id

skos:note

Le problème SAT est un cas particulier du problème de satisfaction de contraintes où les variables prennent la valeur booléenne 0 ou 1. Le problème de satisfaction de contrainte lui-même joue un rôle central dans l'intelligence artificielle (IA). L'étude du problème SAT a une forte utilité pratique car il est à la base de très nombreux problèmes d'IA, notamment la déduction automatique, le contrôle de circuits VLSI, la programmation logique, l'apprentissage, l'ordonnancement, etc. en 1962, Davis, Logemann et Loveland ont présenté leur algorithme, appelé ensuite procédure DPL, pour résoudre le problème SAT. Selon cette procédure, des systèmes complets ont été crées, par exemple, Grasp, Posit, Relsat(4), Satz, etc. notre travail se situe précisément au sein du domaine des études empiriques pour la résolution du problème SAT en utilisant les systèmes complets. Tout d'abord, nous réalisons une étude empirique pour trouver quelques propriétés intéressantes correspondant à la difficulté de la résolution des problèmes 3-SAT aléatoires, en utilisant les systèmes différents. Puis, nous contribuons à l'amélioration du système Satz, en mettant en œuvre une série d'expérimentations utilisant heuristiques UP différentes. Nous utilisons ensuite Satz pour analyser les arbres produits par ce système, pour réaliser la comparaison avec les systèmes les plus performants de la littérature et également pour créer quelques extensions. Enfin, nous essayons d'expliquer la performance de Satz par l'hypothèse de contrainte. Nos expériences dans ce travail renforcent la conviction que l'heuristique UP est puissante pour les problèmes SAT aléatoires, et elle l'est aussi pour les problèmes SAT structures. Nous pensons également que la stratégie essentielle, pour implanter la procédure DPL dans un système, est d'essayer d'atteindre une contradiction aussi vite que possible ; d'autre part, selon nous, les heuristiques sont probablement la méthode la plus efficace pour mettre en œuvre de telles stratégies. Toutefois, si les heuristiques venaient à ne pas bien fonctionner, il faudrait recourir à d'autres méthodes. Par exemple, pour les problèmes ou la plupart des variables sont symétriques, il pourrait être judicieux d'essayer des méthodes telles que l'apprentissage ou la détection de symétrie. Satz pourrait être amélioré dans ce sens. Il n'existe a ce jour aucun système capable de résoudre tous les problèmes NP-complets et en particulier les problèmes SAT. Les systèmes qui existent actuellement ne résolvent que certaines classes du problème SAT.

dc:type

Text

n5:P1001

n6:T1009

rdaw:P10219

1998

rdau:P60049

n4:1020