Laurent Petitprez

Les conseils de Wouf

Beaucoup d’élèves entrant au lycée ont en effet des difficultés à manipuler les fractions, les racines carrées, les puissances, à factoriser des expressions… Ces notions, apprises au collège, sont mal assimilées, et le programme des classes de lycée ne prévoit pas de les retravailler en profondeur.

Cet ouvrage propose une remédiation pas à pas. Un code simple et mnémotechnique est associé à chacune des règles et rappelé dans toutes les corrections d’exercices. Il permet de se repérer et de comprendre ses erreurs.

Le premier homme qui est mort a du être drôlement surpris.

George Wolinski (sur mon T shirt!)

Voir toutes les citations.

---

 

NEWS

• Page : https://site2wouf.fr/algorithme2019-2020_s2.php
• Catégorie : Informatique

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 plusieurs 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’encodage 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 simp...
   lien vers l'article sur wouf blog

 

TIPS

Perdu l'annuaire?

www.118218.fr est accessible sur le site de Wouf, par l'intermédiaire du menu "Liens" en cliquant sur "Annuaire"

Voir tous les conseils.

Dernière mise à jour:

Juillet-aôut 2023

Nouvelle Page !

• Exercices du jour : Les 16 immeubles !

Pages modifiées (ou corrigées) !

• Exercices du jour : L'enclos
• Exercices du jour : Les carrelages de couleur /a>

Voir toutes les mises à jour.

 

Trois liens disponibles !

Votre propre message ici, c'est possible! Plus d'informations

---

Sauf mention contraire, le site est placé sous double licence Creative Commons et GNU Free Documentation License, par contre les grandes images décoratives appartiennent à Corbis et sont licenciées par microsoft

Contact: w0uf@free.fr (avec un zéro à la place du O)