Résumé de section

    • Merci de vous inscrire dans un des groupes de travail ci-dessous. Effectifs mini/maxi = 3/4.

      En cas de non-inscription (ou de monôme ou de binôme), sauf cas particulier vu avec votre enseignant de TD, vous pourrez être affecté d'office à un groupe.

    • Pour les étudiants d'INM-3, merci de vous reporter au module de dépôt de votre groupe.

      Rappels

      Votre rapport doit au minimum :

      • Présenter le problème choisi en français : règles, contraintes et plusieurs exemples ;
      • Spécifier la formalisation de ce problème en logique ;
      • Fournir une FNC avec le détail des calculs pour y arriver.
      Votre code doit comporter :
      • les fichiers sources de vos programmes, commentés à bon escient
      • les instructions pour les compiler et/ou les exécuter (où trouver le SAT-solveur utilisé, README et/ou Makefile selon le langage de programmation utilisé, script pour enchaîner les différents programmes)
      • une description du format d'entrée attendu par vos programmes
      • une série pertinente d'exemples d’instances de votre problème
    • Équipe enseignante

      Supports de cours

      Évaluation

      • 10% Quicks (brèves interros durant les TDs)
      • 20% Partiel
      • 30% Projet
      • 40% Examen

      Projet

      Par groupes de 3 (éventuellement 4)
      • Phase 1 : Modélisation en forme normale conjonctive d'un problème de votre choix
      • Phase 2 : Programmation d'une interface logicielle pour traduire automatiquement tout instance de ce problème au format Dimacs  et utilisation d'un SAT solveur pour résoudre le problème
      • Optionnel : Mise au format 3-SAT et écriture d'un SAT solveur (non-déterministe)
      Sujet détaillé
      Autres documents liés au projet
      Des idées de problèmes bien adaptés à ce projet