Soutenance these

Gilles Audemard

Informations

• Publié par: Adrie
• Nombre de lectures: 40
• Langue: Français

Extrait

R´esolution du probl`eme SAT
et
G´en´eration de Mod`eles finis en logique
du premier ordre
Gilles Audemard
Le 25 octobre 2001
Pr´epar´ee au sein du LIM
•Page 1 / 46 •First •Prev •Next •LastPlan
Le probl`eme SAT
• D´efinitions
• Production de litt´eraux
• La m´ethode Aval
• Exp´erimentations
•Page 2 / 46 •First •Prev •Next •LastPlan
Le probl`eme SAT
• D´efinitions
• Production de litt´eraux
• La m´ethode Aval
• Exp´erimentations
G´en´eration de mod`eles finis
• D´efinitions
• Propagations de contraintes
• D´ependances des symboles fonctionnels
• Sym´etries triviales
• Recherche dynamique des sym´etries
• Exp´erimentations
•Page 2 / 46 •First •Prev •Next •LastLe probl`eme SAT
•Page 3 / 46 •First •Prev •Next •LastLe probl`eme SAT
Un ensemble de variables {x ,...,x }1 n
•Page 3 / 46 •First •Prev •Next •LastLe probl`eme SAT
Un ensemble de variables {x ,...,x }1 n
• Un litt´eral est une variable ou sa n´egation : x ,¬x1 4
•Page 3 / 46 •First •Prev •Next •LastLe probl`eme SAT
Un ensemble de variables {x ,...,x }1 n
• Un litt´eral est une variable ou sa n´egation : x ,¬x1 4
• Une clause est une disjonction de litt´eraux : x ∨¬x1 4
•Page 3 / 46 •First •Prev •Next •LastLe probl`eme SAT
Un ensemble de variables {x ,...,x }1 n
• Un litt´eral est une variable ou sa n´egation : x ,¬x1 4
• Une clause est une disjonction de litt´eraux : x ∨¬x1 4
• Une formule sous forme CNF est une conjonction de clauses
•Page 3 / 46 •First •Prev •Next •LastLe probl`eme SAT
Un ensemble de variables {x ,...,x }1 n
• Un litt´eral est une variable ou sa n´egation : x ,¬x1 4
• Une clause est une disjonction de litt´eraux : x ∨¬x1 4
• Une formule sous forme CNF est une conjonction de clauses
Existe-t-il une interpr´etation des variables qui satisfait l’ensemble des
clauses ?
•Page 3 / 46 •First •Prev •Next •Last6
6
6
Le probl`eme SAT
Un ensemble de variables {x ,...,x }1 n
• Un litt´eral est une variable ou sa n´egation : x ,¬x1 4
• Une clause est une disjonction de litt´eraux : x ∨¬x1 4
• Une formule sous forme CNF est une conjonction de clauses
Existe-t-il une interpr´etation des variables qui satisfait l’ensemble des
clauses ?
Exemple :
¬x ∨ ¬x ∨ x Variable x x x1 2 31 2 3
x ∨ x Vrai2 3
x ∨ ¬x Faux1 2
•Page 3 / 46 •First •Prev •Next •Last