Z3-Python 01 — Introduction a la resolution de contraintes SMT

Navigation : Index | Z3-Python-01b (style declaratif) >> | Twin C# 01

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez : 1. Modeliser un problème sous forme de contraintes et le resoudre avec le solveur Z3 en Python 2. Distinguer les reponses sat, unsat et unknown du solveur 3. Manipuler les types de base : entiers (Int), booléens (Bool) et reels (Real) 4. Utiliser l’optimisation (Optimize) pour maximiser/minimiser une variable sous contraintes

Prerequis

  • Python 3.10+
  • Notions de logique booleenne et d’arithmetic de base

Duree estimee : ~30 min

Z3 est un solveur SMT (Satisfiability Modulo Théories) developpe par Microsoft Research. Un solveur SMT determine si un ensemble de contraintes logiques et arithmetiques peut etre satisfait, et si oui, fournit un modèle (une assignation concrete des variables). Cette serie utilise z3-py, le binding Python officiel (package pip z3-solver), qui expose l’integralite de l’API Z3 sans la limitation d’un binding declaratif. Pour les fondements théoriques de la resolution SMT (DPLL(T)) et la presentation du solveur Z3 lui-même, voir de Moura & Bjorner, Z3: An Efficient SMT Solver (TACAS 2008) et Nieuwenhuis, Oliveras & Tinelli, Solving SAT and SAT Modulo Théories: From an Abstract DPLL Procedure to DPLL(T) (JACM 2006) ; les tactiques (notebook 3) et MaxSAT (notebook 6) sont ancrees dans la section References du README.

# Imports et verification de l'environnement
# Le package pip s'appelle 'z3-solver' (et non 'z3').
# Dans cet environnement il est deja installe. Pour l'installer ailleurs :
# !pip install z3-solver

from z3 import *

print(f"Imports OK : z3-solver version {get_version_string()}")
Imports OK : z3-solver version 4.16.0

1. Premier solveur : entiers et satisfaction

Commencons par le cas le plus simple : deux variables entieres x et y soumises a un ensemble de contraintes lineaires. Le patron d’usage est toujours le même :

  1. Créer un Solver()
  2. Declarer des variables typees (Int, Real, Bool…)
  3. Ajouter des contraintes avec s.add(...)
  4. Verifier la satisfiabilite avec s.check() -> renvoie sat, unsat ou unknown
  5. Si sat, extraire un modèle avec s.model()
# Premier exemple : deux entiers sous contraintes lineaires
s = Solver()
x = Int('x')
y = Int('y')

# Contraintes : x + y = 10, x et y strictement positifs, x > y
s.add(x + y == 10)
s.add(x > 0, y > 0)
s.add(x > y)

resultat = s.check()
print("Resultat de s.check() :", resultat)

if resultat == sat:
    m = s.model()
    print("Modele trouve :")
    print("  x =", m[x].as_long())
    print("  y =", m[y].as_long())
    print("  Verification : x + y =", m[x].as_long() + m[y].as_long())
Resultat de s.check() : sat
Modele trouve :
  x = 9
  y = 1
  Verification : x + y = 10

Interpretation : sat / unsat / unknown

Sortie obtenue : le solveur repond sat et fournit un modèle concret (x = 9, y = 1 ici, parmi d’autres possibles).

Reponse Signification Action
sat Il existe au moins une assignation satisfaisant toutes les contraintes s.model() donne un exemple
unsat Aucune assignation ne peut satisfaire les contraintes (contradiction) Le système est sur-contraint
unknown Le solveur ne peut pas conclure (trop complexe, quantificateurs, timeout) Simplifier ou changer de tactique

Points cles : 1. s.model() ne donne qu’un modèle parmi potentiellement plusieurs ; Z3 ne garantit pas lequel. 2. Les variables Z3 sont des objets symboliques : x + y == 10 construit une formule, n’evaluate rien tant que check() n’est pas appele. 3. m[x].as_long() convertit la valeur Z3 en entier Python natif.

# Exemple insatisfiable : contraintes contradictoires
s2 = Solver()
x = Int('x')
s2.add(x > 5)
s2.add(x < 3)

print("Contraintes : x > 5 ET x < 3")
print("Resultat de s.check() :", s2.check())

# Le noyau d'insatisfiabilite (unsat core) identifie les contraintes en conflit.
# Pour l'obtenir, il faut nommer les assertions avec assert_and_track.
s3 = Solver()
x = Int('x')
c1 = Bool('c1')
c2 = Bool('c2')
s3.assert_and_track(x > 5, c1)
s3.assert_and_track(x < 3, c2)
print("\nAvec assert_and_track :")
print("Resultat :", s3.check())
print("Noyau d'insatisfiabilite (contraintes en conflit) :", s3.unsat_core())
Contraintes : x > 5 ET x < 3
Resultat de s.check() : unsat

Avec assert_and_track :
Resultat : unsat
Noyau d'insatisfiabilite (contraintes en conflit) : [c2, c1]

Interpretation : contradiction et noyau d’insatisfiabilite

Sortie obtenue : s2.check() renvoie unsat, et le noyau identifie les deux assertions contradictoires.

Concept Description
unsat Aucun entier x ne peut etre simultanement > 5 et < 3
unsat_core() Sous-ensemble minimal d’assertions responsables du conflit (necessite assert_and_track)

Note technique : Le noyau d’insatisfiabilite est precieux en pratique : il pointe exactement les contraintes a assouplir pour rendre un problème realisable (utile en planification, configuration, debogage de contrats).

2. Logique booleenne : Bool, And, Or, Not, Implies

Z3 manipule des variables booleennes et des connecteurs logiques. Illustrons-le avec un classique : le paradoxe du menteur.

Trois personnes A, B et C. L’une dit la verite, les autres mentent. On sait que : - A dit : « B ment » - B dit : « C ment » - C dit : « A et B mentent tous les deux »

Qui dit la verite ? Modelisons True = « dit la verite ».

# Le menteur : qui dit la verite ?
s = Solver()
A = Bool('A')  # A dit la verite ?
B = Bool('B')
C = Bool('C')

# A affirme que B ment : si A dit vrai, alors B est faux.
s.add(A == Not(B))
# B affirme que C ment
s.add(B == Not(C))
# C affirme que A et B mentent tous les deux
s.add(C == And(Not(A), Not(B)))

print("Resultat :", s.check())
m = s.model()
print("A dit la verite :", bool(m[A]))
print("B dit la verite :", bool(m[B]))
print("C dit la verite :", bool(m[C]))
veridique = "A" if bool(m[A]) else ("B" if bool(m[B]) else "C")
print("\nSynthese :", veridique, "dit la verite.")
Resultat : sat
A dit la verite : False
B dit la verite : True
C dit la verite : False

Synthese : B dit la verite.

Interpretation : raisonnement propositionnel

Sortie obtenue : le solveur identifie qui dit la verite de maniere coherente avec les trois affirmations.

Connecteur Z3 Equivalent logique
And(p, q) \(p \land q\)
Or(p, q) \(p \lor q\)
Not(p) \(\lnot p\)
Implies(p, q) \(p \Rightarrow q\)
Xor(p, q) \(p \oplus q\)

Points cles : 1. L’opérateur Python == est surcharge pour exprimer l’equivalence logique entre deux formules Z3. 2. Z3 resout instantanement des systèmes propositionnels qui necessiteraient une enumeration exhaustive manuelle.

3. Nombres reels : Real et l’arithmetic rationnelle

Le type Real modelise des nombres rationnels. Z3 travaille en arithmetic exacte (pas de virgule flottante) : les fractions sont manipulees symboliquement. Ideal pour des problemes de partage ou de dosage précis.

# Arithmetic rationnelle exacte avec Real.
# Trois enfants se partagent 10 euros.
# L'aine recoit le double du cadet, le benjamin recoit 1 euro de plus que le cadet.
s = Solver()
aine = Real('aine')
cadet = Real('cadet')
benjamin = Real('benjamin')

s.add(aine + cadet + benjamin == 10)
s.add(aine == 2 * cadet)
s.add(benjamin == cadet + 1)

print("Partage de 10 euros :", s.check())
m = s.model()
print(f"  Aine     : {m[aine]} euros")
print(f"  Cadet    : {m[cadet]} euros")
print(f"  Benjamin : {m[benjamin]} euros")
Partage de 10 euros : sat
  Aine     : 9/2 euros
  Cadet    : 9/4 euros
  Benjamin : 13/4 euros

Interpretation : arithmetic exacte

Sortie obtenue : le solveur trouve aine = 9/2, cadet = 9/4, benjamin = 13/4 (soit 4,5 EUR, 2,25 EUR et 3,25 EUR).

Variable Fraction Decimal
Aine 9/2 4,5 EUR
Cadet 9/4 2,25 EUR
Benjamin 13/4 3,25 EUR

Points cles : 1. Z3 manipule les fractions exactes, jamais d’erreur d’arrondi flottant. 2. Verification : \(9/2 + 9/4 + 13/4 = 18/4 + 9/4 + 13/4 = 40/4 = 10\). 3. Real est ideal pour les problemes de partage, de dosage ou de conversion ou la precision exacte compte.

4. Optimisation : Optimize

La classe Optimize etend Solver en ajoutant un objectif a maximiser ou minimiser sous contraintes. C’est l’outil de choix pour l’allocation de ressources, le sac a dos ou la planification.

Modelisons un mini-sac a dos : on dispose de 3 objets de valeurs et poids différents, et d’une capacite maximale. On cherche a maximiser la valeur sans depasser le poids.

# Mini sac a dos : maximiser la valeur transportee sous contrainte de poids.
opt = Optimize()

# Variables : nombre d'unites de chaque objet (entiers >= 0)
n_a = Int('n_a')  # objet A : valeur 4, poids 2
n_b = Int('n_b')  # objet B : valeur 5, poids 3
n_c = Int('n_c')  # objet C : valeur 7, poids 5

# Domaine : quantites non negatives
opt.add(n_a >= 0, n_b >= 0, n_c >= 0)

# Capacite maximale du sac : 10 kg
opt.add(2 * n_a + 3 * n_b + 5 * n_c <= 10)

# Objectif : maximiser la valeur totale
valeur = 4 * n_a + 5 * n_b + 7 * n_c
opt.maximize(valeur)

print("Optimisation :", opt.check())
m = opt.model()
print("Solution optimale :")
print(f"  Objet A (v=4, p=2) : {m[n_a]} unites")
print(f"  Objet B (v=5, p=3) : {m[n_b]} unites")
print(f"  Objet C (v=7, p=5) : {m[n_c]} unites")
poids_total = 2 * m[n_a].as_long() + 3 * m[n_b].as_long() + 5 * m[n_c].as_long()
valeur_totale = 4 * m[n_a].as_long() + 5 * m[n_b].as_long() + 7 * m[n_c].as_long()
print(f"  Poids total : {poids_total} / 10 kg")
print(f"  Valeur totale : {valeur_totale}")
Optimisation : sat
Solution optimale :
  Objet A (v=4, p=2) : 5 unites
  Objet B (v=5, p=3) : 0 unites
  Objet C (v=7, p=5) : 0 unites
  Poids total : 10 / 10 kg
  Valeur totale : 20

Interpretation : optimisation sous contraintes

Sortie obtenue : Z3 trouve la combinaison maximisant la valeur sans depasser 10 kg.

Classe Rôle Equivalent
Solver Verifier la satisfiabilite « Existe-t-il une solution ? »
Optimize Trouver la meilleure solution « Quelle est la solution optimale ? »

Points cles : 1. opt.maximize(expr) cherche le maximum ; opt.minimize(expr) cherche le minimum. 2. L’optimisation combinatoire d’entiers est NP-difficile, mais Z3 (moteur branches-bornes) reste efficace sur de petites instances. 3. On peut combiner plusieurs objectifs avec des priorites (optimisation lexicographique ou ponderee).

Note technique : Optimize etend Solver. Tout ce qui fonctionne avec Solver (types, contraintes) s’applique aussi a Optimize.

Aller plus loin : un cas ou le glouton echoue, et ou Optimize devient indispensable

L’exemple precedent etait un sac a dos non borne (variables >= 0) avec un objet dominant : A a la meilleure densite (valeur/poids), donc la strategie gloutonne - remplir le sac en priorisant les objets les plus denses - donne deja l’optimum. Dans ce cas degenere, le moteur branches-boundes de Optimize n’apporte rien : une heuristique triviale suffit.

Pour voir l’apport d’un solveur exact, il faut un probleme ou le glouton echoue. Passons au sac a dos 0/1 : chaque objet est pris une fois au plus (variable binaire 0 ou 1), avec une instance classique (Cormen, Leiserson, Rivest, Stein) concue pour pieger le glouton. On compare alors les deux approches cote a cote.

# Sac a dos 0/1 (binaire) : pourquoi Optimize est indispensable.
# Instance classique (Cormen et al.) : 3 objets, capacite 50 kg.
# (nom, valeur, poids)
objets = [("A", 60, 10), ("B", 100, 20), ("C", 120, 30)]
CAPACITE = 50

# --- 1. Heuristique gloutonne : trier par densite decroissante, prendre tant que possible ---
ordre = sorted(range(len(objets)), key=lambda i: objets[i][1] / objets[i][2], reverse=True)
poids_g, valeur_g, choix_g = 0, 0, []
for i in ordre:
    if poids_g + objets[i][2] <= CAPACITE:
        poids_g += objets[i][2]
        valeur_g += objets[i][1]
        choix_g.append(objets[i][0])

print("Glouton (densite) :", choix_g)
print(f"  poids = {poids_g}/{CAPACITE} kg (capacite inutilisee : {CAPACITE - poids_g} kg)")
print(f"  valeur = {valeur_g}")
print()
# --- 2. Z3 Optimize : resolution EXACTE du sac a dos 0/1 ---
opt = Optimize()
x = [Int(f"x_{i}") for i in range(len(objets))]   # x_i = 1 si l'objet i est pris, 0 sinon
for xi in x:
    opt.add(xi >= 0, xi <= 1)                       # variable binaire 0/1
opt.add(Sum([objets[i][2] * x[i] for i in range(len(objets))]) <= CAPACITE)
opt.maximize(Sum([objets[i][1] * x[i] for i in range(len(objets))]))

print("Optimisation Z3 :", opt.check())
m = opt.model()
choix_z = [objets[i][0] for i in range(len(objets)) if m[x[i]].as_long() == 1]
poids_z = sum(objets[i][2] for i in range(len(objets)) if m[x[i]].as_long() == 1)
valeur_z = sum(objets[i][1] for i in range(len(objets)) if m[x[i]].as_long() == 1)
print("Optimum Z3      :", choix_z)
print(f"  poids = {poids_z}/{CAPACITE} kg (capacite inutilisee : {CAPACITE - poids_z} kg)")
print(f"  valeur = {valeur_z}")
print()
# --- 3. Confrontation : l'ecart rend visible la valeur d'Optimize ---
ecart = valeur_z - valeur_g
print(f"Ecart glouton -> optimum : {ecart} ({100 * ecart / valeur_z:.0f} % de valeur perdue)")
print("-> le glouton est SOUS-OPTIMAL : Optimize trouve une meilleure solution.")
Glouton (densite) : ['A', 'B']
  poids = 30/50 kg (capacite inutilisee : 20 kg)
  valeur = 160

Optimisation Z3 : sat
Optimum Z3      : ['B', 'C']
  poids = 50/50 kg (capacite inutilisee : 0 kg)
  valeur = 220

Ecart glouton -> optimum : 60 (27 % de valeur perdue)
-> le glouton est SOUS-OPTIMAL : Optimize trouve une meilleure solution.

Interpretation : pourquoi le glouton echoue (et pourquoi Optimize gagne)

Sortie obtenue :

Methode Objets choisis Poids utilise Valeur
Glouton (densite) A, B 30 / 50 kg 160
Z3 Optimize (exact) B, C 50 / 50 kg 220

Le glouton echoue de deux manieres cumulees :

  1. Mauvaise composition. Il prend d’abord A (densite 6,0) puis B (densite 5,0), atteignant 30 kg. Il ne peut alors plus faire rentrer C (30 kg) : il abandonne. La solution optimale abandonne A pour liberer de la place et prend B + C (50 kg, valeur 220). Le glouton est myope : il ne peut pas “voir” que renoncer a l’objet le plus dense libere assez de capacite pour un objet plus valuable.
  2. Capacite gaspillee. Le glouton laisse 20 kg inutilises (30/50), alors que l’optimum remplit le sac parfaitement (50/50). Un sac a dos 0/1 n’est pas juste un probleme de “prendre le maximum d’objets” : c’est un equilibre global que seul un parcours exact du domaine retrouve.

Lecon : le sac a dos 0/1 est NP-difficile. Aucune heuristique gloutonne ne garantit l’optimum (le glouton peut etre arbitrairement mauvais sur certaines instances). Optimize, par son exploration branches-boundes avec preuves de borne, garantit l’optimum global - c’est precisement la capacite distinctive que la cellule precedente (instance degeneree) ne permettait pas d’exercer.

Astuce : variables binaires x_i dans {0, 1} modelisees par Int + contraintes xi >= 0, xi <= 1. Z3 expose aussi un type Bool mieux adapte aux pures decisions vrai/faux, mais la formulation entiere 0/1 se prete naturellement au calcul de poids et de valeur via Sum.

Exercice 1 : Triplets pythagoriciens

Enonce

Un triplet pythagoricien est un ensemble d’entiers \((a, b, c)\) tels que \(a^2 + b^2 = c^2\). Par exemple \((3, 4, 5)\).

Ecrivez un programme Z3 qui trouve un triplet pythagoricien avec \(a, b, c\) tous positifs, \(a < b < c\) et \(c \leq 20\).

Indices :

  • Utilisez Int('a'), Int('b'), Int('c') et la contrainte a * a + b * b == c * c.
  • Ajoutez a < b, b < c, c <= 20 et a > 0.
  • Pensez a la fonction s.check() puis s.model().
# EXERCICE 1 : Trouver un triplet pythagoricien avec Z3.

def trouver_triplet_pythagoricien(borne_max: int = 20) -> tuple:
    """Retourne un triplet (a, b, c) tel que a^2 + b^2 = c^2, a < b < c <= borne_max.

    # Indice : creez un Solver, des variables Int, ajoutez les contraintes,
    #           puis appelez check() et model().
    # Etape 1 : declarer les variables a, b, c
    # Etape 2 : ajouter a*a + b*b == c*c et les bornes
    # Etape 3 : extraire le modele et retourner (a, b, c)
    """
    # TODO etudiant : implémentez la résolution
    return None  # TODO etudiant : remplacer par le triplet trouvé

triplet = trouver_triplet_pythagoricien(20)
print("Triplet pythagoricien :", triplet)
Triplet pythagoricien : None

Exercice 2 : Ordonnancement de deux tâches

Enonce

Deux tâches T1 et T2 doivent etre planifiees. Chacune a une duree (en heures) et ne peut commencer qu’a un entier debut >= 0. Les contraintes sont : - T1 dure 3 heures, T2 dure 2 heures. - Les deux tâches ne peuvent pas se chevaucher dans le temps. - T1 doit commencer avant T2. - On veut que T2 se termine le plus tot possible.

Modelisez ce problème avec Z3 et trouvez l’heure de debut optimale de chaque tâche.

Indices :

  • Variables : d1 = Int('debut_T1'), d2 = Int('debut_T2'), toutes >= 0.
  • Comme T1 commence avant T2 et ne se chevauchent pas, ajoutez d2 >= d1 + 3.
  • Utilisez Optimize pour minimiser d2 + 2 (la fin de T2).
# EXERCICE 2 : Ordonnancer deux taches sans chevauchement.

def ordonnancer_taches() -> dict:
    """Planifie T1 (3h) et T2 (2h) sans chevauchement, T2 finissant au plus tot.

    # Indice : utilisez Optimize avec debut_T1 >= 0, debut_T2 >= 0.
    # Etape 1 : declarer debut_T1, debut_T2
    # Etape 2 : contrainte debut_T2 >= debut_T1 + 3 (pas de chevauchement, T1 avant)
    # Etape 3 : minimiser debut_T2 + 2
    """
    # TODO etudiant : implémentez l'ordonnancement optimal
    return None  # TODO etudiant : remplacer par {'debut_T1': ..., 'debut_T2': ...}

planning = ordonnancer_taches()
print("Planning optimal :", planning)
Planning optimal : None

Exercice 3 : Allocation de ressources (Optimize)

Enonce

Une PME produit deux produits P et Q. Chaque unite de P rapporte 30 EUR et consomme 2 heures de machine ; chaque unite de Q rapporte 50 EUR et consomme 4 heures. L’atelier dispose de 20 heures de machine au total. On veut au moins 2 unites de chaque produit.

Trouvez la production (P, Q) qui maximise le profit sous ces contraintes.

Indices :

  • Variables : p = Int('p'), q = Int('q').
  • Contraintes : p >= 2, q >= 2, 2*p + 4*q <= 20.
  • Objectif : maximize(30*p + 50*q).
# EXERCICE 3 : Maximiser le profit de production sous contrainte de machine.

def allocation_optimale() -> dict:
    """Retourne {'P': p, 'Q': q, 'profit': profit} maximisant le profit.

    # Indice : utilisez Optimize, p >= 2, q >= 2, 2*p + 4*q <= 20.
    # Etape 1 : declarer p, q (Int)
    # Etape 2 : ajouter les contraintes de production
    # Etape 3 : maximize(30*p + 50*q) et extraire le modele
    """
    # TODO etudiant : implémentez l'allocation optimale
    return None  # TODO etudiant : remplacer par le résultat

resultat = allocation_optimale()
print("Allocation optimale :", resultat)
Allocation optimale : None

Recapitulatif

Ce notebook a pose les fondations de la resolution de contraintes avec z3-py :

Concept API Z3 Usage
Solveur de base Solver, add, check, model Satisfiabilite d’un système de contraintes
Insatisfiabilite unsat, unsat_core Detecter et expliquer les contradictions
Logique booleenne Bool, And, Or, Not, Implies Raisonnement propositionnel
Nombres reels Real Arithmetic rationnelle exacte
Optimisation Optimize, maximize, minimize Trouver la meilleure solution

Le changement de paradigme est fondamental : vous decrivez ce que vous voulez (les contraintes), pas comment l’obtenir (l’algorithme). Le notebook suivant, Z3-Python-02 Sudoku, applique cette approche declarative a un problème concret : la resolution de grilles de Sudoku.

Retour au sommet