École d'été | 10 juin 2026 : Bridging Theory and Practice with SAT and MaxSAT par Ruben Martins

Valeur des informations & solidité de l’argumentation

La valeur des informations est élevée pour un public non spécialiste : l’orateur démystifie SAT en montrant que malgré sa complexité théorique, il est utilisable en pratique. L’argumentation est solide, appuyée par des exemples concrets (installation de paquets, planification) et des démonstrations interactives. La progression pédagogique est bien pensée : des bases (définitions, CNF) vers des techniques avancées (CDCL) puis vers l’optimisation (MaxSAT). L’accent mis sur l’importance de la modélisation est pertinent. Cependant, certains aspects techniques (comme l’apprentissage de clauses) sont survolés, ce qui limite la profondeur pour un public averti. La présentation est convaincante et encourage à utiliser ces outils.

Rigueur scientifique, qualité des sources, adéquation du titre

La rigueur scientifique est bonne : les concepts sont correctement définis et les algorithmes expliqués avec précision. L’orateur cite des références reconnues comme le Handbook of Satisfiability (2e édition, 2021) et le livre de Donald Knuth sur SAT, ce qui renforce la crédibilité. Cependant, aucune source détaillée n’est fournie dans la description, ce qui limite la vérifiabilité. Le titre est fidèle au contenu : il annonce le pont entre théorie et pratique, et la présentation tient cette promesse. L’adéquation titre/contenu est donc bonne.

Le titre reflète bien le contenu : la présentation établit le pont entre la théorie (SAT, MaxSAT) et la pratique (modélisation, solveurs).

8/10

Exposé clair et structuré par un chercheur reconnu, couvrant les fondamentaux de SAT et MaxSAT avec des exemples concrets. Les concepts sont présentés avec rigueur, bien que le niveau reste introductif. Les sources mentionnées (handbook, Knuth) sont fiables, mais aucune référence détaillée n'est fournie dans la description.

Repères établis par PSI à partir de la transcription : le créateur n'a pas défini de chapitres.

• 00:00Introduction par l'organisateur, présentation de Ruben Martins.
• 01:00Début de l'exposé : applications du raisonnement automatisé, importance de SAT.
• 05:00Définition de SAT, terminologie (variables, littéraux, clauses, CNF).
• 10:00Présentation de l'algorithme DPLL et de la propagation unitaire.
• 15:00Exemple interactif de résolution avec le jeu SAT.
• 20:00Introduction à l'apprentissage de clauses par conflit (CDCL).
• 30:00Évolution des solveurs SAT, graphique cactus, améliorations.
• 40:00Modélisation d'un problème réel : installation de paquets logiciels.
• 50:00Introduction à MaxSAT, clauses dures et molles, applications.
• 1:00:00Exemples d'applications : Eclipse, localisation d'erreurs, planification de mariage.

• Handbook of Satisfiability (2nd edition) — Référence mentionnée comme ouvrage de référence sur SAT.
• The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability — Livre de Donald Knuth consacré à SAT, cité comme source d'inspiration.

• Handbook of Satisfiability — Ouvrage de référence cité par l'orateur, couvrant l'état de l'art sur SAT.
• The Art of Computer Programming, Volume 4, Fascicle 6 — Livre de Donald Knuth, qui a consacré un fascicule à SAT, confirmant l'importance du sujet.