-
Notifications
You must be signed in to change notification settings - Fork 3
/
916.tex
134 lines (106 loc) · 4.25 KB
/
916.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
\documentclass{agregfiche}
\title{Leçon 916 -- Formules du calcul propositionnel : Représentation, formes
normales, satisifiabilité. Applications.}
\begin{document}
\maketitle
\secrapports
\begin{rapport}{2017,2018,2019}
Le jury attend des candidats qu'ils abordent les questions de la complexité de la satisfiabilité. Pour autant, les applications ne sauraient se réduire à la réduction de problèmes NP-complets à SAT. Une partie significative du plan doit être consacrée à la représentation des formules et à leurs formes normales.
\end{rapport}
\secindispensables
\begin{itemize}
\item Syntaxe et la sémantique des propositions, tables de vérité.
\item Formes normales (CNF, DNF, BDD),
\item Les méthodes syntaxiques de preuve. (déduction naturelle,
calcul des séquents, résolution)
\item Validité, satisfiabilité.
\end{itemize}
\secasavoir
\begin{itemize}
\item Complétude du calcul propositionnel.
\item Les méthodes sémantiques de preuve (DPLL, tableau,
table de vérité, BDD).
\item Complexité ave SAT, 3SAT, HORNSAT, et 2SAT.
\item Système de connecteurs, complétude (le XOR est complet).
pour chacune la complexité des problèmes de décision,
et du passage d'une forme à l'autre. (pour la validité ? pour la
satisfiabilité ?)
\end{itemize}
\secidees
\begin{itemize}
\item Le théorème de compacité.
% (validé par le jury en 2018)
\item L'étude du fragment propositionnel
via Herbrand.
\item La résolution au premier ordre.
\item Applications des SAT solvers
(HAMPATH, Sudoku, coloration de graphes, crack de MD5).
Attention les réductions sont \emph{à l'envers} !
% \item Affirmer plus de choses sur les BDD (représentation mémoire
% via hash-consing,
% étude de cas pathologiques).
% \item Passer plus de temps sur les systèmes complets, les
%problèmes sont-ils
% plus ou moins durs en fonction du système de connecteur
%choisi~?
\item Génération de circuits.
\item Application de HORNSAT aux gestions de dépendances (analyse
syntaxique, transformation d'automates et grammaires)
\end{itemize}
\secpieges
\begin{itemize}
\item Ne pas centrer toute la leçon sur $NP$.
\item Faire une grosse partie sur les formes normales, leurs avantages
et leurs inconvénients (vitesse, conversion).
\item Bien comparer les méthodes de résolution, leurs avantages et leurs
inconvénients (vitesse, certificat).
\item Différents livres peuvent avoir des notations
différentes ($\neg T, \overline{T}$), rester cohérent.
\item Ne pas oublier les applications.
\end{itemize}
\secquestionsclassiques
\begin{itemize}
\item Pourquoi fait-on tout en CNF alors que la DNF possède de meilleures
propriétés ?
% On peut trouver une formule équisatisfiable en 3CNF en temps linéaire
\item En utilisant un SAT solveur, on doit écrire une traduction, quelle
est la condition nécessaire et suffisante sur le problème pour que ce soit
possible ?
\item Quel est l'algorithme pour résoudre HORNSAT en temps linéaire ?
Quelles applications ?
\item Donner un exemple de formule pour laquelle le BDD est de
taille
exponentielle.
\item Comparer la résolution, DPLL et les autres méthodes ?
\item Combien de résolutions pour prouver $\bot$ ?
\item Comment utiliser la résolution pour résoudre $2SAT$ en temps polynomial ?
\end{itemize}
\secreferences
\begin{itemize}
\item \input{refs/goubault}
\item \input{refs/corilascar}
\item \input{refs/david}
\item \input{refs/dowek}
% \item \temporary{Goubault}
% \item \temporary{Cori Lascar 1/2}
% \item \temporary{Raffali}
% \item \temporary{René Lalement}
\end{itemize}
\secdev
\begin{itemize}
% \item \temporary{Compacité du calcul propositionnel et
%application}
%% \item \temporary{2SAT est $NL$-complet et en temps linéaire sur
%%une
%% machine RAM}
% \item \temporary{Complétude de la résolution propositionnelle}
\item[++] \input{dev/cook}
\item[++] \input{dev/2SAT}
\item[++] \input{dev/resolution}
\item[++] \input{dev/CNFformula}
\end{itemize}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: