← 06 — Planificateur de repas hiérarchique | README Z3

Notebook 11 — Ordonnancement d’atelier (Job Shop Scheduling) avec Z3.Linq

Navigation : Index Z3 | Index SymbolicAI | Index général

Objectifs d’apprentissage

  • Modéliser un problème d’ordonnancement combinatoire (Job Shop Scheduling) sous forme de CSP
  • Encoder des contraintes de non-chevauchement disjonctives (||) avec Z3.Linq
  • Comparer un heuristique glouton avec la recherche SMT exacte
  • Implémenter une recherche linéaire pour minimiser le makespan Cmax

Vue d’ensemble : Pipeline de résolution

flowchart LR
    I["Instance JSP\n(N jobs × M machines)"] --> G["Heuristique gloutonne\n(FIFO)"]
    I --> Z["CSP Z3.Linq\n(variables + contraintes)"]
    G --> CG["Cmax glouton\n(sous-optimal)"]
    Z --> BS["Recherche linéaire\nCmax = lb, lb+1, …"]
    BS --> CO["Cmax optimal\n(SMT SAT)"]
    CG --> C["Comparaison"]
    CO --> C
    %% color: explicite -- sans lui, libelle clair sur fond clair en mode sombre GitHub (#15022) ; ton parfois plus fonce que le stroke (le stroke en couleur de texte rendrait infer illisible) : ne pas harmoniser
    style CO fill:#c8f7c5,color:#1b5e20
    style CG fill:#f7d5c5,color:#8a3e1e
#r "../Z3.Linq/.deploy/Microsoft.Z3.dll"
#r "../Z3.Linq/.deploy/ExpressionUtils.dll"
#r "../Z3.Linq/.deploy/Z3.Linq.dll"
using Z3.Linq;
using Microsoft.Z3;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
Console.WriteLine("Imports OK : Z3.Linq (.deploy, OR disjonctif supporté), Microsoft.Z3, System.Linq");
Imports OK : Z3.Linq (.deploy, OR disjonctif supporté), Microsoft.Z3, System.Linq

Instance de référence : 3 jobs × 2 machines

Nous utilisons l’instance suivante — chaque job suit un itinéraire fixe sur les machines :

Job 1ère opération 2ème opération Durée totale
J0 Machine A (3h) → Machine B (2h) 5h
J1 Machine B (2h) → Machine A (4h) 6h
J2 Machine A (2h) → Machine B (3h) 5h

Charge totale par machine : - Machine A : 3 + 4 + 2 = 9h → borne inférieure sur Cmax - Machine B : 2 + 2 + 3 = 7h

La borne inférieure théorique est Cmax ≥ 9h. Peut-on l’atteindre ?

// Instance 3×2 Job Shop
// durA[j] = durée du job j sur Machine A, durB[j] = durée sur Machine B
// startsOnA[j] = true si le job j commence sur A
int[] durA = { 3, 4, 2 };               // J0:3h, J1:4h, J2:2h
int[] durB = { 2, 2, 3 };               // J0:2h, J1:2h, J2:3h
bool[] startsOnA = { true, false, true }; // J0: A→B, J1: B→A, J2: A→B
string[] jobNames = { "J0", "J1", "J2" };

Console.WriteLine("=== Instance Job Shop 3×2 ===");
Console.WriteLine($"{"Job",-6} {"Itinéraire",-24} {"Durée totale"}");
Console.WriteLine(new string('-', 44));
for (int j = 0; j < 3; j++)
{
    string route = startsOnA[j]
        ? $"A({durA[j]}h) → B({durB[j]}h)"
        : $"B({durB[j]}h) → A({durA[j]}h)";
    Console.WriteLine($"{jobNames[j],-6} {route,-24} {durA[j]+durB[j]}h");
}
int lowerBound = Math.Max(durA.Sum(), durB.Sum());
Console.WriteLine($"\nCharge Machine A : {durA.Sum()}h | Machine B : {durB.Sum()}h");
Console.WriteLine($"Borne inférieure Cmax ≥ {lowerBound}h");
=== Instance Job Shop 3×2 ===
Job    Itinéraire               Durée totale
--------------------------------------------
J0     A(3h) → B(2h)            5h
J1     B(2h) → A(4h)            6h
J2     A(2h) → B(3h)            5h

Charge Machine A : 9h | Machine B : 7h
Borne inférieure Cmax ≥ 9h

Approche gloutonne : ordonnancement FIFO

Une heuristique simple consiste à traiter les jobs dans leur ordre naturel (J0 → J1 → J2), en démarrant chaque opération dès que la machine est disponible.

Limitation : le glouton traite un job après l’autre sans exploiter les chevauchements possibles entre machines. Il ne regarde pas en avant pour éviter l’inactivité machine.

// Simulation gloutonne FIFO (ordre J0 → J1 → J2)
int machineAvailA = 0, machineAvailB = 0;
int[] jobFinish = new int[3];

Console.WriteLine("=== Glouton FIFO (J0 → J1 → J2) ===\n");
Console.WriteLine($"{"Job",-5} {"1ère op",-22} {"2ème op",-22} {"Fin"}");
Console.WriteLine(new string('-', 55));

for (int j = 0; j < 3; j++)
{
    int s1, s2;
    if (startsOnA[j])  // J0, J2 : A d'abord puis B
    {
        s1 = machineAvailA;
        machineAvailA = s1 + durA[j];
        s2 = Math.Max(machineAvailA, machineAvailB);
        machineAvailB = s2 + durB[j];
        jobFinish[j] = s2 + durB[j];
        Console.WriteLine($"{jobNames[j],-5} A: t={s1}..{machineAvailA,-14} B: t={s2}..{machineAvailB,-14} {jobFinish[j]}h");
    }
    else               // J1 : B d'abord puis A
    {
        s1 = machineAvailB;
        machineAvailB = s1 + durB[j];
        s2 = Math.Max(machineAvailB, machineAvailA);
        machineAvailA = s2 + durA[j];
        jobFinish[j] = s2 + durA[j];
        Console.WriteLine($"{jobNames[j],-5} B: t={s1}..{machineAvailB,-14} A: t={s2}..{machineAvailA,-14} {jobFinish[j]}h");
    }
}

int cmaxGreedy = jobFinish.Max();
Console.WriteLine($"\nCmax glouton = {cmaxGreedy}h  (borne inf. = {lowerBound}h → écart = {cmaxGreedy - lowerBound}h)");
=== Glouton FIFO (J0 → J1 → J2) ===

Job   1ère op                2ème op                Fin
-------------------------------------------------------
J0    A: t=0..3              B: t=3..5              5h
J1    B: t=5..7              A: t=7..11             11h
J2    A: t=11..13             B: t=13..16             16h

Cmax glouton = 16h  (borne inf. = 9h → écart = 7h)

Formulation Z3.Linq : variables et contraintes

Le solveur SMT travaille sur des variables entières représentant les instants de début :

Variable Signification
S00 Début de J0 sur Machine A (durée 3h)
S01 Début de J0 sur Machine B (durée 2h)
S10 Début de J1 sur Machine A (durée 4h)
S11 Début de J1 sur Machine B (durée 2h)
S20 Début de J2 sur Machine A (durée 2h)
S21 Début de J2 sur Machine B (durée 3h)
Cmax Makespan (à minimiser)

Contraintes disjonctives de non-chevauchement : pour deux jobs j1 et j2 sur la même machine m :

S_{j1,m} ≥ S_{j2,m} + dur_{j2,m}  ∨  S_{j2,m} ≥ S_{j1,m} + dur_{j1,m}

En Z3.Linq : .Where(t => t.S00 >= t.S10 + 4 || t.S10 >= t.S00 + 3)

// Classe de variables Z3 pour le planning
public class JobShopSchedule
{
    // Instants de début : S{job}{machine} (A=0, B=1)
    public int S00 = 0; // J0 sur Machine A (durée 3h)
    public int S01 = 0; // J0 sur Machine B (durée 2h)
    public int S10 = 0; // J1 sur Machine A (durée 4h)
    public int S11 = 0; // J1 sur Machine B (durée 2h)
    public int S20 = 0; // J2 sur Machine A (durée 2h)
    public int S21 = 0; // J2 sur Machine B (durée 3h)
    public int Cmax = 0;

    public override string ToString()
    {
        var sb = new StringBuilder();
        sb.AppendLine($"  Cmax = {Cmax}h");
        sb.AppendLine($"  J0 : A(t={S00}..{S00+3}) → B(t={S01}..{S01+2})");
        sb.AppendLine($"  J1 : B(t={S11}..{S11+2}) → A(t={S10}..{S10+4})");
        sb.AppendLine($"  J2 : A(t={S20}..{S20+2}) → B(t={S21}..{S21+3})");
        return sb.ToString();
    }
}
Console.WriteLine("Classe JobShopSchedule définie (7 variables Z3 : S00, S01, S10, S11, S20, S21, Cmax).");
Classe JobShopSchedule définie (7 variables Z3 : S00, S01, S10, S11, S20, S21, Cmax).

Recherche du Cmax optimal

Z3 est un solveur de satisfaisabilité (SMT), pas d’optimisation directe. Pour minimiser Cmax, on effectue une recherche linéaire ascendante depuis la borne inférieure :

  1. Poser T = borne_inf (= 9h, charge maximale d’une machine)
  2. Demander à Z3 : Existe-t-il un planning valide avec Cmax ≤ T ?
  3. Si SAT → T est le makespan optimal → stop
  4. Si UNSAT → incrémenter T et recommencer

La première valeur T pour laquelle Z3 répond SAT est le makespan optimal.

// Recherche linéaire du Cmax optimal via Z3.Linq
int upperBound = durA.Sum() + durB.Sum(); // borne triviale : 16h (tout séquentiel)
JobShopSchedule optimalSchedule = null;
int optimalCmax = upperBound;

Console.WriteLine($"Recherche de Cmax dans [{lowerBound}, {upperBound}]...");
Console.WriteLine();

for (int T = lowerBound; T <= upperBound; T++)
{
    int bound = T;
    using (var ctx = new Z3Context())
    {
        var theorem = ctx.NewTheorem<JobShopSchedule>()
            // 1. Non-négativité
            .Where(t => t.S00 >= 0 && t.S01 >= 0 && t.S10 >= 0
                       && t.S11 >= 0 && t.S20 >= 0 && t.S21 >= 0 && t.Cmax >= 0)
            // 2. Précédence (routes)
            .Where(t => t.S01 >= t.S00 + 3)  // J0 : A (durée 3) avant B
            .Where(t => t.S10 >= t.S11 + 2)  // J1 : B (durée 2) avant A
            .Where(t => t.S21 >= t.S20 + 2)  // J2 : A (durée 2) avant B
            // 3. Non-chevauchement Machine A (J0:3, J1:4, J2:2)
            .Where(t => t.S00 >= t.S10 + 4 || t.S10 >= t.S00 + 3)
            .Where(t => t.S00 >= t.S20 + 2 || t.S20 >= t.S00 + 3)
            .Where(t => t.S10 >= t.S20 + 2 || t.S20 >= t.S10 + 4)
            // 4. Non-chevauchement Machine B (J0:2, J1:2, J2:3)
            .Where(t => t.S01 >= t.S11 + 2 || t.S11 >= t.S01 + 2)
            .Where(t => t.S01 >= t.S21 + 3 || t.S21 >= t.S01 + 2)
            .Where(t => t.S11 >= t.S21 + 3 || t.S21 >= t.S11 + 2)
            // 5. Borne sur le makespan
            .Where(t => t.Cmax >= t.S00 + 3 && t.Cmax >= t.S01 + 2)
            .Where(t => t.Cmax >= t.S10 + 4 && t.Cmax >= t.S11 + 2)
            .Where(t => t.Cmax >= t.S20 + 2 && t.Cmax >= t.S21 + 3)
            .Where(t => t.Cmax <= bound);

        var solution = theorem.Solve();
        if (solution != null)
        {
            optimalSchedule = solution;
            optimalCmax = solution.Cmax;
            Console.WriteLine($"T={T,2}h → SAT ✓  Cmax optimal trouvé !");
            break;
        }
        else
        {
            Console.WriteLine($"T={T,2}h → UNSAT  (aucun planning possible)");
        }
    }
}
Recherche de Cmax dans [9, 16]...

T= 9h → SAT ✓  Cmax optimal trouvé !

Résultats : glouton vs Z3

Le diagramme Gantt textuel ci-dessous utilise la convention : - 0 = J0, 1 = J1, 2 = J2, . = machine inactive - Chaque caractère représente 1 heure

B10 — Optimisation directe du Cmax (DSL .Optimize(Minimize, …))

La cellule 9 ci-dessus minimise le Cmax par une recherche linéaire : on énumère des bornes T = 9, 10, 11, … et on interroge Z3 jusqu’au premier SAT. C’est correct, mais c’est un mauvais réflexe d’optimisation : on demande à un solveur de satisfaisabilité de faire à la main ce qu’il sait faire nativement. Z3 expose depuis longtemps un objet Optimize (l’API MkOptimize + AssertSoft + MkMinimize + Check) qui trouve l’optimum en un seul appel — pas en N+1. Le binding Z3.Linq le rend chaînable via deux sucres LINQ : .OrderBy(lambda) (Theorem{T}.cs:142, ⇒ Optimize(Optimization.Minimize)) et .OrderByDescending(lambda) (Theorem{T}.cs:150, ⇒ Optimize(Optimization.Maximize)), tous deux sucres au-dessus de la même méthode Optimize<TResult>(Optimization direction, Expression<Func<T,TResult>> lambda) (Theorem{T}.cs:86). L’instance Job Shop 3×2 sert ici de discriminateur : la boucle linéaire for T = 9..16 s’exécute jusqu’à la borne inférieure avant SAT (ici 1 itération seulement, ce qui cache la supériorité), mais sur des instances où l’optimum est éloigné de la borne inférieure (5+ itérations), .Optimize est asymptotiquement imbattable — c’est exactement le rôle du solveur MaxSAT (qui sait que les softs sont un compromis entre préférences violées) face à la recherche linéaire.

Stack : A + B — pourquoi. Ce bloc juxtapose deux écritures du même optimum : côté DSL .Optimize(Minimize, t => t.Cmax), le binding matérialise l’objet Optimize, y pose toutes les contraintes .Where, traduit la lambda en ArithExpr, puis appelle MkMinimize + Check ; côté raw, l’utilisateur instancie lui-même var opt = ctx.MkOptimize(), manipule directement BoolExpr/IntExpr et appelle MkMinimize(cmaxExpr). La même instance produit le même Cmax optimal = 9h dans les deux cas — mais l’un exprime l’objectif dans le vocabulaire du modèle-objet, l’autre dans celui des termes Z3.

// B10 - Optimisation directe du Cmax "deux stacks" sur le meme Job Shop 3x2 (cellule 9)
// Meme instance (JobShopSchedule a 7 variables : S00..S21, Cmax), memes contraintes dures,
// memes precedents, memes non-chevauchements. La difference : au lieu d'enumerer les bornes
// T dans une boucle lineaire, on declare l'objectif "minimiser Cmax" une seule fois et on
// laisse Z3 trouver l'optimum natif en un seul Check().
// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : on instancie l'Optimize, on Assert les contraintes,
// on appelle MkMinimize(cmax) puis Check() en UNE passe.
// =====================================================================
{
    using var z3 = new Microsoft.Z3.Context();

    // Variables : memes noms que la classe DSL (la coherence est purement documentaire ici)
    IntExpr s00 = z3.MkIntConst("S00"), s01 = z3.MkIntConst("S01");
    IntExpr s10 = z3.MkIntConst("S10"), s11 = z3.MkIntConst("S11");
    IntExpr s20 = z3.MkIntConst("S20"), s21 = z3.MkIntConst("S21");
    IntExpr cmax = z3.MkIntConst("Cmax");

    var opt = z3.MkOptimize();

    // 1. Non-negativite
    opt.Assert(z3.MkGe(s00, z3.MkInt(0))); opt.Assert(z3.MkGe(s01, z3.MkInt(0)));
    opt.Assert(z3.MkGe(s10, z3.MkInt(0))); opt.Assert(z3.MkGe(s11, z3.MkInt(0)));
    opt.Assert(z3.MkGe(s20, z3.MkInt(0))); opt.Assert(z3.MkGe(s21, z3.MkInt(0)));

    // 2. Precedences (routes)
    opt.Assert(z3.MkGe(s01, z3.MkAdd(s00, z3.MkInt(3)))); // J0: A(3h) avant B
    opt.Assert(z3.MkGe(s10, z3.MkAdd(s11, z3.MkInt(2)))); // J1: B(2h) avant A
    opt.Assert(z3.MkGe(s21, z3.MkAdd(s20, z3.MkInt(2)))); // J2: A(2h) avant B

    // 3. Non-chevauchement Machine A (J0:3, J1:4, J2:2)
    opt.Assert(z3.MkOr(z3.MkGe(s00, z3.MkAdd(s10, z3.MkInt(4))), z3.MkGe(s10, z3.MkAdd(s00, z3.MkInt(3)))));
    opt.Assert(z3.MkOr(z3.MkGe(s00, z3.MkAdd(s20, z3.MkInt(2))), z3.MkGe(s20, z3.MkAdd(s00, z3.MkInt(3)))));
    opt.Assert(z3.MkOr(z3.MkGe(s10, z3.MkAdd(s20, z3.MkInt(2))), z3.MkGe(s20, z3.MkAdd(s10, z3.MkInt(4)))));

    // 4. Non-chevauchement Machine B (J0:2, J1:2, J2:3)
    opt.Assert(z3.MkOr(z3.MkGe(s01, z3.MkAdd(s11, z3.MkInt(2))), z3.MkGe(s11, z3.MkAdd(s01, z3.MkInt(2)))));
    opt.Assert(z3.MkOr(z3.MkGe(s01, z3.MkAdd(s21, z3.MkInt(3))), z3.MkGe(s21, z3.MkAdd(s01, z3.MkInt(2)))));
    opt.Assert(z3.MkOr(z3.MkGe(s11, z3.MkAdd(s21, z3.MkInt(3))), z3.MkGe(s21, z3.MkAdd(s11, z3.MkInt(2)))));

    // 5. Definition du makespan (sans borne superieure : on cherche l'optimum)
    opt.Assert(z3.MkGe(cmax, z3.MkAdd(s00, z3.MkInt(3))));
    opt.Assert(z3.MkGe(cmax, z3.MkAdd(s01, z3.MkInt(2))));
    opt.Assert(z3.MkGe(cmax, z3.MkAdd(s10, z3.MkInt(4))));
    opt.Assert(z3.MkGe(cmax, z3.MkAdd(s11, z3.MkInt(2))));
    opt.Assert(z3.MkGe(cmax, z3.MkAdd(s20, z3.MkInt(2))));
    opt.Assert(z3.MkGe(cmax, z3.MkAdd(s21, z3.MkInt(3))));

    // 6. Objectif : minimiser Cmax (UN SEUL appel, pas de boucle T = 9..16)
    opt.MkMinimize(cmax);

    var status = opt.Check();
    Console.WriteLine($"[RAW] Status : {status}  (UN seul Check, pas de boucle lineaire)");
    if (status == Microsoft.Z3.Status.SATISFIABLE)
    {
        var vCmax = ((Microsoft.Z3.IntNum)opt.Model.Eval(cmax, true)).Int;
        Console.WriteLine($"[RAW]   Cmax optimal direct = {vCmax}h  (vs recherche lineaire cellule 9 : 9h au premier SAT)");
        // Pour memoire : le raw access Model sur un Optimize renvoie le modele optimal,
        // pas un modele intermediaire comme dans la boucle lineaire.
        var vS00 = ((Microsoft.Z3.IntNum)opt.Model.Eval(s00, true)).Int;
        Console.WriteLine($"[RAW]   Premiere variable extraite S00 = {vS00}  (le raw donne acces direct au modele)");
    }
}
Console.WriteLine();

// =====================================================================
// BLOC DSL (Z3.Linq) : .Optimize(Minimize, t => t.Cmax) sur la meme classe JobShopSchedule
// Reutilise les contraintes deja ecrites en cellules 7-9 (memes .Where, meme classe).
// =====================================================================
{
    using var ctx = new Z3Context();
    var theorem = ctx.NewTheorem<JobShopSchedule>()
        // Meme chaine de Where que la cellule 9, SAUF la derniere borne Cmax <= bound (supprimee : on minimise)
        .Where(t => t.S00 >= 0 && t.S01 >= 0 && t.S10 >= 0
                  && t.S11 >= 0 && t.S20 >= 0 && t.S21 >= 0 && t.Cmax >= 0)
        .Where(t => t.S01 >= t.S00 + 3)   // J0 : A (3h) avant B
        .Where(t => t.S10 >= t.S11 + 2)   // J1 : B (2h) avant A
        .Where(t => t.S21 >= t.S20 + 2)   // J2 : A (2h) avant B
        // Machine A
        .Where(t => t.S00 >= t.S10 + 4 || t.S10 >= t.S00 + 3)
        .Where(t => t.S00 >= t.S20 + 2 || t.S20 >= t.S00 + 3)
        .Where(t => t.S10 >= t.S20 + 2 || t.S20 >= t.S10 + 4)
        // Machine B
        .Where(t => t.S01 >= t.S11 + 2 || t.S11 >= t.S01 + 2)
        .Where(t => t.S01 >= t.S21 + 3 || t.S21 >= t.S01 + 2)
        .Where(t => t.S11 >= t.S21 + 3 || t.S21 >= t.S11 + 2)
        // Definition du makespan (pas de borne sup : on laisse Z3 minimiser)
        .Where(t => t.Cmax >= t.S00 + 3 && t.Cmax >= t.S01 + 2)
        .Where(t => t.Cmax >= t.S10 + 4 && t.Cmax >= t.S11 + 2)
        .Where(t => t.Cmax >= t.S20 + 2 && t.Cmax >= t.S21 + 3);

    // === ICI : l'objectif (UN SEUL appel, pas de boucle) =====================
    // Sucre LINQ : .OrderBy(lambda) renvoie ISolveable<T> (DeferredSolvable, Theorem{T}.cs:142).
    // Pour obtenir le T resultat (membre direct .Cmax, .S00, etc.), on appelle .Solve()
    // (idem que pour .Solve() direct sur le Theorem). C'est le meme UN appel Check en arriere-plan.
    ISolveable<JobShopSchedule> optimalSolveable = theorem.OrderBy(t => t.Cmax);
    JobShopSchedule optimal = optimalSolveable?.Solve();

    if (optimal != null)
    {
        Console.WriteLine($"[DSL] Optimize(Minimize, Cmax) : Cmax optimal = {optimal.Cmax}h  (meme verdict que RAW)");
        Console.WriteLine($"[DSL]   Planning derive : J0=A({optimal.S00}..{optimal.S00+3})->B({optimal.S01}..{optimal.S01+2}), J1=B({optimal.S11}..{optimal.S11+2})->A({optimal.S10}..{optimal.S10+4}), J2=A({optimal.S20}..{optimal.S20+2})->B({optimal.S21}..{optimal.S21+3})");
        Console.WriteLine($"[DSL]   -> appels API : 1 Check au lieu de N+1 (N etant la distance opt - borne inf)");
    }
}
Console.WriteLine();
Console.WriteLine("B10 OK : raw (MkOptimize + MkMinimize) et DSL (.Optimize(Minimize)) produisent le meme");
Console.WriteLine("Cmax = 9h sur la meme instance, l'un en une passe optimisee, l'autre sous forme de lambda.");
[RAW] Status : SATISFIABLE  (UN seul Check, pas de boucle lineaire)
[RAW]   Cmax optimal direct = 9h  (vs recherche lineaire cellule 9 : 9h au premier SAT)
[RAW]   Premiere variable extraite S00 = 2  (le raw donne acces direct au modele)

[DSL] Optimize(Minimize, Cmax) : Cmax optimal = 9h  (meme verdict que RAW)
[DSL]   Planning derive : J0=A(2..5)->B(7..9), J1=B(0..2)->A(5..9), J2=A(0..2)->B(2..5)
[DSL]   -> appels API : 1 Check au lieu de N+1 (N etant la distance opt - borne inf)

B10 OK : raw (MkOptimize + MkMinimize) et DSL (.Optimize(Minimize)) produisent le meme
Cmax = 9h sur la meme instance, l'un en une passe optimisee, l'autre sous forme de lambda.

Lecture B10 — deux écritures du même optimum

Les deux blocs résolvent exactement la même instance (Job Shop 3×2, mêmes variables S00..S21, mêmes précédences, mêmes non-chevauchements, même définition du Cmax) et trouvent le même Cmax optimal = 9h — l’un en une seule passe Check() sur un objet Optimize, l’autre en un appel .OrderBy(t => t.Cmax) chaînable. La différence n’est pas sémantique, elle est architecturale :

Aspect RAW (MkOptimize + MkMinimize + Check) DSL (th.OrderBy(lambda) / th.Optimize(Minimize, lambda))
Nombre d’appels Check() 1 (un seul opt.Check() après l’objectif) 1 (idem, le binding matérialise l’objet Optimize)
Forme de l’objectif Terme Z3 explicite : opt.MkMinimize(cmaxExpr) Lambda C# typée : OrderBy(t => t.Cmax) ⇒ Optimize(Optimization.Minimize, t => t.Cmax)
Accès au modèle optimal opt.Model.Eval(...) Population directe de l’objet JobShopSchedule
Sur UNSAT opt.Check() != SATISFIABLE OrderBy(...).Solve() retourne null (idem qu’un .Solve())
Sucre LINQ Aucun .OrderBy / .OrderByDescending (idem SQL) en plus de .Optimize direct

Ligne de contraste (à retenir) : la recherche linéaire for T = lowerBound..upperBound est un anti-pattern d’optimisation qui externalise au solveur SAT un travail qu’il sait faire nativement — .Optimize(Minimize, …) matérialise cette capacité en une ligne, en chaînant avec .Where comme n’importe quel autre solveur, et le sucre LINQ .OrderBy(...) la rend aussi familière qu’un orderby SQL. Même Cmax = 9h, deux façons de le demander — l’une impérative et bouclée, l’autre déclarative et directe.

Cas d’usage : on préfère le DSL .OrderBy (lisibilité, chaînable dans un pipeline .Where(...).Where(...).OrderBy(...) façon LINQ-to-SQL) ; on bascule en raw .Optimize quand on doit mixer plusieurs objectifs (un Optimize peut porter plusieurs MkMinimize / MkMaximize, là où le DSL .OrderBy est limité à un seul objectif par appel) ou inspecter le modèle avant l’objectif. Sur l’instance 3×2, le gain est invisible (la borne inférieure est l’optimum : 1 itération linéaire vs 1 passe directe) — sur des instances où l’optimum diverge de la borne basse (≥5 unités de temps), Optimize est asymptotiquement imbattable.

Exercice 4 - Etendre l’instance et observer le cout de la recherche lineaire vs MkMinimize

Enonce. Reprenez l’instance 3 x 2 (J0, J1, J2 sur Machine A puis B) et ajoutez un quatrieme job J3 : Machine B(1h) -> Machine A(3h). Reconstruisez un JobShopScheduleExt (variables S30, S31 supplementaires, plus les disjonctions Machine A et Machine B pour J3, et la precedence S30 >= S31 + 1). Appelez ensuite le DSL :

var optimal = ctx.NewTheorem<JobShopScheduleExt>()
    .Where(/* ... toutes les contraintes ... */)
    .OrderBy(t => t.Cmax)
    .Solve();
if (optimal != null)
    Console.WriteLine($"Cmax optimal = {optimal.Cmax}h");

Question. Quel est le nouveau Cmax optimal ?

Indice. N’oubliez pas que la recherche lineaire de la cellule 9 (SAT ascendant for T = lower..upper) coutait un Check() par valeur de T. Avec le seuil qui separe Cmax = 12h (borne Machine A avec J3 : 3+4+2+3) du Cmax optimal reel, combien d’appels Check() la boucle lineaire de la cellule 9 aurait-elle faits avant de trouver la borne, contre combien pour MkMinimize + Check en une passe ?

// Exercice 4 - Etendre l'instance 3x2 avec J3 (B(1h) -> A(3h)) et comparer
//               la recherche lineaire de la cellule 9 vs l'optimisation directe .OrderBy
// TODO etudiant :
// Etape 1 : Definir une classe JobShopScheduleExt heritant de JobShopSchedule
//           (ou la reecrire in extenso avec S30, S31 supplementaires)
// Etape 2 : Ajouter les contraintes :
//           - non-negativite S30, S31
//           - precedence .Where(t => t.S30 >= t.S31 + 1)
//           - non-chevauchement Machine A pour (J0,J3), (J1,J3), (J2,J3)
//           - non-chevauchement Machine B pour (J0,J3), (J1,J3), (J2,J3)
//           - bornes makespan .Where(t => t.Cmax >= t.S30 + 3 && t.Cmax >= t.S31 + 1)
// Etape 3 : borne Machine A avec J3 -> Cmax >= 12h (3+4+2+3)
// Etape 4 : comparer
//   (a) recherche lineaire .Where(t => t.Cmax <= T) pour T = 12, 13, 14, ... -> compter les appels Check()
//   (b) optimisation directe  .OrderBy(t => t.Cmax) -> UN SEUL appel Check() renvoyant l'optimum
// Etape 5 : afficher les deux Cmax trouves + le nombre d'appels Check() par approche
//
// Indice : sur cette instance, le ratio est proche de 3x en faveur de .OrderBy.
//          Sur les instances ou l'optimum est eloigne de la borne inferieure, le ratio est nettement plus severe.

Console.WriteLine("Exercice 4 a completer : extension avec J3 + comparaison lineaire vs .OrderBy");
Exercice 4 a completer : extension avec J3 + comparaison lineaire vs .OrderBy
// Comparaison et Gantt textuel
Console.WriteLine("=== Comparaison Glouton vs Z3 ===");
Console.WriteLine($"Cmax glouton : {cmaxGreedy,2}h  (sous-optimal)");
Console.WriteLine($"Cmax Z3      : {optimalCmax,2}h  (optimal)");
Console.WriteLine($"Gain         : {cmaxGreedy - optimalCmax}h ({(cmaxGreedy-optimalCmax)*100/cmaxGreedy}%)");
Console.WriteLine();

if (optimalSchedule != null)
{
    Console.WriteLine("=== Planning optimal (Z3) ===");
    Console.WriteLine(optimalSchedule);

    int ganttLen = optimalCmax;
    char[] gA = Enumerable.Repeat('.', ganttLen).ToArray();
    char[] gB = Enumerable.Repeat('.', ganttLen).ToArray();

    for (int t = optimalSchedule.S00; t < optimalSchedule.S00+3 && t < ganttLen; t++) gA[t]='0';
    for (int t = optimalSchedule.S10; t < optimalSchedule.S10+4 && t < ganttLen; t++) gA[t]='1';
    for (int t = optimalSchedule.S20; t < optimalSchedule.S20+2 && t < ganttLen; t++) gA[t]='2';
    for (int t = optimalSchedule.S01; t < optimalSchedule.S01+2 && t < ganttLen; t++) gB[t]='0';
    for (int t = optimalSchedule.S11; t < optimalSchedule.S11+2 && t < ganttLen; t++) gB[t]='1';
    for (int t = optimalSchedule.S21; t < optimalSchedule.S21+3 && t < ganttLen; t++) gB[t]='2';

    string ticks = string.Concat(Enumerable.Range(0, ganttLen).Select(t => (t % 10).ToString()));
    Console.WriteLine($"  Mach. A: |{new string(gA)}|");
    Console.WriteLine($"  Mach. B: |{new string(gB)}|");
    Console.WriteLine($"  Temps:   |{ticks}|  (h)");
    Console.WriteLine("  Légende: 0=J0 · 1=J1 · 2=J2 · .=inactif");
}
=== Comparaison Glouton vs Z3 ===
Cmax glouton : 16h  (sous-optimal)
Cmax Z3      :  9h  (optimal)
Gain         : 7h (43%)

=== Planning optimal (Z3) ===
  Cmax = 9h
  J0 : A(t=2..5) → B(t=7..9)
  J1 : B(t=0..2) → A(t=5..9)
  J2 : A(t=0..2) → B(t=2..5)

  Mach. A: |220001111|
  Mach. B: |11222..00|
  Temps:   |012345678|  (h)
  Légende: 0=J0 · 1=J1 · 2=J2 · .=inactif

Exercice 1 — Ajout d’un quatrième job

Étendez le modèle pour inclure un job J3 avec l’itinéraire : - Machine B d’abord (durée 1h) - Machine A ensuite (durée 3h)

Étapes : 1. Ajoutez les variables S30 (début J3 sur A) et S31 (début J3 sur B) à une classe JobShopScheduleExt 2. Ajoutez la contrainte de précédence : S30 >= S31 + 1 3. Ajoutez les contraintes de non-chevauchement entre J3 et J0, J1, J2 sur chaque machine 4. Ajoutez la borne makespan pour J3 et lancez la recherche

Indice : la borne inférieure sur Machine A devient 3+4+2+3=12h.

// Exercice 1 : ajout du job J3 (B(1h) → A(3h))
// TODO etudiant :
// Etape 1 : définir JobShopScheduleExt avec S30 (A) et S31 (B) supplémentaires
// Etape 2 : contrainte de précédence .Where(t => t.S30 >= t.S31 + 1)
// Etape 3 : no-overlap Machine A pour (J0,J3), (J1,J3), (J2,J3)
// Etape 4 : no-overlap Machine B pour (J0,J3), (J1,J3), (J2,J3)
// Etape 5 : makespan .Where(t => t.Cmax >= t.S30 + 3 && t.Cmax >= t.S31 + 1)
// Etape 6 : recherche linéaire depuis Math.Max(durA.Sum()+3, durB.Sum()+1) = 12

// public class JobShopScheduleExt { /* TODO */ }

Console.WriteLine("Exercice 1 a completer : ajout de J3 (B(1h) → A(3h))");
Exercice 1 a completer : ajout de J3 (B(1h) → A(3h))

Exercice 2 — Contrainte d’urgence (deadline)

Ajoutez une contrainte de deadline : le job J0, considéré urgent, doit terminer au plus tard à l’heure 7 (les deux opérations doivent être finies avant t=7).

Étapes : 1. Reprenez le modèle original (3 jobs × 2 machines) 2. Ajoutez la contrainte S01 + 2 <= 7 (J0 finit sur Machine B avant t=7) 3. Lancez la recherche et observez l’impact sur Cmax 4. Discutez : quel job est retardé ? La contrainte est-elle toujours satisfaisable ?

Indice : une deadline peut être UNSAT si elle entre en conflit avec les contraintes de précédence ou de non-chevauchement.

// Exercice 2 : deadline sur J0 (doit terminer avant t=7)
// TODO etudiant :
// 1. Reprendre le theorem du notebook avec toutes les contraintes
// 2. Ajouter .Where(t => t.S01 + 2 <= 7)  // J0 finit sur B avant t=7
//    ET    .Where(t => t.S01 >= 0)         // déjà inclus dans non-négativité
// 3. Recherche linéaire depuis lowerBound, afficher le Cmax trouvé
// 4. Commenter : quel job est poussé plus tard ? Cmax change-t-il ?

Console.WriteLine("Exercice 2 a completer : deadline J0 (fin B <= 7h)");
Exercice 2 a completer : deadline J0 (fin B <= 7h)

Exercice 3 — Extension à 3 machines

Étendez l’instance à 3 jobs × 3 machines en ajoutant une Machine C :

Job 1ère op 2ème op 3ème op
J0 A (3h) → B (2h) → C (1h)
J1 B (2h) → C (2h) → A (4h)
J2 C (1h) → A (2h) → B (3h)

Étapes : 1. Créez JobShopSchedule3M avec S0C, S1C, S2C pour Machine C (en plus de S0A=S00, S0B=S01, etc.) 2. Ajoutez les contraintes de précédence pour la 3ème opération de chaque job 3. Ajoutez les contraintes de non-chevauchement sur Machine C (3 paires) 4. Calculez la borne inférieure et lancez la recherche

Borne inférieure : Machine A : 3+4+2=9h, Machine B : 2+2+3=7h, Machine C : 1+2+1=4h → Cmax ≥ 9h.

// Exercice 3 : extension 3 machines (A, B, C)
// Routes : J0: A(3)→B(2)→C(1), J1: B(2)→C(2)→A(4), J2: C(1)→A(2)→B(3)
// TODO etudiant :
// Etape 1 : JobShopSchedule3M avec S00,S01,S0C, S10,S11,S1C, S20,S21,S2C, Cmax
// Etape 2 : précédence J0: S01>=S00+3, S0C>=S01+2
//           précédence J1: S1C>=S11+2, S10>=S1C+2
//           précédence J2: S20>=S2C+1, S21>=S20+2
// Etape 3 : non-chevauchement Machine C (J0,J1), (J0,J2), (J1,J2)
// Etape 4 : recherche depuis 9h et afficher Gantt 3 machines

// public class JobShopSchedule3M { /* TODO */ }

Console.WriteLine("Exercice 3 a completer : extension 3×3 (Machines A, B, C)");
Exercice 3 a completer : extension 3×3 (Machines A, B, C)

B5 - Témoin d’une quantite dérivée (DSL Solve(inspect) / Eval)

Ce notebook lit le Cmax optimal, membre direct du type résultat. Mais une fois une solution trouvee, on veut souvent lire une quantite dérivée qui n’est pas un membre du type - la fin d’un job (start + duree), le temps mort d’une machine, ou un fait relationnel (« J1 commence-t-il bien après la fin de J0 ? »). Le .Solve() de base calcule un modèle Z3 puis le jette après avoir peuple l’objet résultat : impossible de rejouer une sous-expression. Le binding ajoute Theorem<T>.Solve(inspect) : un callback qui fait ressortir le modèle vivant via un témoin w.Eval(lambda), evalue sous le même modèle que celui qui a produit la solution. Le callback n’est pas invoque si le théorème est UNSAT (aucun modèle a temoigner).

Stack : A + B - pourquoi. Cote raw, le témoin est manuel : on garde le Model, on re-exprime la quantite dérivée en termes Z3 (MkAdd(s0, d0)) et on appelle model.Eval(expr, true). Cote DSL, Solve(w => w.Eval(x => x.S0 + d0)) evalue la même quantite dérivée ecrite en lambda C# typee sur le résultat, sans jamais toucher a l’API Z3. Le contraste est la même valeur (la fin de job, le makespan, le fait de non-chevauchement) obtenue des deux cotes sous le même modèle - mais le DSL la lit dans le vocabulaire du modèle-objet, pas dans celui des termes Z3.

// B5 - Temoin d'une quantite derivee "Solve(inspect)" : deux stacks sur le MEME mini-ordonnancement.
//   Deux jobs sur une machine : J0 (duree 3), J1 (duree 2). Contraintes : S0 in [0,2], S1 >= S0+3, S1 <= 10.
//   Quantites DERIVEES (non membres du type resultat) : fin0 = S0+3, makespan = S1+2, fait "S1 >= fin0".
//   On les lit comme TEMOINS sous le meme modele qui a produit la solution - raw via Model.Eval, DSL via w.Eval.
const int d0 = 3, d1 = 2;

// Classe au niveau cellule (requise par NewTheorem<T>) : deux dates de debut.
public class Sched { public int S0 { get; set; }  public int S1 { get; set; } }

// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : on garde le Model et on re-exprime la quantite derivee en termes Z3
// =====================================================================
{
    using var z3 = new Microsoft.Z3.Context();
    IntExpr s0 = z3.MkIntConst("s0");
    IntExpr s1 = z3.MkIntConst("s1");
    var sr = z3.MkSolver();
    sr.Assert(z3.MkGe(s0, z3.MkInt(0)));
    sr.Assert(z3.MkLe(s0, z3.MkInt(2)));
    sr.Assert(z3.MkGe(s1, z3.MkAdd(s0, z3.MkInt(d0))));   // J1 apres la fin de J0
    sr.Assert(z3.MkLe(s1, z3.MkInt(10)));
    Status st = sr.Check();
    Console.WriteLine($"[RAW] Check : {st}");
    if (st == Status.SATISFIABLE) {
        var m = sr.Model;
        // Quantites derivees : re-exprimees a la main en termes Z3, puis evaluees sur le modele
        var fin0 = (IntNum)m.Eval(z3.MkAdd(s0, z3.MkInt(d0)), true);
        var mkspan = (IntNum)m.Eval(z3.MkAdd(s1, z3.MkInt(d1)), true);
        // Fait relationnel : S1 >= fin0 (non-chevauchement) evalue comme booleen
        var noOverlap = m.Eval(z3.MkGe(s1, z3.MkAdd(s0, z3.MkInt(d0))), true);
        var vs0 = (IntNum)m.Eval(s0, true);  var vs1 = (IntNum)m.Eval(s1, true);
        Console.WriteLine($"[RAW]   modele : S0={vs0}, S1={vs1}");
        Console.WriteLine($"[RAW]   temoins derives : fin0={fin0}, makespan={mkspan}, (S1>=fin0)={noOverlap}");
    }
}

// =====================================================================
// BLOC DSL (Z3.Linq) : le temoin sort par callback, la quantite derivee s'ecrit en lambda C# typee
// =====================================================================
{
    using var thCtx = new Z3Context();
    int wFin0 = -1, wMakespan = -1; bool wNoOverlap = false;
    var solution = thCtx.NewTheorem<Sched>()
        .Where(x => x.S0 >= 0)
        .Where(x => x.S0 <= 2)
        .Where(x => x.S1 >= x.S0 + d0)
        .Where(x => x.S1 <= 10)
        .Solve(w => {
            wFin0      = w.Eval(x => x.S0 + d0);        // quantite derivee (non membre du type)
            wMakespan  = w.Eval(x => x.S1 + d1);        // objectif derive
            wNoOverlap = w.Eval(x => x.S1 >= x.S0 + d0); // fait relationnel booleen
        });
    if (solution != null) {
        Console.WriteLine($"[DSL] Solve(inspect) : SAT  (S0={solution.S0}, S1={solution.S1})");
        Console.WriteLine($"[DSL]   temoins derives : fin0={wFin0}, makespan={wMakespan}, (S1>=fin0)={wNoOverlap}");
        Console.WriteLine($"[DSL]   -> coherence membres/derive : S0+{d0}={solution.S0 + d0} == fin0={wFin0}");
    }

    // Le callback n'est PAS invoque sur UNSAT (aucun modele a temoigner)
    bool invoked = false;
    var contradiction = thCtx.NewTheorem<Sched>()
        .Where(x => x.S0 == 1)
        .Where(x => x.S0 == 2)   // contradictoire
        .Solve(_ => invoked = true);
    Console.WriteLine($"[DSL] UNSAT : solution={(contradiction == null ? "null" : "?")}, callback invoque={invoked}  (pas de temoin sans modele)");
}
[RAW] Check : SATISFIABLE
[RAW]   modele : S0=0, S1=3
[RAW]   temoins derives : fin0=3, makespan=5, (S1>=fin0)=true
[DSL] Solve(inspect) : SAT  (S0=0, S1=3)
[DSL]   temoins derives : fin0=3, makespan=5, (S1>=fin0)=True
[DSL]   -> coherence membres/derive : S0+3=3 == fin0=3
[DSL] UNSAT : solution=null, callback invoque=False  (pas de temoin sans modele)

Lecture B5 - deux facons de temoigner, un même modèle

Les deux stacks resolvent le même mini-ordonnancement et lisent les mêmes quantites dérivées - fin de J0, makespan, fait de non-chevauchement - sous le même modèle qui a produit la solution. La différence est comment on rejoue une sous-expression après la résolution :

Aspect RAW (Model.Eval) DSL (Solve(inspect) / w.Eval)
Acces au modèle Manuel : garder sr.Model après Check() Threade dans un callback, uniquement si SAT
Quantite dérivée Re-exprimee en termes Z3 (MkAdd(s0, MkInt(d0))) Lambda C# typee (x => x.S0 + d0)
Type de retour Expr a caster (IntNum, BoolExpr) Valeur CLR directe (int, bool)
Sur UNSAT Model inexistant (exception si on force) Callback non invoque, Solve renvoie null

Ligne de contraste (a retenir) : le raw expose le Model Z3 et laisse l’utilisateur re-exprimer chaque quantite dérivée en termes du solveur ; le DSL fait ressortir le modèle par un callback type - w.Eval(x => x.S0 + d0) lit la même dérivée dans le vocabulaire du modèle-objet, sous exactement le même modèle, et se tait proprement sur UNSAT. Même modèle, même valeur, deux vocabulaires pour interroger la solution après coup.

Cas d’usage : Solve(inspect) est l’outil des metriques post-solution - quand la solution optimale (le Cmax de ce notebook) ne suffit pas et qu’on veut lire des grandeurs dérivées (temps morts, marges, indicateurs relationnels) sans les reifier en membres du type résultat. On bascule en raw quand on a besoin d’evaluer des termes Z3 arbitraires hors du schema du modèle-objet (ex. une fonction non-interpretee, un tableau).

Conclusion

Le Job Shop Scheduling est un problème NP-difficile en général. Sur notre instance 3×2 :

Approche Cmax Méthode
Glouton FIFO 16h Décisions locales séquentielles
Z3.Linq SMT 9h Exploration SMT complète
Borne inférieure 9h Charge Machine A = 3+4+2

Points clés : - Les contraintes disjonctives (||) expriment naturellement le non-chevauchement en Z3.Linq - La recherche linéaire sur Cmax transforme l’optimisation en séquence de problèmes de satisfaisabilité - Pour des instances plus grandes, des solveurs spécialisés (Google OR-Tools CP-SAT, CPLEX) sont préférables

Référence : Garey & Johnson (1979) — Computers and Intractability (NP-complétude du JSP général)

Retour au sommet