General information

Teaching team

• Lectures: 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

Teaching material

• English handout

Evaluation

• 10% Quicks tests (during TDs)
• 20% Midterm
• 30% Project
• 40% Exam

Project

• Phase 1 : Modelization the problem your choose in conjunctive normal form
• Phase 2 : Programming a software interface for converting automatically any instance of that problem into Dimacs format and using a SAT solver to solve the problem
• Optional : Transformation into 3-SAT format and programming of a (non-deterministic) SAT solver

Detailed subject

• English project description

Other documents for the project

• Grading indications
• Help for the Dimacs format
• Help for reduction SAT to 3-SAT.

Problem ideas suitable for this project

• Easy:
  • Easy as ABC
  • Mosaic
  • No four in a row
  • Gappy
  • Eulero
  • Numbrix
• Intermediate:
  • Magnets
  • Bricks
  • Norinori
  • Makaro
  • Some of the problems listed in this file or on that page (check feasability with your teacher)
• Hard:
  • Juosan
  • Tents
  • Light Up
  • Usowan
  • Hitori
  • Kurotto
  • Tetravex
• Problems to be avoided:
  • Studied too often: Tout noir tout blanc, Dosun-Fuwari, Hashiwokakero, N reines, Squaro, graph colouring, Sudoku, Takuzu, Futoshiki
  • Possible but really tricky: Camping, Antimorpion, Nonogram
  • Unsuitable for a static modelization: solitaire, draughts, chess, go, 15 puzzle, master mind
  • Requires arithmetic computations: Kakuro