17 — UNSAT cores Z3 : expliquer l’insatisfiabilité (le « pourquoi »)

Notebook de la série Z3 / SMT (Track C#, Z3.Linq fork). Troisième et dernière théorie-capacité jamais exercée dans les notebooks 01-16 : les UNSAT cores — non plus décider qu’une formule est insatisfiable, mais expliquer quelles contraintes précisément la rendent insatisfiable. Stack : B — API brute Microsoft.Z3 (Check(assumptions)/UnsatCore) : l’extraction de core n’a pas d’équivalent dans le DSL Z3.Linq.

Pourquoi ce notebook

Les notebooks 15 (bit-vectors) et 16 (réels) ont mis en scène la distinction cardinale SAT vs UNSAT : un solveur ne trouve pas seulement des solutions, il certifie leur impossibilité. Mais une question reste ouverte : quand Z3 répond UNSAT, pourquoi ? L’utilisateur a écrit une dizaine de contraintes ; lesquelles, précisément, se contredisent ?

C’est le service de l’UNSAT core : parmi les contraintes (hypothèses) fournies, Z3 isole le sous-ensemble minimal qui suffit à provoquer l’insatisfiabilité. Les contraintes irrelevantes (qui ne participent pas au conflit) sont écartées du core. C’est l’outil canonique du débogage de spécifications surcontraintes : plutôt que de lire 100 contraintes à la main pour trouver l’incohérence, on laisse le solveur pointer les coupables.

Prong-B (non-trivial) : le calcul d’un UNSAT core est un service algorithmique distinct de la simple décision SAT/UNSAT. Il repose sur la résolution assimilable (clauses apprises/learned clauses) et l’extraction du sous-ensemble d’hypothèses impliqué dans la dérivation du vide. Aucun des notebooks 01-16 ne l’exerçait — tous s’arrêtaient au verdict (SAT/UNSAT), jamais à l’explication.

1. Du verdict à l’explication

Jusqu’ici, la série posait une question binaire :

Ce système de contraintes a-t-il une solution ? → SAT (oui, voici un témoin) ou UNSAT (non, prouvé impossible).

Mais pour un ingénieur qui écrit la spécification, UNSAT est souvent un bug de modélisation : il a écrit une contrainte trop forte, ou deux contraintes incompatibles. La réponse « impossible » ne l’aide pas à corriger. L’UNSAT core répond à la vraie question :

Quelles contraintes, parmi celles que j’ai écrites, se contredisent ?

La mécanique : on fournit les contraintes comme des hypothèses (Check(assumptions)), et si le système est insatisfiable, Z3 renvoie le core — le sous-ensemble minimal d’hypothèses suffisant à prouver l’insatisfiabilité.

#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;
Console.OutputEncoding = Encoding.UTF8;

var ctx = new Context();

// Rappel : un système contradictoire est UNSAT (verdict, sans explication)
var s0 = ctx.MkSolver();
BoolExpr a = ctx.MkBoolConst("a");
BoolExpr b = ctx.MkBoolConst("b");
s0.Assert(ctx.MkImplies(a, b));   // a -> b
s0.Assert(a);                      // a
s0.Assert(ctx.MkNot(b));           // !b   (contredit a -> b)
Console.WriteLine($"« a->b, a, !b » : {s0.Check()}  (verdict : impossible)");
Console.WriteLine("-> Z3 dit NON, mais ne dit pas (encore) POURQUOI.");
« a->b, a, !b » : UNSATISFIABLE  (verdict : impossible)
-> Z3 dit NON, mais ne dit pas (encore) POURQUOI.

2. Le core : quelles contraintes se contredisent ?

Maintenant, fournissons les contraintes comme hypothèses et demandons le core. Trois contraintes sur un entier x :

x ≥ 3     (borne inférieure)
x ≤ 5     (borne supérieure)
x = 10    (valeur imposée)

Le système est UNSAT (x = 10 viole x ≤ 5). Mais laquelle des contraintes est coupable ? L’UNSAT core isole le sous-ensemble minimal conflictuel.

// Trois contraintes sur x : lesquelles se contredisent ?
IntExpr x = ctx.MkIntConst("x");

BoolExpr c1 = ctx.MkGe(x, ctx.MkInt(3));    // x >= 3
BoolExpr c2 = ctx.MkLe(x, ctx.MkInt(5));    // x <= 5
BoolExpr c3 = ctx.MkEq(x, ctx.MkInt(10));   // x = 10

// On fournit les contraintes COMME HYPOTHÈSES (pas Assert dur) -> Check(assumptions)
BoolExpr[] assumptions = new BoolExpr[]{ c1, c2, c3 };
var s1 = ctx.MkSolver();
Status st = s1.Check((System.Collections.Generic.IEnumerable<BoolExpr>)assumptions);

Console.WriteLine($"« x>=3, x<=5, x=10 » : {st}");
Console.WriteLine();
if (st == Status.UNSATISFIABLE) {
    Console.WriteLine("UNSAT CORE (contraintes conflictuelles, sous-ensemble MINIMAL) :");
    foreach (var c in s1.UnsatCore) {
        Console.WriteLine($"  - {c}");
    }
}
« x>=3, x<=5, x=10 » : UNSATISFIABLE

UNSAT CORE (contraintes conflictuelles, sous-ensemble MINIMAL) :
  - (<= x 5)
  - (= x 10)

3. Le core est MINIMAL : les contraintes irrelevantes sont écartées

L’observation clé : le core de la section 2 contenait x ≤ 5 et x = 10, mais pas x ≥ 3. Ce n’est pas un oubli — c’est que x ≥ 3 est irrelevant pour le conflit : la contradiction vient uniquement de la borne supérieure et de la valeur imposée. Retirer x ≥ 3 ne change rien au verdict UNSAT.

C’est la propriété fondamentale d’un UNSAT core : il identifie exactement les contraintes qui participent au conflit, et ignore celles qui sont compatibles (même si elles figurent dans le système). Pour un débogueur, c’est inestimable : sur 100 contraintes, le core peut n’en contenir que 2.

Vérifions : le système {x ≤ 5, x = 10} (sans x ≥ 3) est-il déjà UNSAT ?

// Vérifions : {x<=5, x=10} SEUL (sans x>=3) est-il déjà UNSAT ?
IntExpr y = ctx.MkIntConst("y");
BoolExpr p1 = ctx.MkLe(y, ctx.MkInt(5));    // y <= 5
BoolExpr p2 = ctx.MkEq(y, ctx.MkInt(10));   // y = 10

var s2 = ctx.MkSolver();
Status st2 = s2.Check((System.Collections.Generic.IEnumerable<BoolExpr>)(new BoolExpr[]{ p1, p2 }));

Console.WriteLine($"« y<=5, y=10 » (sans y>=3) : {st2}");
if (st2 == Status.UNSATISFIABLE) {
    Console.WriteLine("-> CONFIRMÉ : la paire {x<=5, x=10} suffit au conflit.");
    Console.WriteLine("   Z3 avait donc raison d'EXCLURE « x>=3 » du core : elle est irrelevant.");
}
« y<=5, y=10 » (sans y>=3) : UNSATISFIABLE
-> CONFIRMÉ : la paire {x<=5, x=10} suffit au conflit.
   Z3 avait donc raison d'EXCLURE « x>=3 » du core : elle est irrelevant.

4. Application : déboguer une spécification surcontrainte

Cas d’usage réel : un planificateur de réunion pose 5 contraintes et obtient UNSAT. Lequel relâcher ? Sans core, il faut tester les combinaisons à la main. Avec le core, Z3 pointe la (les) contrainte(s) coupable(s).

Modélisons : une réunion doit avoir lieu à une heure h (entière) satisfaisant :

  1. h ≥ 9 (pas avant 9h)
  2. h ≤ 17 (pas après 17h)
  3. h ≠ 12 (pas pendant la pause déjeuner)
  4. h = 12 (le seul créneau libre de l’animateur) ← contradiction avec la 3
  5. h ≥ 9 (redondant, répète la 1)

Z3 isole le conflit réel (h ≠ 12 vs h = 12) et ignore les contraintes compatibles.

// Spécification surcontrainte : laquelle relâcher ?
IntExpr h = ctx.MkIntConst("h");

BoolExpr[] specs = new BoolExpr[] {
    ctx.MkGe(h, ctx.MkInt(9)),                    // 1. h >= 9
    ctx.MkLe(h, ctx.MkInt(17)),                   // 2. h <= 17
    ctx.MkNot(ctx.MkEq(h, ctx.MkInt(12))),        // 3. h != 12 (pause déjeuner)
    ctx.MkEq(h, ctx.MkInt(12)),                   // 4. h = 12 (animateur)  <-- conflit
    ctx.MkGe(h, ctx.MkInt(9))                     // 5. h >= 9 (redondant)
};

var s3 = ctx.MkSolver();
Status st3 = s3.Check((System.Collections.Generic.IEnumerable<BoolExpr>)specs);
Console.WriteLine($"Spécification (5 contraintes) : {st3}");
Console.WriteLine();
if (st3 == Status.UNSATISFIABLE) {
    Console.WriteLine("Core = les contraintes qui PARTICIPENT au conflit :");
    int n = 0;
    foreach (var c in s3.UnsatCore) {
        Console.WriteLine($"  COUPABLE : {c}");
        n++;
    }
    Console.WriteLine();
    Console.WriteLine($"-> Sur 5 contraintes, {n} seulement sont en conflit.");
    Console.WriteLine("   Les autres (h>=9, h<=17, h>=9 redondant) sont COMPATIBLES -> Z3 les ignore.");
    Console.WriteLine("   Action : relâcher la contrainte 'h=12' (animateur) OU 'h!=12' (pause).");
}
Spécification (5 contraintes) : UNSATISFIABLE

Core = les contraintes qui PARTICIPENT au conflit :
  COUPABLE : (= h 12)
  COUPABLE : (not (= h 12))

-> Sur 5 contraintes, 2 seulement sont en conflit.
   Les autres (h>=9, h<=17, h>=9 redondant) sont COMPATIBLES -> Z3 les ignore.
   Action : relâcher la contrainte 'h=12' (animateur) OU 'h!=12' (pause).

B6 - Cores UNSAT côté DSL (Theorem<T>.Explain())

Tout ce notebook lit le core par l’API brute : solver.Check(assumptions) puis solver.UnsatCore. Longtemps le DSL Z3.Linq n’avait pas d’équivalent - .Solve() réduit tout échec à null (« insatisfiable » et « le solveur n’a pas su décider » deviennent indistinguables, et le pourquoi est perdu). Le binding ajoute désormais une surface diagnostique parallèle et non-cassante : Theorem<T>.Explain() renvoie une Explanation qui distingue SolveStatus Satisfiable / Unsatisfiable / Unknown et, sur UNSAT, expose le core minimal sous forme de ConstraintRef (Index, Expression) - le sous-ensemble contradictoire des .Where durs, avec leur expression source. .Solve() reste inchangé.

Stack : A + B - pourquoi. Ce bloc corrige un cadrage vieilli du tableau A/B (« UNSAT cores = sans équivalent LINQ ») : le core UNSAT a maintenant une écriture DSL. Le raw Check(assumptions) + UnsatCore matérialise le mécanisme (contraintes fournies comme hypothèses traçables) ; .Explain() le déclare en LINQ, en portant en plus l’expression source de chaque coupable. Le contraste est le même core minimal ({#0, #2}, la contrainte innocente #1 écartée) obtenu des deux côtés sur le même système.

// B6 - Cores UNSAT côté DSL "Explain()" : deux stacks sur le MEME systeme sur-contraint.
//   x == 1  (contrainte #0)   |   x >= 0  (contrainte #1, INNOCENTE)   |   x == 2  (contrainte #2)
// Le systeme est UNSAT ; le core MINIMAL est {#0, #2} : Z3 ecarte #1, non impliquee dans le conflit.
// Le meme core minimal sort du raw (Check(assumptions)+UnsatCore) et du DSL (Explain().UnsatCore).

// Classe au niveau cellule (requise par NewTheorem<T>).
public class Cell { public int X { get; set; } }

// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : contraintes fournies comme hypotheses tracables
// =====================================================================
{
    using var z3 = new Microsoft.Z3.Context();
    IntExpr xr = z3.MkIntConst("x");
    Microsoft.Z3.BoolExpr r0 = z3.MkEq(xr, z3.MkInt(1));   // #0 : x == 1
    Microsoft.Z3.BoolExpr r1 = z3.MkGe(xr, z3.MkInt(0));   // #1 : x >= 0 (innocente)
    Microsoft.Z3.BoolExpr r2 = z3.MkEq(xr, z3.MkInt(2));   // #2 : x == 2
    var sr = z3.MkSolver();
    var assumptions = new Microsoft.Z3.BoolExpr[] { r0, r1, r2 };
    Status st = sr.Check((System.Collections.Generic.IEnumerable<Microsoft.Z3.BoolExpr>)assumptions);
    Console.WriteLine($"[RAW] Check(assumptions) : {st}");
    Console.Write("[RAW]   UnsatCore = { ");
    foreach (var c in sr.UnsatCore) Console.Write(c + "  ");
    Console.WriteLine("}   (x>=0 exclu du core)");
}

// =====================================================================
// BLOC DSL (Z3.Linq) : la meme explication en LINQ, avec l'expression source de chaque coupable
// =====================================================================
{
    using var thCtx = new Z3Context();
    var explanation = thCtx.NewTheorem<Cell>()
        .Where(c => c.X == 1)   // #0
        .Where(c => c.X >= 0)   // #1 (innocente)
        .Where(c => c.X == 2)   // #2
        .Explain();
    Console.WriteLine($"[DSL] Explain().Status : {explanation.Status}");
    Console.WriteLine("[DSL]   UnsatCore (core minimal) :");
    foreach (var cr in explanation.UnsatCore)
        Console.WriteLine($"[DSL]     {cr}");   // ConstraintRef.ToString() = "#Index: Expression"
    // Indices coupables (sans System.Linq)
    var idx = new System.Text.StringBuilder();
    foreach (var cr in explanation.UnsatCore) { if (idx.Length > 0) idx.Append(","); idx.Append(cr.Index); }
    Console.WriteLine($"[DSL]   -> indices coupables = {{{idx}}}  (#1 x>=0 exclu du core minimal)");
}
[RAW] Check(assumptions) : UNSATISFIABLE
[RAW]   UnsatCore = { (= x 1)  (= x 2)  }   (x>=0 exclu du core)
[DSL] Explain().Status : Unsatisfiable
[DSL]   UnsatCore (core minimal) :
[DSL]     #0: (c.X == 1)
[DSL]     #2: (c.X == 2)
[DSL]   -> indices coupables = {0,2}  (#1 x>=0 exclu du core minimal)

Lecture B6 - deux surfaces, un même core minimal

Les deux stacks partent du même système sur-contraint (x==1, x>=0, x==2) et isolent le même core minimal {#0, #2} - la contrainte innocente #1 (x>=0, satisfiable seule) est écartée. La différence est ce que chaque surface rend :

Aspect RAW (Check(assumptions) + UnsatCore) DSL (Explain())
Verdict Status (Sat/Unsat) — Unknown non distingué de Unsat par Solve() SolveStatus : Sat / Unsat / Unknown explicitement distingués
Core IEnumerable<BoolExpr> (les termes Z3 fournis comme hypothèses) IReadOnlyList<ConstraintRef> : index + expression source du .Where
Traçabilité l’utilisateur doit relier chaque BoolExpr à son intention chaque coupable porte sa position (#Index) et son texte
.Solve() inchangé inchangé (Explain() est une surface parallèle)

Ligne de contraste (à retenir) : le raw expose le mécanisme Z3 des cores (assumptions traçables passées à Check) ; le DSL en fait un diagnostic de première classe - Explain() distingue les trois statuts et renvoie le core comme une liste de ConstraintRef (Index, Expression), si bien qu’on sait non seulement qu’il y a conflit mais quelles lignes .Where le portent. Ce bloc met à jour le cadrage historique (« UNSAT cores : sans équivalent LINQ ») : le core a désormais une écriture DSL ; seule la preuve par réfutation (block-and-resolve manuel) reste l’apanage du raw.

Cas d’usage : Explain() est l’outil de débogage de spécifications sur-contraintes quand on travaille déjà en DSL - on garde la lisibilité des .Where et on obtient le sous-ensemble coupable sans redescendre à l’API brute. On bascule en raw pour la preuve par réfutation (prouver l’unicité d’une solution par UNSAT du complément), que Explain() ne couvre pas.

5. Ce que ce notebook a démontré

L’UNSAT core complète l’arc des trois capacités de Z3 ouvertes par les notebooks 15-17 :

Capacité Question Notebook
Décider (SAT) Une solution existe-t-elle ? 01-14 (entiers), 15 (bit-vectors)
Prouver (UNSAT) L’impossibilité est-elle certifiée ? 15, 16 (réfutation)
Expliquer (core) Quelles contraintes causent l’insatisfiabilité ? 17 (ce notebook)

Le passage du verdict à l’explication est le saut qui transforme un solveur en outil de débogage de spécifications : sur un système surcontraint, le core pointe le sous-ensemble minimal de contraintes coupables, écartant les contraintes irrelevantes (compatibles). C’est inestimable pour un ingénieur qui doit relâcher la bonne contrainte parmi des dizaines.

La leçon d’arc : un solveur SMT ne se résume pas à une boîte « satisfiable ou non ». Il opère à trois niveaux — trouver (témoignage), certifier (preuve d’impossibilité), expliquer (core). Les trois sont des services distincts, et maîtriser Z3 c’est savoir demander le bon.

Où aller ensuite

Avec les notebooks 15 (bit-vectors), 16 (réels) et 17 (UNSAT cores), la série a désormais exercé les théories et capacités centrales que le binding LINQ (notebooks 01-14) masquait. Les prolongements naturels :

  • Combiner les théories : un même problème mélangeant entiers, réels et bit-vectors (le terrain réel des vérificateurs industriels — la combinaison de théories est elle-même un sujet algorithmique, Nelson-Oppen).
  • Les preuves formelles (Proof = true) : non plus un core (sous-ensemble de contraintes), mais la dérivation complète justifiant l’UNSAT — l’objet qu’un vérificateur externalisé peut re-vérifier indépendamment de Z3.

6. Exercices

Trois exercices pour approfondir. Stubs incomplets — le notebook s’exécute de bout en bout même non complété (convention C.1).

Exercice 1 — Core sur un conflit caché

Construisez 4 contraintes sur un entier z telles que seules 2 d’entre elles soient en conflit, les 2 autres étant compatibles. Vérifiez que l’UNSAT core ne contient que les 2 coupables (pas les 2 irrelevantes).

Indice : par exemple z ≥ 0, z ≤ 100, z = 50 (compatibles), z = 200 (conflit avec z ≤ 100). Le core devrait être {z ≤ 100, z = 200}.

// Exercice 1 : core sur un conflit caché (2 coupables parmi 4)
IntExpr z = ctx.MkIntConst("z");
// TODO etudiant : 4 contraintes (2 compatibles, 2 en conflit), Check(assumptions), afficher le core
// Etape 1 : BoolExpr[] cons = { ... };
// Etape 2 : solver.Check((IEnumerable<BoolExpr>)cons)
// Etape 3 : foreach (var c in solver.UnsatCore) afficher -> doit contenir seulement les 2 coupables
Console.WriteLine("Exercice 1 à compléter.");
Exercice 1 à compléter.

Exercice 2 — Spécification de planning

Un cours doit être programmé à un jour j (1=lundi … 5=vendredi) satisfaisant : (a) j ≠ 3 (pas mercredi), (b) j = 3 (seul jour libre de la salle), (c) j ≥ 1, (d) j ≤ 5. Utilisez l’UNSAT core pour identifier la contrainte à relâcher, puis relâchez-la et vérifiez que le système devient SAT.

Indice : le core = {j≠3, j=3}. Après relâche de l’une des deux, Check doit donner SAT.

// Exercice 2 : planning, identifier puis relâcher la contrainte coupable
IntExpr j = ctx.MkIntConst("j");
// TODO etudiant : encoder (a)(b)(c)(d), obtenir le core, relâcher la coupable, re-Check -> SAT
// Etape 1 : core = {j!=3, j=3} -> choisir laquelle relâcher
// Etape 2 : solver.Check sur le sous-ensemble SANS la coupable -> SATISFIABLE
Console.WriteLine("Exercice 2 à compléter.");
Exercice 2 à compléter.

Exercice 3 — Taille du core vs nombre de contraintes

Générez un système de 10 contraintes sur un entier k dont seulement 3 sont en conflit (les 7 autres compatibles). Mesurez la taille du core et comparez-la au nombre total de contraintes. L’UNSAT core est-il bien minimal (≤ 3) ?

Indice : 3 contraintes mutuellement incompatibles (ex. k=1, k=2, k=3) + 7 contraintes compatibles (k≥0, k≤100, etc.). Le core doit faire exactement 3.

// Exercice 3 : core minimal parmi 10 contraintes
IntExpr k = ctx.MkIntConst("k");
// TODO etudiant : 10 contraintes (3 conflictuelles + 7 compatibles), mesurer |core|
// Etape 1 : BoolExpr[] ten = { k==1, k==2, k==3, k>=0, k<=100, ... };
// Etape 2 : solver.Check((IEnumerable<BoolExpr>)ten)
// Etape 3 : compter solver.UnsatCore -> doit valoir 3 (les 3 k==n incompatibles)
Console.WriteLine("Exercice 3 à compléter.");
Exercice 3 à compléter.
Retour au sommet