Le module Z3 de Python : logique, contraintes et résolution de problèmes

1. Introduction : Le module Z3 de Python

La résolution de problèmes par contraintes est devenue un paradigme central en vérification
formelle, planification, analyse de programmes, cybersécurité et optimisation discrète. Plutôt
que d’écrire un algorithme spécifique pour chaque problème, l’utilisateur exprime un ensemble
de variables et de propriétés que toute solution valide doit satisfaire. Le solveur se charge ensuite
d’explorer l’espace de recherche.

Dans cet écosystème, Z3 occupe une place singulière : il combine les techniques SAT modernes
avec des théories riches comme l’arithmétique linéaire, les tableaux, les fonctions non interprétées
et les bit-vecteurs. Le module z3 pour Python rend ces capacités accessibles dans un environnement de prototypage rapide, ce qui le rend particulièrement adapté à la recherche scientifique
et à l’enseignement.

Cet article poursuit trois objectifs :

• expliquer les bases théoriques de la logique SMT ;
• montrer comment construire un modèle en Python avec Z3 ;
• illustrer la résolution de problèmes typiques à l’aide d’exemples commentés.

2. Fondements : logique propositionnelle, SAT et SMT

La logique propositionnelle manipule des variables booléennes reliées par des connecteurs tels
que ∧, ∨, ¬ et ⇒. Le problème SAT consiste à déterminer s’il existe une valuation rendant une
formule vraie.

La SMT généralise ce cadre en autorisant des objets plus structurés : entiers, réels, tableaux,
suites de bits ou fonctions abstraites. On ne cherche plus simplement une valuation booléenne,
mais un modèle satisfaisant simultanément une structure logique et les axiomes d’une ou plu-
sieurs théories.
Formellement, un problème SMT peut s’écrire comme la recherche d’un modèle M tel que
M |= φ, où φ est une formule du premier ordre restreinte à des théories décidables ou semi-décidables
traitées efficacement par le solveur.

L’intérêt pratique est majeur : de nombreux problèmes informatiques peuvent se reformuler sous
la forme de contraintes, par exemple :

• vérifier l’absence d’état invalide dans un programme ;
• trouver une affectation de ressources compatible avec des règles ;
• synthétiser des entrées provoquant un comportement particulier ;
• démontrer qu’une configuration est impossible

3. Architecture conceptuelle de Z3

Z3 repose sur une architecture hybride. Le solveur booléen traite le squelette propositionnel de
la formule, tandis que des solveurs spécialisés vérifient la cohérence des contraintes de théorie.
Le dialogue entre ces deux couches permet d’éliminer rapidement de vastes portions de l’espace
de recherche.

On peut synthétiser ce fonctionnement par le diagramme suivant :

Cette organisation présente deux avantages :

• 1. la factorisation des techniques SAT très optimisées ;
• 2. l’ajout modulaire de théories selon les besoins du problème.

4. Prise en main du module Python z3

L’usage typique du module suit quatre étapes :

• 1. déclarer les variables ;
• 2. construire les contraintes ;
• 3. les ajouter à un solveur ;
• 4. interroger le résultat puis le modèle

Exemple minimal de résolution avec Z3

from z3 import *
x = Int('x')
y = Int('y')

s = Solver()

s.add(x > 0)
s.add(y > x)
s.add(x + y == 10)

if s.check() == sat:
    m = s.model()
    print(m[x], m[y])

Dans cet exemple, les variables x et y sont de type entier. Le solveur recherche une valuation
telle que les trois contraintes soient vraies simultanément. Si le résultat est sat, la méthode
model() renvoie une solution concrète.

4.1 Principaux types manipulés

Le module Python offre plusieurs sortes de variables, chacune correspondant à une théorie ou à
une représentation logique particulière.

Le choix du type est déterminant : il influence à la fois l’expressivité du modèle et l’efficacité de
la résolution

5. Modéliser un problème par contraintes

Une bonne modélisation repose sur trois principes :

• choisir des variables fidèles au problème ;
• exprimer les règles sous forme de contraintes simples ;
• casser les symétries ou borner le domaine pour réduire la recherche.

5.1 Cohérence d’un emploi du temps

Supposons que trois tâches A, B et C doivent être planifiées sur des créneaux entiers. On impose :

• A, B, C ∈ {1, 2, 3},
• A ≠ B,
• B < C.

La traduction Z3 est directe :

from z3 import *
A, B, C = Ints('A B C')
s = Solver()
for task in [A, B, C]:
    s.add(And(task >= 1, task <= 3))
s.add(A != B)
s.add(B < C)

L’intérêt scientifique d’un tel encodage est sa généralisation : il suffit d’ajouter des variables et
des contraintes pour traiter des problèmes d’ordonnancement plus riches.

5.2 Puzzle logique

Les puzzles de type Sudoku, Einstein ou Latin square (ou les jeux comme Juniper-U , des activités comme Les 16 immeubles ) se prêtent bien à Z3. Par exemple, pour
imposer que plusieurs variables entières prennent des valeurs distinctes, on utilise la contrainte
Distinct.

from z3 import *
x1, x2, x3, x4 = Ints('x1 x2 x3 x4')
s = Solver()
s.add(Distinct(x1, x2, x3, x4))
s.add([And(v >= 1, v <= 4) for v in [x1, x2, x3, x4]])

5.3 Raisonnement sur les bit-vecteurs

Les bit-vecteurs sont essentiels pour l’analyse bas niveau, car ils reproduisent la sémantique des
registres machine sur un nombre fixé de bits.

from z3 import *
x = BitVec(’x’, 8)
s = Solver()
s.add(x + 1 == 0)

Ici, la solution correspond à la valeur 255, car l’addition est effectuée modulo 28. Ce type d’en-
codage est crucial pour la détection d’overflow, l’analyse symbolique et la recherche de contre-
exemples en sécurité logicielle.

6. Vérification et extraction de modèles

Le solveur retourne généralement l’un des trois statuts suivants :

• sat : les contraintes admettent au moins une solution ;
• unsat : aucune solution n’existe ;
• unknown : Z3 ne peut pas conclure avec la procédure engagée.

Dans le cas sat, le modèle fourni doit être interprété comme un témoin de satisfiabilité. Dans
le cas unsat, on peut parfois analyser un sous-ensemble minimal de contraintes contradictoires,
ce qui aide à diagnostiquer une spécification erronée.

from z3 import *
x = Int('x')
s = Solver()
s.add(x > 5)
s.add(x < 3)
print(s.check())

Ce fragment renvoie unsat. En recherche, ce comportement est très utile pour démontrer l’in-
compatibilité d’hypothèses, vérifier des invariants ou réfuter des conjectures sur un domaine
fini.

6.2 Cas unknown : causes et interprétation

Le statut unknown est moins intuitif mais théoriquement fondamental. Il signifie que Z3 a abandonné la recherche sans pouvoir trancher. Plusieurs situations le provoquent.

Quantificateurs universels ou existentiels. Dès qu’une formule contient des quantificateurs sur des domaines infinis, la décidabilité n’est plus garantie. Z3 tente des heuristiques d’instanciation (E-matching), mais peut échouer si elles ne convergent pas.

from z3 import *
x, y = Ints('x y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(ForAll(x, f(x) > 0))
s.add(f(y) < 0)
print(s.check())  # souvent unknown selon la version et la config

Arithmétique non linéaire. La multiplication de deux variables (x * y) sort du fragment linéaire, pour lequel Z3 dispose d’algorithmes complets. En non linéaire, le solveur recourt à des approximations qui peuvent ne pas suffire.

from z3 import *
x, y = Reals('x y')
s = Solver()
s.add(x * x + y * y < 1)
s.add(x * y > 10)
print(s.check())  # unsat ici, mais des formules NL plus complexes retournent unknown

Timeout ou limite de ressources. On peut fixer un temps maximal via set_param ou via les paramètres du solveur. Lorsque le délai est atteint, Z3 rend unknown plutôt que de bloquer indéfiniment.

from z3 import *
set_param('timeout', 1000)  # 1 seconde en millisecondes
x = Int('x')
s = Solver()
s.add(x > 0)
print(s.check())

Que faire face à unknown ?

Plusieurs stratégies permettent d’y remédier :

• Changer de théorie : remplacer des Real par des Int ou des BitVec si le problème s’y prête, afin de rester dans un fragment décidable ;
• Linéariser manuellement : reformuler les contraintes non linéaires en introduisant des variables auxiliaires ou des bornes explicites ;
• Utiliser des tactiques : Z3 expose des tactiques de résolution (then, try_for, qe pour l’élimination de quantificateurs) qui peuvent débloquer certains cas ;
• Augmenter le timeout avec prudence, ou découper le problème en sous-problèmes plus simples ;
• Interpréter prudemment : unknown n’est ni sat ni unsat — on ne peut rien conclure sur la satisfiabilité du problème original.

Ce dernier point est crucial en contexte scientifique : un unknown ne valide ni n’invalide une hypothèse. Il signale simplement une limite de l’outil face à la complexité du modèle proposé.

7. Optimisation et variantes avancées

Z3 propose un objet Optimize permettant de maximiser ou minimiser
certaines expressions.

from z3 import *
x, y = Ints('x y')
opt = Optimize()
opt.add(x >= 0, y >= 0, x + y <= 12)
opt.maximize(3*x + 2*y)
if opt.check() == sat:
    print(opt.model())

Cette fonctionnalité est pertinente pour les problèmes de configuration, d’allocation et de synthèse, lorsque l’on souhaite non seulement trouver une solution valide, mais aussi une solution
optimale selon un critère donné.
Parmi les mécanismes avancés, on peut également citer :

• les solveurs incrémentaux avec push() et pop() ;
• les hypothèses temporaires pour l’exploration de cas ;
• les symboles non interprétés pour la modélisation abstraite ;
• les quantificateurs, plus expressifs mais souvent plus coûteux ;
• les tactiques, qui orientent la stratégie de résolution.

8. Bonnes pratiques de modélisation

L’expérience montre que les meilleures performances proviennent rarement d’un modèle pure-
ment naïf. Quelques bonnes pratiques se dégagent :

1. borner les domaines dès que possible ;
2. préférer des contraintes simples à des formules trop imbriquées ;
3. réduire les symétries pour éviter des solutions équivalentes ;
4. valider les modèles progressivement avec des jeux de test ;
5. choisir la bonne théorie selon la sémantique recherchée.

Par exemple, un problème de calcul machine doit souvent être encodé avec des BitVec plu-
tôt qu’avec des entiers mathématiques, faute de quoi les phénomènes de débordement seraient
ignorés.

9. Apports et limites de Z3 dans un cadre scientifique

Le module Python de Z3 offre plusieurs avantages aux chercheurs :

• une expressivité élevée pour modéliser rapidement une hypothèse ;
• une intégration naturelle dans des scripts expérimentaux ;
• une capacité à produire des contre-exemples exploitables ;
• un pont entre preuve formelle, exploration symbolique et prototypage.

Cependant, certaines limites doivent être soulignées. Les performances dépendent fortement de
l’encodage. Les quantificateurs peuvent rendre la recherche difficile. Enfin, un modèle incorrectement spécifié peut fournir une solution logiquement valide mais scientifiquement non pertinente.
La rigueur de la formalisation demeure donc essentielle.

10. Conclusion

Le module z3 de Python constitue un outil puissant pour la logique appliquée, la modélisation par
contraintes et la résolution de problèmes. En combinant l’expressivité de Python et la puissance
d’un solveur SMT moderne, il permet d’aborder de manière uniforme des tâches très diverses :
vérification, planification, synthèse, analyse symbolique et optimisation.

Lire aussi

Documentation officielle et code source

• Dépôt GitHub de Z3 (Microsoft Research / Z3Prover) Sources, exemples par langage, notes de version → https://github.com/Z3Prover/z3
• Référence complète de l’API Python (z3py) Documentation générée automatiquement depuis le code source → https://z3prover.github.io/api/html/namespacez3py.html
• Package PyPI z3-solver Installation via pip, historique des versions (dernière : 4.16.0) → https://pypi.org/project/z3-solver/

Tutoriel interactif

• Z3Py Guide (tutoriel officiel de l’équipe Z3) Introduction progressive avec exemples commentés : entiers, tableaux, bit-vecteurs, Sudoku → https://ericpony.github.io/z3py-tutorial/guide-examples.htm

Publication scientifique fondatrice

• De Moura, L. & Bjørner, N. — Z3: An Efficient SMT Solver (TACAS 2008) L’article original présentant l’architecture et les choix de conception de Z3 → https://link.springer.com/chapter/10.1007/978-3-540-78800-3_24 DOI : 10.1007/978-3-540-78800-3_24

Pour aller plus loin

• Liste des publications de l’équipe Z3 (wiki GitHub) Articles sur l’optimisation, les théories non linéaires, les séquences, etc. → https://github.com/Z3Prover/z3/wiki/Publications