Identifiant pérenne de la notice : 21332489X
Notice de type
Notice de regroupement
Note publique d'information : CE TRAVAIL PRESENTE D'ABORD LES DIFFERENTS ALGORITHMES DE RESOLUTION DU PROBLEME DE
SATISFAISABILITE. LES RECENTS TRAVAUX ET ANALYSES THEORIQUES CONNUS SONT EGALEMENT
EXAMINES. ENSUITE, EST ETUDIEE UNE CLASSE DE DONNEES DITES D'ENTROPIE MAXIMALE: CELLES
QUI ONT UNE CHANCE SUR DEUX D'ETRE SATISFAISABLES. CETTE CLASSE VA INTERVENIR DANS
L'UN DES CRITERES DE COMPARAISON DE CERTAINS ALGORITHMES DE RESOLUTION. SOUS UNE CERTAINE
HYPOTHESE, ON DEMONTRE L'IDENTITE ENTRE CETTE CLASSE ET UNE AUTRE CLASSE DE DONNEES;
CE QUI REPRESENTE UNE NOUVELLE METHODE DE DETERMINATION DES DONNEES D'ENTROPIE MAXIMALE.
CE TRAVAIL CONTIENT ENSUITE LES RESULTATS D'EXPERIMENTATIONS SUR L'APPORT, DE DIFFERENTES
HEURISTIQUES OU STRATEGIES, A LA PROCEDURE DE DAVIS-PUTNAM QUI N'UTILISE QUE LE BACKTRACK
(DP) AINSI QU'A L'ALGORITHME DE SL-RESOLUTION. ON PROCEDE EGALEMENT A LA COMPARAISON
DES PERFORMANCES DES MEILLEURES VARIANTES DE CHACUN DES DEUX ALGORITHMES. AFIN D'ACCELERER
L'ALGORITHME DE SL-RESOLUTION AVEC REMONTEE D'IMPASSES (SLRI), DES HEURISTIQUES CORRESPONDANT
A CELLES CONNUES POUR DP Y SONT INTRODUITES. DANS LE CAS DE DONNEES D'ENTROPIE MAXIMALE,
L'ACCELERATION DE SLRI PAR LA REGLE DE LA CLAUSE MONO-LITTERALE VA S'AVERER COMPARABLE
A CELLE DE DP PAR LA MEME REGLE. ON EXPERIMENTE, ENFIN, DES METHODES DE DETERMINATION
DES THEOREMES ATOMIQUES (CLAUSES PRODUITES MONO-LITTERALES) POUR UNE CERTAINE DONNEE.
ON PRESENTE EGALEMENT UNE METHODE PROBABILISTE DONT LE DEGRE DE CONFIANCE EST ESTIME
paprika.idref.fr
data.idref.fr
Documentation
