Informations générales

Équipe enseignante

• Chargé de cours : Benjamin Wack
• groupe INM-01 : Astor Bizard
• groupe INM-02 : Cristian Ene
• groupe INM-03 : Matthieu Petiteau
• groupe MIN-01 : Cristian Ene
• groupe MIN-03 : Benjamin Gaudin
• groupe MAT-02 : François Puitg
• group MIN-int: Aleksei Gorelov

Supports de cours

• Poly de cours et d'exercices

Évaluation

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

Projet

• 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é

• Sujet du projet

Autres documents liés au projet

• Grille indicative de notation
• Aide pour le format Dimacs
• Aide pour la réduction SAT vers 3-SAT.

Des idées de problèmes bien adaptés à ce projet

• Facile :
  • Easy as ABC
  • Mosaic
  • No four in a row
  • Gappy
  • Eulero
  • Numbrix
• Moyen :
  • Magnets
  • Bricks
  • Norinori
  • Makaro
  • Certains des problèmes mentionnés dans ce fichier ou sur cette page (consulter votre enseignant pour vérifier la faisabilité)
• Difficile :
  • Juosan
  • Tents
  • Light Up
  • Usowan
  • Hitori
  • Kurotto
  • Tetravex
• Des sujets à éviter, pour des raisons théoriques ou par expérience :
  • Traité trop de fois : Tout noir tout blanc, Dosun-Fuwari, Hashiwokakero, N reines, Squaro, coloration de graphes, Sudoku, Takuzu, Futoshiki
  • Possible mais très ardu : Camping, Antimorpion, Nonogram
  • Problème mal adapté à une modélisation statique : solitaire, dames, échecs, go, taquin, master mind
  • Nécessité de calculs arithmétiques, pénibles à modéliser : Kakuro