Soutenance these

R´esolution du probl`eme SATetG´en´eration de Mod`eles finis en logiquedu premier ordreGilles AudemardLe 25 octobre 2001Pr´epar´ee au sein du LIM•Page 1 / 46 •First •Prev •Next •LastPlanLe probl`eme SAT• D´efinitions• Production de litt´eraux• La m´ethode Aval• Exp´erimentations•Page 2 / 46 •First •Prev •Next •LastPlanLe probl`eme SAT• D´efinitions• Production de litt´eraux• La m´ethode Aval• Exp´erimentationsG´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 SATUn ensemble de variables {x ,...,x }1 n•Page 3 / 46 •First •Prev •Next •LastLe probl`eme SATUn 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 SATUn 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 SATUn 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 SATUn ensemble de variables ...