← 13 - UNSAT cores | README Z3-Python

Z3-Python-13b — UNSAT cores : le MUS (sous-ensemble irréductible)

Compagnon « preuve minimale » du module Z3-Python-13 — UNSAT cores.

Le notebook 13 a établi le noyau d’insatisfiabilité (core) : assert_and_track étiquette chaque contrainte, unsat_core() isole celles qui conflitent. Ce compagnon 13b pousse là où le 13 s’arrête : d’abord un système où le conflit est invisible à l’inspection (aucune paire ne se contredit, l’insatisfiabilité émerge d’une combinaison), ensuite la limite de unsat_core() — Z3 ne garantit pas la minimalité — et l’algorithme deletion-based qui calcule le MUS (Minimal Unsatisfiable Subset) : le sous-ensemble irréductible, dont retirer n’importe quelle contrainte rend le système satisfiable.

from z3 import *

1. Le vrai test : un core invisible a l’inspection

Les exemples du notebook 13 - UNSAT cores (sections 2 a 5) partagent une limite : dans chacun, le conflit est visible a l’oeil nu – deux contraintes se contredisent textuellement (h == 12 vs h != 12, x == 1 vs x == 2). On n’a pas vraiment besoin de Z3 pour les isoler.

C’est la que unsat_core() devient precieux : sur un systeme ou aucune paire de contraintes ne se contredit, mais ou l’insatisfiabilite emerge d’une combinaison. Cas concret, un projet de planification : quatre taches \(T_0, T_1, T_2, T_3\) s’enchainent (chacune doit finir avant que la suivante commence), chacune dure 2 unites, et tout doit etre termine avant la date 7. Aucune contrainte prise isolement n’est absurde – et pourtant le systeme est insatisfiable. Lequel des 11 ingredients faut-il relacher ?

# Planification surcontrainte : 4 taches enchainees (T0->T1->T2->T3), duree 2 chacune,
# a finir avant la date 7. Aucune contrainte isolee n'est absurde -> conflit structurel.
s_start = [Int(f"start_{i}") for i in range(4)]
DUREE = 2
DATE_LIMITE = 7
s5 = Solver()
s5.set("unsat_core", True)
labels = []

def ajouter(constraint, nom):
    b = Bool(nom)
    s5.assert_and_track(constraint, b)
    labels.append(b)
    return b

# Chaque tache : demarre apres 0 et finit avant la date limite
for i in range(4):
    ajouter(s_start[i] >= 0, f"release_T{i}")
    ajouter(s_start[i] + DUREE <= DATE_LIMITE, f"deadline_T{i}")
# Enchainement : Ti finit avant que Ti+1 commence
for i in range(3):
    ajouter(s_start[i] + DUREE <= s_start[i + 1], f"precedence_T{i}_vers_T{i + 1}")

print("Check : %s" % s5.check())
core = s5.unsat_core()
print("Core minimal = { %s }" % "  ".join(str(c) for c in core))
print("Taille du core : %d contraintes sur %d" % (len(core), len(labels)))
innocentes = [str(b) for b in labels if b not in core]
print("Contraintes innocentes ecartees (%d) : %s" % (len(innocentes), ", ".join(innocentes)))
Check : unsat
Core minimal = { release_T0  deadline_T3  precedence_T0_vers_T1  precedence_T1_vers_T2  precedence_T2_vers_T3 }
Taille du core : 5 contraintes sur 11
Contraintes innocentes ecartees (6) : deadline_T0, release_T1, deadline_T1, release_T2, deadline_T2, release_T3

Lecture : le core isole la chaine, pas une paire

Le core minimal contient 5 contraintes sur 11 : le release_T0 (point de depart), les trois precedences qui enchainent \(T_0 \to T_1 \to T_2 \to T_3\), et le deadline_T3 (echeance finale). Les 6 autres – les bornes et echeances intermediaires deadline_T0, release_T1/T2/T3, deadline_T1/T2 – sont ecartees : la chaine les implique deja, elles ne sont pas necessaires au conflit.

Pourquoi ce core est invisible a l’inspection : aucune des 5 contraintes coupables ne contredit une autre textuellement. Il faut tracer la chaine – start_T0 >= 0, puis +2 a chaque precedence, donc start_T1 >= 2, start_T2 >= 4, start_T3 >= 6, puis +2 de duree = 8 > 7 (la deadline) – pour voir le conflit. Et ce core de 5 est le SEUL possible : retirer release_T0 et la chaine flotte librement, retirer une precedence et la chaine se coupe, retirer deadline_T3 et chaque echeance restante est tenable – le core rendu n’est pas un choix parmi d’autres, c’est l’unique sous-ensemble irreductible, et les 6 contraintes ecartees le sont a bon droit.

C’est precisement le travail fastidieux qu’evite unsat_core() : parmi 11 contraintes, il isole chirurgicalement les 5 qui forment la preuve d’insatisfiabilite.

2. Au-dela du core : le MUS (Minimal Unsatisfiable Subset)

Jusqu’ici, on a fait confiance a unsat_core() pour renvoyer un sous-ensemble minimal de contraintes. Mais Z3 ne le garantit pas : le core est un sous-ensemble responsable du conflit, pas necessairement le plus petit. Sur l’arithmetique lineaire simple, Z3 minimise souvent bien ; sur des modeles plus riches (graphe de precedences, contraintes transitives), il peut laisser des contraintes redundantes dans le core.

Le MUS (Minimal Unsatisfiable Subset) est le sous-ensemble irreductible : retirer n’importe laquelle de ses contraintes rend le systeme satisfiable. L’algorithme deletion-based est simple et garantit cette irreductibilite : on retire les contraintes une a une, et si le systeme reste UNSAT sans l’une d’elles, c’est qu’elle etait superflue — on la supprime definitivement.

from z3 import *

def compute_mus(constraints):
    """MUS deletion-based : sous-ensemble irreductible rendant le systeme UNSAT.

    constraints : liste de couples (formule, etiquette Bool).
    Renvoie le plus petit sous-ensemble tel qu'aucune contrainte ne puisse
    etre retiree sans rendre le systeme satisfiable."""
    mus = list(constraints)
    i = 0
    while i < len(mus):
        candidat = mus[:i] + mus[i+1:]          # mus sans la contrainte i
        s = Solver(); s.set("unsat_core", True)
        for formule, etiquette in candidat:
            s.assert_and_track(formule, etiquette)
        if s.check() == unsat:
            mus = candidat                       # reste UNSAT -> i etait superflue
        else:
            i += 1                                # i est essentielle -> on la garde
    return mus

# Ordonnancement de taches : 5 taches t0..t4 avec precedences (durees) + deadline.
# Les aretes transitives (ex. t0 -> t3) rendent certaines contraintes redondantes.
t = [Int('t%d' % k) for k in range(5)]
precedences = [
    (t[1] >= t[0] + 5,  Bool('e01')),   # t0 -> t1 (duree 5)
    (t[2] >= t[1] + 3,  Bool('e12')),   # t1 -> t2 (duree 3)
    (t[3] >= t[2] + 4,  Bool('e23')),   # t2 -> t3 (duree 4)
    (t[3] >= t[0] + 12, Bool('e03')),   # t0 -> t3 transitif (5+3+4 = 12)
    (t[4] >= t[3] + 2,  Bool('e34')),   # t3 -> t4 (duree 2)
    (t[4] <= t[0] + 10, Bool('dead')),  # deadline : chemin total = 14 > 10 -> UNSAT
]

# Core brut de Z3
s_core = Solver(); s_core.set("unsat_core", True)
for f, e in precedences:
    s_core.assert_and_track(f, e)
print("Ordonnancement :", s_core.check())
core_z3 = [str(c) for c in s_core.unsat_core()]
print("Core Z3 (brut) :", sorted(core_z3), "- taille", len(core_z3))

# MUS irreductible
mus = compute_mus(precedences)
mus_labels = sorted(str(e) for f, e in mus)
print("MUS (irreductible) :", mus_labels, "- taille", len(mus_labels))
print("Contraintes redundantes eliminees :", sorted(set(core_z3) - set(mus_labels)))
print("-> Le core de Z3 (taille %d) n'etait PAS minimal : le MUS est de taille %d." % (len(core_z3), len(mus_labels)))
Ordonnancement : unsat
Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5
MUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3
Contraintes redundantes eliminees : ['e01', 'e12', 'e23']
-> Le core de Z3 (taille 5) n'etait PAS minimal : le MUS est de taille 3.

Lecture chiffree — deux preuves differentes du meme UNSAT. Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5 puis MUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3. Regarder les etiquettes, pas seulement les tailles : le core brut contient le chemin DETAILLE t0->t1->t2->t3, le MUS contient l’arete TRANSITIVE e03 — absente du core. Z3 refute en descendant la chaine (5+3+4 = 12, puis +2 = 14, contre la borne de 10) ; l’algorithme deletion-based trouve le raccourci et rend une preuve 40 % plus courte (3 contraintes contre 5).

Pourquoi le core n’etait pas minimal. Les aretes e01, e12, e23 (le chemin t0->t1->t2->t3) sont impliquees par l’arete transitive e03 (t0->t3, de duree cumulee 12). Z3 les a inclues dans son core parce qu’elles participent a la refutation, mais elles sont logiquement superflues des que e03 est presente. Le MUS les ecarte et ne garde que l’irreductible : e03 + e34 + dead (la deadline que les 14 unites de chemin total violent).

Le MUS n’est pas forcement unique — et le core depend du chemin de refutation. Un systeme peut contenir plusieurs sous-ensembles minimaux distincts. Si l’on a trois paires de contraintes independantes chacune contradictoire ({A,B}, {C,D}, {E,F}), chacune est un MUS valide de taille 2. unsat_core() en renvoie un ; l’algorithme deletion-based en renvoie un autre selon l’ordre de suppression — avant de s’appuyer sur UN core pour relacher une contrainte, savoir qu’un autre existait, plus petit. C’est la limite du core unique : il diagnostique un conflit, pas tous les conflits minimaux (les enumerer tous est un probleme distinct, dit MUS enumeration, nettement plus couteux).

Pont avec les sections precedentes. Le unsat_core() (sections 2-6) repond : ces contraintes suffisent au conflit. Le MUS repond plus fort : aucune d’elles ne peut etre retiree. Sur un modele ou l’on veut corriger la specification (relacher la bonne contrainte), c’est le MUS — pas le core brut — qui indique exactement les frontieres du conflit irreductible.

3. Ce que ce notebook a demontre

Trois lecons au-dela du core brut : 1. Là où ça compte - sur un système où aucun conflit n’est visible à l’œil (section 1), le core isole la combinaison coupable parmi de nombreuses contraintes innocentes – c’est là que le diagnostic devient indispensable, pas décoratif.

  1. Irréductibilité - le MUS est le sous-ensemble dont chaque membre est essentiel : le retirer rend le système satisfiable. L’algorithme deletion-based le garantit constructivement, là où le core brut de Z3 peut contenir des contraintes redondantes.

  2. Deux preuves du même UNSAT - le core brut et le MUS sont deux refutations différentes de la même insatisfiabilité ; le MUS est la plus courte (section 2 : 5 contraintes contre 3, l’arête transitive remplaçant le chemin détaillé). Comparer les deux, c’est mesurer à quel point un diagnostic peut être resserré.

4. Exercices

Les trois exercices vous font manipuler le MUS sur des variantes : irréductibilité vérifiée membre par membre (1), arête transitive contre chemin détaillé (2), diagnostic actionnable par le MUS (3). La fonction compute_mus est définie à la section 2 ; les stubs sont self-contained.

Exercice 1 - Irréductibilité vérifiée membre par membre

Construisez 8 contraintes sur w : 3 en conflit de chaîne (ex : w >= 0, w >= 4, w + 4 <= 6, w == 5) plus 4 compatibles (w <= 100, w != 7, etc.). Calculez le MUS avec compute_mus, puis vérifiez la propriété définitoire : retirer une à une chaque contrainte du MUS et re-checker — chaque sous-ensemble doit être SATISFIABLE.

Étapes : 8 assert_and_track étiquetés ; boucle sur le résultat de compute_mus ; pour chaque membre, check() sur les autres seuls -> sat attendu.

# Exercice 1 : irreductibilite verifiee membre par membre
# TODO etudiant :
# Etape 1 : w = Int('w') ; 8 contraintes etiquetees (chaine en conflit + compatibles)
# Etape 2 : mus = compute_mus(couples) -> sous-ensemble irreductible
# Etape 3 : pour chaque (formule, etiquette) du MUS : re-check SANS elle -> sat attendu
result = None  # TODO etudiant
print("Exercice 1 a completer : verifiez que chaque membre du MUS est essentiel")
Exercice 1 a completer : verifiez que chaque membre du MUS est essentiel

Exercice 2 - Arête transitive contre chemin détaillé

Encodez 3 tâches t0, t1, t2 (durée 2) en chaîne t0 -> t1 -> t2 plus l’arête transitive directe t0 -> t2, avec une échéance qui rend le tout insatisfiable. Comparez la taille du core brut (unsat_core()) et la taille du MUS : le MUS doit écarter le chemin détaillé au profit de l’arête transitive.

Étapes : assert_and_track pour chaque arête + échéance ; len(unsat_core()) vs len(compute_mus(...)) -> le MUS est plus court.

# Exercice 2 : arete transitive contre chemin detaille
# TODO etudiant :
# Etape 1 : start_0/1/2 = Int ; duree 2 ; aretes t0->t1, t1->t2 ET transitive t0->t2, echeance
# Etape 2 : s.check() + s.unsat_core() -> taille du core brut
# Etape 3 : compute_mus sur les memes couples -> taille du MUS (plus petite)
taille_mus = None  # TODO etudiant
print("Exercice 2 a completer : comparez |core brut| et |MUS| sur le meme systeme")
Exercice 2 a completer : comparez |core brut| et |MUS| sur le meme systeme

Exercice 3 - Diagnostic : laquelle relâcher, décidé par le MUS

Construisez une spécification surcontrainte sur h où le core brut contient ~5 contraintes mais où le MUS en isole 2. Relâchez une seule contrainte du MUS, re-checkez : le système devient SATISFIABLE — preuve que le MUS, pas le core brut, désigne le relâchement minimal.

Étapes : encoder la spécification étiquetée ; compute_mus ; retirer un membre du MUS ; re-check() -> sat.

# Exercice 3 : diagnostic actionnable, decide par le MUS
# TODO etudiant :
# Etape 1 : spec surcontrainte sur h etiquetee (core brut ~5 contraintes)
# Etape 2 : mus = compute_mus(...) -> isole 2 contraintes essentielles
# Etape 3 : retirer UNE contrainte du MUS, re-check -> sat (systeme reparable d'un geste)
result = None  # TODO etudiant
print("Exercice 3 a completer : relachez une contrainte du MUS et re-checkez")
Exercice 3 a completer : relachez une contrainte du MUS et re-checkez

Conclusion

Le MUS referme l’arc ouvert par le 13 : là où unsat_core() rend le conflit visible, le MUS le rend irréductible — la preuve la plus courte qu’aucune contrainte ne puisse être retirée sans faire disparaître le conflit. Sur une spécification surcontrainte, c’est le diagnostic ultime : non seulement quelles contraintes conflitent, mais lesquelles relâcher au strict minimum.

La série poursuit avec Z3-14 - Bit-vectors : l’arithmétique bornée des machines, où le débordement devient une propriété décidable — et se prouve.

Retour au sommet