from z3 import *
print("Imports OK : z3-solver (theorie Real)")Imports OK : z3-solver (theorie Real)← 11 - Coloration de graphe | README Z3-Python | 13 - UNSAT cores >> # 12. Arithmetique reelle : raisonner sur les irrationnels exacts Jusqu’ici nous avons raisonne sur des entiers (coloration de graphe, cryptarithmes, ordonnancement). Z3 sait aussi raisonner sur les reels via la théorie Real (SMT-LIB Reals). C’est une capacite profondement différente : les solutions peuvent etre rationnelles exactes (pas d’arrondi flottant), des irrationnels algebriques (racine carree de 2 representee comme racine d’un polynome, pas comme 1.4142…), et l’absence de solution peut etre prouvee (unsat) sur le corps des reels tout entier. Ce notebook explore les trois postures : arithmetique lineaire (solution rationnelle exacte), non-lineaire (irrationnel algebrique), et preuve d’impossibilite sur R. Aucun float, aucun sqrt() approche : tout est symbolique. > Port pyz3 du notebook C# 16_RealArithmetic.ipynb. EPIC #1206, Prong B. (La section B7 Rational du C#, spécifique au DSL Z3.Linq, n’est pas portee.)
Lecture : la théorie se choisit à la déclaration, pas à l’import
Le message d’import nomme la théorie, mais from z3 import * n’en fixe aucune : il ne charge que l’API. C’est la sorte des variables qui décide du fragment logique interrogé. Real('x') place le solveur dans l’arithmétique des réels — un corps réel clos, donc décidable ; Int('x') le mettrait dans l’arithmétique de Presburger ou de Peano selon les opérations employées, avec des propriétés de décidabilité très différentes ; BitVec('x', 32) ouvrirait la théorie des bit-vectors, où l’addition est modulo 2^32.
Cette remarque commande toute la lecture du notebook : les résultats qui suivent ne dépendent pas du solveur mais de la théorie dans laquelle on l’a placé. Un énoncé faux en arithmétique non bornée peut devenir vrai et décidable en arithmétique modulaire — c’est précisément le sujet du notebook 14 consacré aux bit-vectors.
1. La théorie des reels (SMT-LIB Real)
En pyz3, Real('x') créé une variable reelle (théorie des rationnels etant donne que Z3 represente les reels comme des rationnels ou des racines algebriques). Les opérations +, *, comparaisons >= et egalites == s’appliquent. Le solveur decide la satisfiabilite sur cette théorie via des procedure de decision (arithmetique reelle lineaire = simplex ; non-lineaire = méthodes de cylindres algebriques).
2. Arithmetique reelle lineaire : solution rationnelle exacte
Système lineaire x + y = 1, x - y = 3. Solution x = 2, y = -1. Ce sont des rationnels exacts, pas des flottants : Z3 ne fait jamais d’arrondi. Tout le raisonnement est symbolique.
# Systeme lineaire x+y=1, x-y=3 : solution rationnelle EXACTE
x, y = Reals('x y')
s1 = Solver()
s1.add(x + y == 1)
s1.add(x - y == 3)
st1 = s1.check()
print("Systeme x+y=1, x-y=3 : %s" % st1)
if st1 == sat:
m = s1.model()
print(" x = %s" % m[x])
print(" y = %s" % m[y])
print("-> Solution rationnelle EXACTE (pas d'arrondi flottant).")Systeme x+y=1, x-y=3 : sat
x = 2
y = -1
-> Solution rationnelle EXACTE (pas d'arrondi flottant).Lecture : ce que « x = 2 » veut dire exactement
Le modèle rend 2 et -1, pas 2.0 et -1.0. L’écart n’est pas cosmétique : Reals désigne la théorie des corps réels clos, où Z3 représente les valeurs comme des rationnels exacts — numérateur et dénominateur entiers — jamais comme des flottants binaires. Là où une résolution numérique rendrait 2.0000000e+00 avec un résidu d’arrondi, la réponse d’ici est exacte par construction : substituer 2 et -1 dans x + y = 1 et x - y = 3 produit des égalités vraies, pas des égalités à epsilon près.
La conséquence pratique est plus forte qu’il n’y paraît : un check() qui rend sat sur un système linéaire certifie l’existence d’une solution exacte et en fournit une. C’est ce qui rend Z3 utilisable quand les coefficients sont des rationnels non représentables en binaire — précisément le cas où un solveur flottant dérive.
3. Non-lineaire : trouver un irrationnel exact (racine de 2)
Trouvons xs tel que xs^2 = 2, avec xs > 0 (la racine positive). La solution n’est PAS le flottant 1.41421356... : Z3 renvoie une racine algebrique exacte (un root-obj = k-ieme racine d’un polynome a coefficients rationnels), affichée ici en notation decimale avec un ? final qui signale “representation approchee d’un nombre exact”.
# Trouver xs tel que xs^2 = 2, xs > 0 (l'irrationnel sqrt(2))
xs = Real('xs')
s2 = Solver()
s2.add(xs * xs == 2)
s2.add(xs > 0)
st2 = s2.check()
print("xs^2 = 2, xs > 0 : %s" % st2)
if st2 == sat:
m = s2.model()
w = m[xs]
print(" xs = %s" % w)
print(" -> Ce n'est PAS 1.4142... mais une RACINE ALGEBRIQUE exacte.")
print(" (le suffixe '?' = affichage approche d'un root-obj exact ; x^2 - 2 = 0)")xs^2 = 2, xs > 0 : sat
xs = 1.4142135623?
-> Ce n'est PAS 1.4142... mais une RACINE ALGEBRIQUE exacte.
(le suffixe '?' = affichage approche d'un root-obj exact ; x^2 - 2 = 0)Lecture du ? : 1.4142135623? n’est pas un flottant
C’est le point le plus facile à mal lire du notebook. Z3 n’a pas rendu le flottant 1.4142135623730951 : il a rendu un objet-racine (root-obj), et le ? final est la marque de l’affichage. Le modèle porte donc la solution sous forme algébrique symbolique — la racine positive du polynôme minimal x^2 - 2 = 0 — et la forme décimale n’est qu’un rendu approché, produit au moment de l’affichage.
L’écart se mesure : 1.4142135623 ** 2 vaut 1.999999999793256, donc à côté de 2 de plus de 2e-10 ; l’objet-racine, lui, vérifie xs * xs == 2 exactement. C’est toute la différence entre représenter un irrationnel et l’approcher. Le degré du polynôme minimal est l’information qui compte ici — degré 2 pour la racine carrée — et c’est ce qui donne son intérêt à l’exercice 1 : la racine cubique est de degré 3, et la théorie la traite par le même mécanisme, sans changement d’API.
4. Prouver l’absence de racine reelle (UNSAT)
xn^2 + 1 = 0 n’a pas de solution reelle (le discriminant est negatif, les racines sont imaginaires +/-i). Z3 le prouve : unsat. C’est une preuve sur le corps des reels tout entier - il n’existe AUCUN reel satisfaisant cette equation. Aucune approche numérique (essayer des valeurs, echantillonner) ne peut etablir cette absence ; seule la decision algebrique le peut.
# Prouver que xn^2 + 1 = 0 n'a PAS de solution reelle
xn = Real('xn')
s3 = Solver()
s3.add(xn * xn + 1 == 0)
st3 = s3.check()
print("xn^2 + 1 = 0 sur les reels : %s" % st3)
if st3 == unsat:
print(" -> UNSAT : Z3 PROUVE qu'il n'existe pas de racine reelle.")
else:
print(" -> inattendu (devrait etre impossible sur R).")xn^2 + 1 = 0 sur les reels : unsat
-> UNSAT : Z3 PROUVE qu'il n'existe pas de racine reelle.Lecture : unsat est une preuve, pas un échec de recherche
unsat se lit souvent comme « le solveur n’a rien trouvé ». Ici c’est l’inverse : sur la théorie des réels, unsat signifie que la négation de l’énoncé est insatisfiable, donc que l’énoncé est valide pour toutes les valuations. Z3 ne dit pas « je n’ai pas trouvé de xn tel que xn^2 + 1 = 0 » ; il dit qu’un tel xn n’existe pas dans R. La traduction algébrique est immédiate : xn^2 = -1 n’a pas de solution réelle puisque le carré d’un réel est positif ou nul — le discriminant < 0 du trinôme dit exactement la même chose, vue par les coefficients.
Cette bascule sat / unsat est ce qui fait de Z3 un prouveur et non seulement un chercheur de solutions. Elle sert directement à l’exercice 2, où discriminer deux trinômes revient à comparer un sat et un unsat sur la même famille de formules.
5. Application geometrique : l’inegalite triangulaire
Trois longueurs a, b, c forment un triangle ssi chacune est <= la somme des deux autres (a + b >= c, etc.). Pour (3, 4, 5) c’est SAT (triangle rectangle canonique) ; pour (1, 2, 5) c’est UNSAT (1 + 2 = 3 < 5, le plus long cote est trop long). La preuve est exacte, pas une verification numérique.
# Trois longueurs forment-elles un triangle ? (inegalite triangulaire)
a, b, c = Reals('a b c')
def triangle(va, vb, vc):
return And(va + vb >= vc, va + vc >= vb, vb + vc >= va)
# Triangle (3, 4, 5) ?
sA = Solver()
sA.add(triangle(RealVal(3), RealVal(4), RealVal(5)))
print("Triangle(3, 4, 5) : %s" % sA.check())
# Triangle (1, 2, 5) ?
sB = Solver()
sB.add(triangle(RealVal(1), RealVal(2), RealVal(5)))
stB = sB.check()
print("Triangle(1, 2, 5) : %s" % stB)
if stB == unsat:
print(" -> UNSAT : impossible (1 + 2 = 3 < 5, le plus long cote est trop long).")Triangle(3, 4, 5) : sat
Triangle(1, 2, 5) : unsat
-> UNSAT : impossible (1 + 2 = 3 < 5, le plus long cote est trop long).Lecture : le même encodage rend sat puis unsat
Les deux appels partagent exactement la même formule triangle(...) — seule change la valuation. (3, 4, 5) satisfait les trois inégalités ; (1, 2, 5) échoue sur celle qui compte, 1 + 2 = 3 < 5. Le point pédagogique est que le prédicat n’a pas été réécrit pour le second cas : c’est la même conjonction, et c’est le solveur qui découvre laquelle des trois inégalités tombe.
Notez la frontière exacte de cet encodage : avec des inégalités larges, un triplet (1, 2, 3) rendrait sat alors que le triangle est plat — le cas dégénéré est accepté. Exclure les triangles dégénérés demande la forme stricte. C’est le genre d’ajustement où le solveur continue de donner la bonne réponse sans qu’on ait à énumérer les cas limites à la main.
6. Ce que ce notebook a demontre
Trois capacites distinctes de la théorie des reels : 1. Solution rationnelle exacte (linearite) - pas de flottant, pas d’arrondi.
Irrationnel algebrique exact (non-lineaire) - racine de 2 comme
root-obj, pas comme decimal tronque.Preuve d’absence sur R (
unsat) - aucune racine reelle ax^2 + 1 = 0, preuve globale impossible par echantillonnage.
Ces trois postures sont inaccessibles au calcul numérique classique (float, math.sqrt). Elles illustrent pourquoi la théorie SMT des reels est un outil de raisonnement, pas juste de calcul.
7. Exercices
Les trois exercices ci-dessous vous font manipuler la théorie des reels sur des variantes : racine cubique (1), discriminant d’un trinome (2), optimisation sur les reels (3). Chaque stub est self-contained : les fonctions (Real, Reals, Solver) sont définies dans les sections précédentes.
Exercice 1 - Racine cubique de 2
Trouvez c tel que c^3 = 2, avec c > 0. La racine cubique de 2 est aussi un irrationnel algebrique, mais de degré 3 (vs degré 2 pour la racine carree). Affichez le temoin et comparez la notation.
Étapes : c = Real('c'), ajouter c * c * c == 2 et c > 0, checker, afficher le modèle.
# Exercice 1 : trouver c tel que c^3 = 2 (racine cubique de 2)
# TODO etudiant :
# Etape 1 : c = Real('c')
# Etape 2 : solver.add(c * c * c == 2, c > 0)
# Etape 3 : solver.check() + afficher le root-obj (degre 3 vs degre 2 pour sqrt(2))
result = None # TODO etudiant
print("Exercice 1 a completer : trouvez la racine cubique exacte de 2")Exercice 1 a completer : trouvez la racine cubique exacte de 2Exercice 2 - Discriminant et nombre de racines
Un trinome q^2 + bq + c = 0 a des racines reelles ssi son discriminant D = b^2 - 4c >= 0. - (a) Prouvez que q^2 - 3q + 2 = 0 a une racine reelle (sat ; deux racines : 1 et 2). - (b) Prouvez que q^2 + q + 1 = 0 n’en a aucune (unsat ; D = -3 < 0).
Étapes : pour chaque polynome, encoder = 0 et checker. Le verdict sat/unsat confirme le signe du discriminant.
# Exercice 2 : discriminant et racines reelles
# TODO etudiant :
# (a) q^2 - 3q + 2 = 0 a une racine reelle (SAT, deux racines 1 et 2)
# (b) q^2 + q + 1 = 0 n'en a aucune (UNSAT, D = -3 < 0)
# Etape 1 : encoder chaque polynome = 0
# Etape 2 : solver.check() -> SAT puis UNSAT
result = None # TODO etudiant
print("Exercice 2 a completer : discriminez les trinomes (SAT vs UNSAT)")Exercice 2 a completer : discriminez les trinomes (SAT vs UNSAT)Exercice 3 - Distance minimale (optimisation sur les reels)
Minimisez px^2 + py^2 sous la contrainte px + py = 4 (point de la droite le plus proche de l’origine). La solution exacte est px = py = 2, distance minimale sqrt(8).
Indice : utilisez Optimize() avec .minimize(px*px + py*py). Note : l’optimisation non-lineaire sur les reels est delicate (Z3 peut renvoyer un point sous-optimal) ; si le minimum trouve n’est pas 8, reflechissez a pourquoi (la théorie non-lineaire reelle est decidable mais l’optimisation globale reste dure).
# Exercice 3 : minimiser px^2 + py^2 sous px + py = 4 (point le plus proche de l'origine)
# TODO etudiant :
# Etape 1 : px, py = Reals('px py')
# Etape 2 : opt = Optimize(); opt.add(px + py == 4)
# Etape 3 : opt.minimize(px * px + py * py)
# Etape 4 : opt.check() -> minimum attendu = 8 en px = py = 2 (distance sqrt(8))
result = None # TODO etudiant
print("Exercice 3 a completer : minimisez x^2 + y^2 sous x + y = 4")Exercice 3 a completer : minimisez x^2 + y^2 sous x + y = 4Conclusion
La théorie des reels de Z3 transforme le solveur en outil de raisonnement algebrique exact. La ou le calcul numérique flottant (float, math.sqrt) introduit des erreurs d’arrondi et ne peut jamais prouver une absence de solution, la théorie SMT Real offre : solutions rationnelles exactes, irrationnels algebriques (racine de 2 comme root-obj), et preuves d’impossibilite sur R tout entier (unsat pour x^2 + 1 = 0).
Cette serie Z3-Python (notebooks 01 a 12) couvre maintenant l’eventail complet : entiers (01-06, 10, 11), satisfaction de contraintes (08 ordonnancement, 09 CSP logique, 11 graphes), tactiques (03), et ici l’arithmetique reelle exacte (12). Le pont avec la serie souer Z3.Linq (C#) se fait via les mêmes exemples portes entre Microsoft.Z3 et pyz3.