Générateur de colloscope via SAT Solver

Objectifs et Impact

En discutant avec mes professeurs de classe préparatoire, j'ai réalisé que la création du colloscope était un véritable cauchemar logistique. Les premières versions faites à la main comportaient très souvent des erreurs (chevauchements d'horaires, conflits de salles ou de professeurs).

Pour une classe de 48 élèves (16 groupes) avec des contraintes de roulement complexes (matières hebdomadaires vs quinzaines), la planification manuelle peut prendre un week-end entier. Mon solveur réduit ce temps de calcul à 5-10 minutes, tout en garantissant un planning mathématiquement parfait et sans aucun conflit.

Au-delà de l'utilité de l'outil, c'était un excellent exercice pour comprendre profondément la logique propositionnelle. Modéliser un problème concret en clauses CNF est une porte d'entrée fascinante vers des concepts d'algorithmique plus avancés, comme les solveurs SMT (Satisfiability Modulo Theories), qui sont au cœur de la vérification formelle aujourd'hui.

Source

Le problème

Un colloscope répartit les groupes d'étudiants sur les créneaux de colle de chaque colleur. Il doit respecter un ensemble de contraintes croisées : un colleur ne peut interroger qu'un seul groupe à la fois, un groupe ne peut pas être à deux endroits au même moment, et chaque groupe doit passer dans chaque matière sur la période. Fait à la main, l'exercice demande plusieurs heures et le moindre changement de disponibilité oblige à tout reprendre.

Plutôt que d'écrire un algorithme spécifique au colloscope, le projet ramène le problème à SAT : trouver une affectation de valeurs vrai/faux qui satisfait une formule booléenne. Le planning n'est alors plus qu'une lecture de la solution renvoyée par le solveur.

Modélisation

À chaque combinaison possible correspond une variable booléenne : x(g, c, h) vaut vrai si le groupe g est interrogé par le colleur c au créneau h. La formule est écrite sous forme normale conjonctive (une conjonction de clauses, chaque clause étant une disjonction de littéraux), format attendu par le solveur.

1. Existence. Chaque groupe doit avoir une colle dans chaque matière : une clause qui liste toutes les variables acceptables pour ce couple groupe/matière.
2. Unicité. Deux variables ne peuvent pas être vraies en même temps si elles occupent le même colleur au même créneau, ou le même groupe au même créneau. Cela s'écrit comme un ensemble de clauses à deux littéraux négatifs, de la forme ¬a ∨ ¬b.
3. Disponibilités. Un colleur absent à un créneau élimine simplement les variables correspondantes : elles sont forcées à faux.

Concrètement, une variable est un entier : 3 désigne la variable numéro 3, et -3 sa négation. Une clause est une liste d'entiers, et la formule une liste de clauses.

type variable = int
type fnc_t = variable list list      (* [[1; -2]; [2; 3]] = (x1 ∨ ¬x2) ∧ (x2 ∨ x3) *)
type solution_t = variable array     (* 1 = vrai, -1 = faux, 0 = non affectée *)

Le tableau solution est indexé par le numéro de variable ; la case 0 n'est jamais utilisée.

Le solveur (DPLL)

Le solveur suit l'algorithme DPLL : un parcours en profondeur de l'espace des affectations, allégé à chaque étape par des simplifications logiques.

1. Propagation unitaire. var_clause_uni cherche une clause réduite à un seul littéral. Cette clause ne laisse aucun choix : la variable est affectée immédiatement.
2. Simplification. remove_clause_with_known_uni propage cette valeur : toute clause contenant le littéral est déjà satisfaite et disparaît, et le littéral opposé est retiré des clauses restantes. Si une clause se vide, c'est une contradiction et Unsatisfiable est levée.
3. Pari. S'il ne reste aucune clause unitaire, choose_var prend la première variable encore libre et le solveur la suppose vraie, avant de relancer la propagation.
4. Retour arrière. Si cette branche échoue, l'exception est rattrapée et la variable est réessayée à faux sur une copie propre du tableau solution. Si les deux branches échouent, l'échec remonte d'un niveau.

L'arrêt se fait dans les deux sens : plus aucune clause à satisfaire, et la solution courante est renvoyée ; une clause vide, et la formule est insatisfiable. Ce dernier cas est informatif en pratique : il signifie que les disponibilités fournies ne permettent tout simplement pas de construire un colloscope valide.

Chaîne complète

Le solveur n'est qu'un maillon. Le programme lit un CSV de disponibilités (créneau, nom du colleur, matière), le traduit en formule, résout, puis reconstruit un planning lisible.

1. input.ml analyse le CSV : liste des colleurs sans doublon (les noms sont normalisés pour que « M. Dupont » et « M.Dupont » ne comptent qu'une fois), liste des créneaux, matière de chaque colleur, et pour chaque colleur la liste des créneaux où il est disponible.
2. Properly_sat.ml contient le solveur et renvoie le tableau des variables affectées.
3. output.ml relit ce tableau et remet les indices sous forme de noms, d'horaires et de groupes.
4. colloscope_generator.py fournit l'interface : choix du fichier, lancement du moteur OCaml compilé, puis export en .xlsx avec un code couleur par groupe.

Utilisation

# Compilation du moteur OCaml
$ ocamlfind ocamlopt -o colloscope -linkpkg -package csv,unix \
      Properly_sat.ml input.ml output.ml final_input_version.ml

# Interface graphique (Python 3.10+, environnement virtuel conseillé)
$ pip install pandas customtkinter xlsxwriter pyinstaller
$ python3 colloscope_generator.py

Le CSV d'entrée attend trois colonnes : horaire, nom du colleur, matière. Le calcul prend de 10 secondes à 1 minute selon la taille du problème.

Le code complet est sur GitHub.

Code source

type variable = int
type solution_t = variable array
type fnc_t = variable list list

exception Unsatisfiable
exception Satisfiable

let rec empty_in (fnc : fnc_t) =
  match fnc with
  | [] -> false
  | h :: t when h = [] -> true
  | h :: t -> empty_in t

let choose_var (fnc : fnc_t) (solution : solution_t) =
  (* Search the unassigned variable *)
  let rec find_var_in_clauses = function
    | [] -> raise Unsatisfiable
    | clause :: rest ->
      match List.find_opt (fun x -> solution.(abs x) = 0) clause with
      | Some v -> abs v
      | None -> find_var_in_clauses rest
  in
  find_var_in_clauses fnc

let var_clause_uni (fnc : fnc_t) =
  let rec find_uni = function
    | [] -> 0
    | clause :: rest ->
      match clause with
      | [x] -> x
      | _ -> find_uni rest
  in
  find_uni fnc

let abs (x : variable) =   (* return the absolute value of x *)
  if x < 0 then (-x)
  else x

let rec list_parcours (l : variable list) (x : variable) =
  (* parcours of the fnc, if x is in the clause, then return true. *)
  match l with
  | [] -> false
  | h :: t when h = x || h = -x -> true
  | _ :: t -> list_parcours t x

let rec remove_clause_with_known_uni (fnc : fnc_t) (x : variable) =
  (* Remove all clauses where x is in it, and delete -x from all other clauses. *)
  match fnc with
  | [] -> []
  | clause :: rest ->
    if List.exists (fun lit -> lit = x) clause then
      remove_clause_with_known_uni rest x
    else
      let cleaned_clause = List.filter (fun lit -> lit <> -x) clause in
      if cleaned_clause = [] then
        raise Unsatisfiable
      else
        cleaned_clause :: remove_clause_with_known_uni rest x

let simplify_clause_uni (fnc : fnc_t) (sol : solution_t) =
  (* remove all the unit clause and set the value of each variable of those unit clause *)
  let var = var_clause_uni fnc in
  let new_fnc = ref [] in
  if (var != 0) then begin
    sol.(abs var) <- var ;
    new_fnc := (remove_clause_with_known_uni fnc var)
  end else
    new_fnc := fnc;
  !new_fnc

let rec simplify_all_unit_clauses (fnc : fnc_t) (sol : solution_t) =
  let var = var_clause_uni fnc in
  if var != 0 then
    let new_fnc = remove_clause_with_known_uni fnc var in
    sol.(abs var) <- if var > 0 then 1 else -1;   (* Set 1 for true, -1 for false *)
    simplify_all_unit_clauses new_fnc sol          (* Continue until there is no more unit clauses left *)
  else
    fnc

let get_max_var_index (fnc : fnc_t) =
  fnc
  |> List.flatten              (* concatenate all clauses in one *)
  |> List.map abs              (* apply the absolute value on each variable *)
  |> List.fold_left max 0      (* find the maximum value in the list *)

(* return sol in which the value at the index 0 is always 0,
   because the variable 0 is never used in propositional logic *)
let simplify_fnc (fnc : fnc_t) =
  if empty_in fnc then raise Unsatisfiable;
  let max_idx = get_max_var_index fnc in
  let sol_init = Array.make (max_idx + 1) 0 in

  (* Initial unit propagation *)
  let cleaned_fnc = simplify_all_unit_clauses fnc sol_init in

  let rec solve current_fnc current_sol =
    (* VICTORY CASE: No more clauses to fulfill *)
    if current_fnc = [] then
      current_sol
    (* DEFEATED CASE: An empty clause (contradiction) has been generated. *)
    else if empty_in current_fnc then
      raise Unsatisfiable
    else
      let x =
        try choose_var current_fnc current_sol
        with Unsatisfiable -> raise Unsatisfiable
      in
      try
        let sol_vrai = Array.copy current_sol in
        sol_vrai.(x) <- 1;
        let next = remove_clause_with_known_uni current_fnc x in
        let simplified = simplify_all_unit_clauses next sol_vrai in
        solve simplified sol_vrai
      with Unsatisfiable ->
        (* backtracking *)
        let sol_faux = Array.copy current_sol in
        sol_faux.(x) <- -1;
        let next = remove_clause_with_known_uni current_fnc (-x) in
        let simplified = simplify_all_unit_clauses next sol_faux in
        solve simplified sol_faux
  in
  solve cleaned_fnc sol_init