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 :
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 :
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 :
L’usage typique du module suit quatre étapes :
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.
Le module Python offre plusieurs sortes de variables, chacune correspondant à une théorie ou à
une représentation logique particulière.
| Type Z3 | Usage principal |
|---|---|
| Bool | logique propositionnelle et garde de contraintes |
| Int | arithmétique entière |
| Real | rationnelle et réelle symbolique |
| BitVec | calcul machine, masques, overflow |
| Array | mémoire symbolique, tables et fonctions finies |
| String | chaînes et séquences |
| Function | symboles non interprétés |
Le choix du type est déterminant : il influence à la fois l’expressivité du modèle et l’efficacité de
la résolution
Une bonne modélisation repose sur trois principes :
Supposons que trois tâches A, B et C doivent être planifiées sur des créneaux entiers. On impose :
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.
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]])
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.
Le solveur retourne généralement l’un des trois statuts suivants :
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.
unknown : causes et interprétationLe 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 :
Real par des Int ou des BitVec si le problème s'y prête, afin de rester dans un fragment décidable ;then, try_for, qe pour l'élimination de quantificateurs) qui peuvent débloquer certains cas ;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é.
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 :
L’expérience montre que les meilleures performances proviennent rarement d’un modèle pure-
ment naïf. Quelques bonnes pratiques se dégagent :