Schedule

• Info is available on the S2 schedule

Teachers

• Antoine Gontard (antoine.gontard@inria.fr)
• Raphaël Berthon (rberthon@lmf.cnrs.fr)

Part 1: SAT exercises

• Exercise sheet
• Skeleton files
• Sudoku missing file
• Ocamlc makefile (without print)

Part 2 : Rocq tutorial

• Sheet

Evaluation

Out of 20 total points for this course:

• 3 come from the SAT exercises (Due February 8th)
• 10 come from the Rocq project (Due April 19th)
• 7 come from the DPLL project (Due May 10th)

Aknowledgement

This iteration of the course is strongly inspired by the 2024-25 iteration by Nicolas Margulies and Théo Vignon, itself strongly inspired by the 2020-21 iteration by David Baelde.