← 12 - Arithmetique reelle | README Z3-Python | 14 - BitVectors >> # 13. UNSAT cores : expliquer l’insatisfiabilite (le ’ pourquoi ‘) Jusqu’ici, le solveur repondait a une question binaire : ce système a-t-il une solution ? -> SAT (oui, voici un temoin) ou UNSAT (non, prouve impossible). C’est un verdict, pas une explication. Pour un ingenieur qui ecrit la specification, UNSAT est souvent un bug de modelisation : une contrainte trop forte, ou deux contraintes incompatibles. La reponse’ impossible ’ ne suffit pas - il faut savoir lesquelles des contraintes se contredisent. C’est le rôle du noyau d’insatisfiabilite (UNSAT core) : le sous-ensemble minimal de contraintes responsable du conflit. Z3 passe du diagnostic binaire au diagnostic chirurgical. > Port pyz3 du notebook C# 17_UnsatCores.ipynb. EPIC #1206, Prong B. (Le bloc DSL Explain() du C#, spécifique a Z3.Linq, n’est pas porte ; l’API brute assert_and_track + unsat_core de pyz3 fait le même travail.)

from z3 import *
print("Imports OK : z3-solver (UNSAT cores via assert_and_track)")
Imports OK : z3-solver (UNSAT cores via assert_and_track)

1. Du verdict a l’explication

Commencons par un système trivialement contradictoire. Le solveur dit UNSAT - mais ne dit pas (encore) POURQUOI. C’est le verdict brut.

# Rappel : un systeme contradictoire est UNSAT (verdict, sans explication)
a, b = Bools('a b')
s0 = Solver()
s0.add(Implies(a, b))   # a -> b
s0.add(a)               # a
s0.add(Not(b))          # not b  (contredit a -> b)
print("' a->b, a, !b ' : %s  (verdict : impossible)" % s0.check())
print("-> Z3 dit NON, mais ne dit pas (encore) POURQUOI.")
' a->b, a, !b ' : unsat  (verdict : impossible)
-> Z3 dit NON, mais ne dit pas (encore) POURQUOI.

Lecture chiffree — un systeme ou le core serait TOUT. ' a->b, a, !b ' : unsat : le verdict brut tombe en une ligne. Mais ce petit systeme a une propriete que les exemples suivants n’auront pas : aucune de ses trois contraintes n’est superflue. Chaque paire prise seule est satisfiable — {a->b, a} tient avec b vrai, {a->b, !b} tient avec a faux, {a, !b} tient sans l’implication. Autrement dit, un core etiquete de ce systeme contiendrait les TROIS contraintes : le conflit nait de la combinaison complete, pas d’une paire. C’est la frontiere utile a connaitre avant la section suivante — l’etiquetage assert_and_track ne reduit que ce qui peut l’etre : quand chaque contrainte participe a la refutation, le core egale le systeme, et l’explication reste a ecrire a la main.

2. L’API assert_and_track : etiqueter chaque contrainte

Pour obtenir une explication, on fournit les contraintes comme des hypothese traceables : s.assert_and_track(formule, etiquette) ou etiquette est un Bool servant de nom. Après un unsat, s.unsat_core() renvoie le sous-ensemble minimal d’etiquettes responsable du conflit. Trois contraintes sur x : x >= 3, x <= 5, x = 10. Lesquelles se contredisent ?

# Trois contraintes sur x : lesquelles se contredisent ?
x = Int('x')
s1 = Solver()
s1.set('unsat_core', True)
c1 = Bool('x_ge_3')   # etiquette pour x >= 3
c2 = Bool('x_le_5')   # etiquette pour x <= 5
c3 = Bool('x_eq_10')  # etiquette pour x = 10
s1.assert_and_track(x >= 3, c1)
s1.assert_and_track(x <= 5, c2)
s1.assert_and_track(x == 10, c3)
st1 = s1.check()
print("' x>=3, x<=5, x=10 ' : %s" % st1)
print()
if st1 == unsat:
    print("UNSAT CORE (contraintes conflictuelles, sous-ensemble MINIMAL) :")
    for c in s1.unsat_core():
        print("  - %s" % c)
    print("-> Z3 ecarte 'x>=3' du core : cette contrainte est irrelevant pour le conflit.")
' x>=3, x<=5, x=10 ' : unsat

UNSAT CORE (contraintes conflictuelles, sous-ensemble MINIMAL) :
  - x_le_5
  - x_eq_10
-> Z3 ecarte 'x>=3' du core : cette contrainte est irrelevant pour le conflit.

Lecture chiffree — la minimalite verifiee dans les DEUX sens. Core rendu : x_le_5, x_eq_10 — la section 3 montrera que la paire suffit. L’autre sens est tout aussi testable et complete la definition : chaque membre du core pris individuellement est NECESSAIRE. Retirer x_le_5 : {x>=3, x=10} est satisfiable (x = 10 verifie les deux). Retirer x_eq_10 : {x>=3, x<=5} est satisfiable (tout x de 3 a 5). Aucune des deux ne peut partir — le core est irreductible dans les deux directions : suffisant (paire UNSAT) et necessaire (chaque retrait redevient SAT). C’est la definition complete du MUS que la section 7 formalisera, deja realisee ici sur un exemple ou l’ecart se voit a l’oeil nu : x = 10 est a 5 unites de la borne x <= 5.

3. Minimalite du core : verifier que la paire suffit

Le core est minimal : retirer une seule contrainte du core le rend satisfiable. Verifions que la paire {x<=5, x=10} (sans x>=3) est déjà UNSAT - ce qui confirme que Z3 avait raison d’exclure x>=3.

# Verifions : {x<=5, x=10} SEUL (sans x>=3) est-il deja UNSAT ?
y = Int('y')
s2 = Solver()
s2.set('unsat_core', True)
p1 = Bool('y_le_5')
p2 = Bool('y_eq_10')
s2.assert_and_track(y <= 5, p1)
s2.assert_and_track(y == 10, p2)
st2 = s2.check()
print("' y<=5, y=10 ' (sans y>=3) : %s" % st2)
if st2 == unsat:
    print("-> CONFIRME : la paire {x<=5, x=10} suffit au conflit.")
    print("   Z3 avait donc raison d'EXCLURE 'x>=3' du core : elle est irrelevant.")
' y<=5, y=10 ' (sans y>=3) : unsat
-> CONFIRME : la paire {x<=5, x=10} suffit au conflit.
   Z3 avait donc raison d'EXCLURE 'x>=3' du core : elle est irrelevant.

4. Application : specification surcontrainte - laquelle relacher ?

Cas realiste : un planning ou 5 contraintes s’accumulent. L’une d’elles (h = 12, demande de l’animateur) contredit une autre (h != 12, pause dejeuner). Le core identifie exactement les 2 coupables parmi les 5 - les autres (bornes, redondances) sont compatibles et ignorees. L’action correctrice en decoule directement : relacher l’une des deux contraintes coupables.

# Specification surcontrainte : laquelle relacher ?
h = Int('h')
s3 = Solver()
s3.set('unsat_core', True)
n1 = Bool('h_ge_9')     # 1. h >= 9
n2 = Bool('h_le_17')    # 2. h <= 17
n3 = Bool('h_ne_12')    # 3. h != 12 (pause dejeuner)
n4 = Bool('h_eq_12')    # 4. h = 12 (animateur)  <-- conflit
n5 = Bool('h_ge_9b')    # 5. h >= 9 (redondant)
s3.assert_and_track(h >= 9, n1)
s3.assert_and_track(h <= 17, n2)
s3.assert_and_track(h != 12, n3)
s3.assert_and_track(h == 12, n4)
s3.assert_and_track(h >= 9, n5)
st3 = s3.check()
print("Specification (5 contraintes) : %s" % st3)
print()
if st3 == unsat:
    print("Core = les contraintes qui PARTICIPENT au conflit :")
    core = s3.unsat_core()
    for c in core:
        print("  COUPABLE : %s" % c)
    print()
    print("-> Sur 5 contraintes, %d seulement sont en conflit." % len(core))
    print("   Les autres (h>=9, h<=17, h>=9 redondant) sont COMPATIBLES -> Z3 les ignore.")
    print("   Action : relacher la contrainte 'h=12' (animateur) OU 'h!=12' (pause).")
Specification (5 contraintes) : unsat

Core = les contraintes qui PARTICIPENT au conflit :
  COUPABLE : h_ne_12
  COUPABLE : h_eq_12

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

Lecture chiffree — les deux relachements ne coutent pas le meme prix. Sur 5 contraintes, 2 seulement sont en conflit — mais les deux manieres de guerir ne sont pas equivalentes, et le systeme restant les chiffre. Les trois contraintes innocentes bornent h dans l’intervalle [9, 17], soit 17 - 9 + 1 = 9 valeurs entieres. Relacher h=12 (garder la pause dejeuner) : 9 - 1 = 8 solutions restent. Relacher h!=12 (garder la demande de l’animateur) : exactement 1 solution, h = 12. Le core dit QUELLES contraintes sont en conflit ; compter ce que chaque relachement laisse voir est le pas supplementaire qui transforme le diagnostic en decision — ici, l’option pause dejeuner preserve 8 des 9 plannings possibles, l’option animateur en fige un seul.

5. Innocence prouvee : une contrainte non impliquee ecartee du core

Un dernier temoin de la minimalite : sur un système a 3 contraintes (x == 1, x >= 0 innocente, x == 2), le core minimal est {x==1, x==2}. La contrainte x >= 0 est compatible avec les deux (un x valant 1 ou 2 verifie x >= 0) - elle n’est pas impliquee dans le conflit, donc Z3 l’ecarte du core. C’est ce qui distingue le core d’une simple liste de contraintes : il isole la cause, pas le contexte. > Note port : le notebook C# original compare ici l’API brute (Check(assumptions) + UnsatCore) avec le DSL Z3.Linq (Explain()). Le DSL n’existe pas en pyz3 - l’API brute assert_and_track + unsat_core est l’equivalent direct, et c’est elle que cette section demontre.

# Core minimal : {x==1, x==2} ecarte x>=0 (innocente, non impliquee)
w = Int('w')
s4 = Solver()
s4.set('unsat_core', True)
r0 = Bool('w_eq_1')    # x == 1
r1 = Bool('w_ge_0')    # x >= 0  (innocente)
r2 = Bool('w_eq_2')    # x == 2
s4.assert_and_track(w == 1, r0)
s4.assert_and_track(w >= 0, r1)
s4.assert_and_track(w == 2, r2)
print("Check(assumptions) : %s" % s4.check())
core = s4.unsat_core()
print("UnsatCore = { %s }   (x>=0 exclu du core)" % '  '.join(str(c) for c in core))
Check(assumptions) : unsat
UnsatCore = { w_eq_1  w_eq_2 }   (x>=0 exclu du core)

6. Ce que ce notebook a demontre

Trois lecons sur le noyau d’insatisfiabilite : 1. Du verdict a l’explication - unsat dit qu’il n’y a pas de solution ; unsat_core() dit pourquoi (lesquelles contraintes conflictuent).

  1. Minimalite - le core est le sous-ensemble minimal responsable : retirer un seul élément le rend satisfiable. Les contraintes irrelevant (compatibles, redondantes) sont ecartees.

  2. Actionnable - sur une specification surcontrainte, le core pointe exactement la (ou les) contrainte(s) a relacher, transformant un echec de modelisation en diagnostic chirurgical.

Cette capacite d’explication distingue un solveur d’un simple oracle booléen : il ne dit pas seulement non, il dit a cause de quoi.

7. Exercices

Les trois exercices ci-dessous vous font manipuler le UNSAT core sur des variantes : conflit cache parmi 4 contraintes (1), planning avec relachement (2), core minimal parmi 10 (3). Chaque stub est self-contained : les fonctions (Int, Bool, Solver, assert_and_track) sont définies dans les sections précédentes.

Exercice 1 - Core sur un conflit cache (2 coupables parmi 4)

Construisez 4 contraintes sur z dont 2 sont compatibles et 2 en conflit (ex : z <= 3, z >= 0, z == 7, z != 9). Obtenez le core et verifiez qu’il ne contient que les 2 coupables.

Étapes : z = Int('z'), 4 assert_and_track etiquetes, check(), afficher unsat_core() (doit exclure les 2 compatibles).

# Exercice 1 : core sur un conflit cache (2 coupables parmi 4)
# TODO etudiant :
# Etape 1 : z = Int('z') ; 4 contraintes etiquetees (2 compatibles, 2 en conflit)
# Etape 2 : s.assert_and_track(..., Bool('etiq')) pour chacune
# Etape 3 : s.check() + s.unsat_core() -> doit contenir seulement les 2 coupables
result = None  # TODO etudiant
print("Exercice 1 a completer : isolez les 2 contraintes coupables parmi 4")
Exercice 1 a completer : isolez les 2 contraintes coupables parmi 4

Exercice 2 - Planning : identifier puis relacher la coupable

Encodez un planning sur j : (a) j >= 8, (b) j <= 18, (c) j != 3, (d) j == 3. Obtenez le core, identifiez la coupable, puis relachez-la (re-checkez le sous-ensemble sans elle) -> le système devient SATISFIABLE.

Étapes : core = {j!=3, j=3} ; retirer l’une des deux du solver ; re-check() -> sat.

# Exercice 2 : planning, identifier puis relacher la contrainte coupable
# TODO etudiant :
# Etape 1 : encoder (a)(b)(c)(d) sur j, obtenir le core
# Etape 2 : core = {j!=3, j=3} -> choisir laquelle relacher
# Etape 3 : re-check sur le sous-ensemble SANS la coupable -> SATISFIABLE
result = None  # TODO etudiant
print("Exercice 2 a completer : identifiez et relachez la contrainte coupable")
Exercice 2 a completer : identifiez et relachez la contrainte coupable

Exercice 3 - Core minimal parmi 10 contraintes

Construisez 10 contraintes sur k : 3 conflictuelles (k == 1, k == 2, k == 3) + 7 compatibles (k >= 0, k <= 100, etc.). Le core doit valoir exactement 3 (les 3 incompatibles), les 7 compatibles etant ecartees.

Étapes : 10 assert_and_track ; check() ; compter len(unsat_core()) -> attendu 3.

# Exercice 3 : core minimal parmi 10 contraintes
# TODO etudiant :
# Etape 1 : k = Int('k') ; 10 contraintes (3 k==n incompatibles + 7 compatibles)
# Etape 2 : s.assert_and_track pour les 10
# Etape 3 : s.check() + len(s.unsat_core()) -> doit valoir 3
nb_coupables = None  # TODO etudiant
print("Exercice 3 a completer : mesurer |core| parmi 10 contraintes (attendu : 3)")
Exercice 3 a completer : mesurer |core| parmi 10 contraintes (attendu : 3)

Conclusion

Le UNSAT core transforme le solveur d’oracle binaire en outil de diagnostic. La ou unsat dit seulement ’ impossible ‘, unsat_core() dit’ impossible a cause de ces contraintes-la ’ - le sous-ensemble minimal responsible du conflit. Sur une specification surcontrainte, ce diagnostic est directement actionnable : il pointe la contrainte a relacher.

Cette serie Z3-Python (notebooks 01 a 13) couvre maintenant les trois postures du solveur : decider (sat/unsat, 01-11), optimiser (Optimize, 06/08), et ici expliquer (unsat_core, 13). La ou l’ingenieur classique debug a l’aveugle un système insatisfiable, le solveur SMT isole chirurgicalement la cause - la différence entre un oracle et un partenaire de raisonnement.

Le compagnon Z3-13b - le MUS approfondit ce langage : core invisible a l’inspection, minimalite non garantie par Z3, et l’algorithme deletion-based qui calcule le sous-ensemble irreductible.

Retour au sommet