Navigation : << Z3-Python-01 Introduction | Index | Z3-Python-02 Sudoku >> | Z3 C# (Z3.Linq) ->
Compagnon de style déclaratif du module Z3-Python-01 — Introduction : approfondissement optionnel de la lane Python, extension unilatérale documentée (aucun twin C#).
A la fin de ce notebook, vous saurez : 1. Reconaitre le style declaratif de specification de contraintes (idiome LINQ Where / from ... where ... select) utilise par la serie soueur C# Z3.Linq 2. Traduire cet idiome declaratif en appels imperatifs a l’API z3-py (Solver(), s.add(...), s.check(), s.model()) 3. Diagnostiquer l’insatisfiabilite (unsat) et extraire un noyau d’insatisfiabilite (unsat core) pour identifier les contraintes en conflit 4. Modeliser un problème combinatoire non-trivial (coloration de graphe) ou la puissance declarative du solveur surpasse l’ecriture manuelle d’un backtracking
Cette serie (Z3-Python) utilise z3-py, le binding Python direct, en style imperatif-symbolique : on créé un Solver, on ajoute des contraintes, on appelle check. La serie soeur Z3 C# (Z3.Linq) expose une couche declarative : les contraintes s’ecrivent comme des predicats LINQ, traduits automatiquement en formules SMT.
Ce notebook fait le pont : il montre que les deux styles expriment la même intention declarative (decrire le QUOI, pas le COMMENT), et comment retrouver en Python la lisibilite du DSL C# sans perdre l’acces a l’API complete.
La serie C# Z3.Linq permet d’ecrire un theoreme comme une requête LINQ. Voici un exemple representatif (cellule de reference, executee dans le notebook C# 01_Linq2Z3_Intro.ipynb) :
Ce qui compte pedagogiquement : chaque clause where est une contrainte. L’ordre n’importe pas, la facon dont le solveur resout n’apparait pas. C’est l’essence du declaratif : on decrit les relations que doivent satisfaire les inconnues, pas l’algorithme de recherche.
En Python, z3-py n’a pas de sucre syntaxique equivalent au compilateur d’arbres d’expressions LINQ. On exprime donc les mêmes contraintes par des appels explicites a s.add(...). C’est legerement plus verbeux mais tout aussi declaratif sur le fond — et on garde l’acces a l’API complete (tactiques, Optimize, théories avancees).
Reproduisons en Python le theoreme ci-dessus (5 entiers X1..X5, 4 contraintes). Le patron d’usage z3-py :
Solver()Int)s.add(...)s.check(), puis s.model() pour extraire un modèle# Exemple 1 : theoreme a 5 entiers, 4 contraintes (port direct du theoreme LINQ ci-dessus)
s = Solver()
X1, X2, X3, X4, X5 = Ints('X1 X2 X3 X4 X5')
# Chaque clause 'where' du C# devient un s.add(...) en Python
s.add(X1 - X2 >= 1) # where t.X1 - t.X2 >= 1
s.add(X1 - X2 <= 3) # where t.X1 - t.X2 <= 3
s.add(X1 == 2 * X3 + X5) # where t.X1 == (2 * t.X3) + t.X5
s.add(X3 == X5) # where t.X3 == t.X5
resultat = s.check()
print("Resultat du solveur :", resultat)
if resultat == sat:
m = s.model()
print("Modele trouve :")
for v in [X1, X2, X3, X4, X5]:
val = m[v]
print(" %s = %s" % (v, val if val is not None else "(libre, non assignee par le solveur)"))
# X4 est libre (aucune contrainte) : le solveur ne l'assigne pas dans le modele
print("\nNote : X4 n'apparait dans aucune contrainte -> le modele le laisse non assigne (None).")Resultat du solveur : sat
Modele trouve :
X1 = 3
X2 = 2
X3 = 1
X4 = (libre, non assignee par le solveur)
X5 = 1
Note : X4 n'apparait dans aucune contrainte -> le modele le laisse non assigne (None).| C# Z3.Linq (declaratif) | Python z3-py (imperatif-symbolique) |
|---|---|
ctx.NewTheorem<Symbols<...>>() |
X1, X2, ... = Ints('X1 X2 ...') |
where t.X1 - t.X2 >= 1 |
s.add(X1 - X2 >= 1) |
theorem.Solve() |
s.check() + s.model() |
solution.X1 |
m[X1] |
Le contenu logique est identique : les deux formulations declarent les mêmes 4 contraintes. La différence est purement syntaxique — le compilateur C# traduit l’arbre d’expression LINQ, tandis qu’en Python on ecrit les appels s.add explicitement. En contrepartie, z3-py nous donne acces aux tactiques, a Optimize, et aux théories de bas niveau que la couche LINQ n’expose pas.
Cas d’école : une variable doit etre a la fois > 5 et < 3 — c’est impossible. Le solveur repond unsat. Le noyau d’insatisfiabilite (unsat_core) identifie quelles contraintes, parmi un ensemble etiquete, sont responsables du conflit : c’est un outil de diagnostic indispensable sur de gros modèles.
Pour obtenir un noyau, on etiquete chaque contrainte avec un Bool et on utilise assert_and_track au lieu de add.
# Exemple 2 : systeme UNSAT + extraction du noyau d'insatisfiabilite
s2 = Solver()
x = Int('x')
p1, p2 = Bools('p1 p2') # etiquettes logiques des deux contraintes
# assert_and_track(constraint, label) : la contrainte est ajoutee sous une etiquette
s2.assert_and_track(x > 5, p1) # 'where t.X1 > 5'
s2.assert_and_track(x < 3, p2) # 'where t.X1 < 3'
resultat = s2.check()
print("Contraintes : x > 5 ET x < 3")
print("Resultat du solveur :", resultat)
if resultat == unsat:
noyau = s2.unsat_core()
print("Noyau d'insatisfiabilite :", noyau)
print("-> Les contraintes etiquetees", [str(b) for b in noyau],
"sont conjointement incompatibles.")Contraintes : x > 5 ET x < 3
Resultat du solveur : unsat
Noyau d'insatisfiabilite : [p2, p1]
-> Les contraintes etiquetees ['p2', 'p1'] sont conjointement incompatibles.| Reponse | Sens | Utilite du noyau |
|---|---|---|
sat |
Au moins une assignation satisfait tout | s.model() donne un exemple |
unsat |
Aucune assignation possible | unsat_core() localise les contraintes fautives |
unknown |
Le solveur n’a pas tranche (trop dur / timeout) | Pas de noyau ; affiner le modèle ou augmenter le budget |
Le noyau d’insatisfiabilite est l’equivalent logique d’un message d’erreur précis : au lieu de dire « votre modèle est impossible », il pointe les contraintes (parfois 2 ou 3 parmi des centaines) qui se contredisent. Sur un problème industriel (planning, verification), c’est ce qui rend le debuggage envisageable.
Pour montrer ou le paradigme declaratif prend tout son sens, modelisons un vrai problème combinatoire : la coloration de carte (combien de couleurs suffisent pour que deux regions frontieres aient des couleurs différentes ?). C’est le coeur du theoreme des 4 couleurs.
Nous colorions la carte de l’Australie (6 etats continentaux contigus) avec 3 couleurs. Construire un backtracking manuel pour ce problème est fastidieux (gestion des conflits, ordre d’affectation, retour-arriere). En z3-py, on se contente de declarer l’adjacence et le solveur trouve une coloration valide.
Adjacences (frontieres terrestres) : - Australie-Occidentale (WA) : NT, SA - Territoire du Nord (NT) : WA, SA, Q - Australie-Meridionale (SA) : WA, NT, Q, NSW, V - Queensland (Q) : NT, SA, NSW - Nouvelle-Galles du Sud (NSW) : SA, Q, V - Victoria (V) : SA, NSW
(Tasmanie est insulaire, hors du graphe continental.)
# Exemple 3 : coloration de la carte d'Australie avec 3 couleurs
couleurs = ['rouge', 'vert', 'bleu'] # 3 couleurs
etats = ['WA', 'NT', 'SA', 'Q', 'NSW', 'V']
# Une variable Int par etat, domanee a {0,1,2} (indices de couleurs)
c = {e: Int(e) for e in etats}
s3 = Solver()
for e in etats:
s3.add(c[e] >= 0, c[e] <= 2) # domaine : 3 couleurs
# Adjacences : deux etats frontaliers ont des couleurs differentes
adjacences = [('WA','NT'), ('WA','SA'), ('NT','SA'), ('NT','Q'),
('SA','Q'), ('SA','NSW'), ('SA','V'), ('Q','NSW'), ('NSW','V')]
for a, b in adjacences:
s3.add(c[a] != c[b]) # contrainte 'deux voisins differents'
resultat = s3.check()
print("Coloration 3-couleurs de l'Australie :", resultat)
if resultat == sat:
m = s3.model()
print("\nColoration valide :")
for e in etats:
idx = m[c[e]].as_long()
print(" %-4s -> %s" % (e, couleurs[idx]))
# Verification automatique : aucune paire adjacente n'a la meme couleur
conflits = [(a, b) for a, b in adjacences if m[c[a]].as_long() == m[c[b]].as_long()]
print("\nVerification : %d conflit(s) adjacent(s) -> %s" % (len(conflits), 'OK' if not conflits else 'BUG'))Coloration 3-couleurs de l'Australie : sat
Coloration valide :
WA -> bleu
NT -> vert
SA -> rouge
Q -> bleu
NSW -> vert
V -> bleu
Verification : 0 conflit(s) adjacent(s) -> OKEssayez d’imaginer le code imperatif equivalent : il faudrait choisir un ordre d’affectation des 6 etats, implementer un backtracking avec detection de conflit, gerer l’expiration des branches mortes, et esperer que l’heuristique d’ordre soit bonne. Pour 6 etats c’est faisable ; pour 60 (carte d’un grand pays avec toutes ses subdivisions), c’est un enfer de maintenance.
Avec z3-py, le même patron (declarer le domaine + declarer l’adjacence + check) resout n’importe quelle taille d’instance. Ajouter un etat = ajouter une variable et quelques contraintes d’adjacence ; l’algorithme de resolution, lui, ne change jamais. C’est le gain fondamental du paradigme declaratif : la complexite algorithmique est deleguee au solveur, le modèle exprime seulement la structure du problème.
Lecon : le seuil ou le declaratif surpasse l’imperatif n’est pas le nombre de variables, mais la richesse des contraintes. Des qu’apparait une combinaison de contraintes (adjacence + cardinalite + optimisation), ecrire un backtracking correct devient plus difficile que de declarer les contraintes.
Les trois exercices suivent les exemples ci-dessus. Chaque stub est incomplet (marque # TODO etudiant) : a vous d’ecrire les contraintes. Les cellules s’executent sans erreur même non completees (elles affichent un message d’attente).
Soit le theoreme C# (4 entiers) :
Indice : 4 appels s.add(...). N’oubliez pas les declarations Ints(...). Verifiez avec s.check() puis affichez le modèle.
# Exercice 1 : traduire le theoreme LINQ en pyz3 (etudiant)
s_ex1 = Solver()
# X1, X2, X3, X4 = Ints('X1 X2 X3 X4') # TODO etudiant : declarer les variables
# s_ex1.add(...) # TODO etudiant : ajouter les 3 contraintes
# TODO etudiant : verifier (s_ex1.check()) et afficher le modele
print("Exercice 1 a completer : retirez les commentaires TODO et ajoutez vos contraintes.")Exercice 1 a completer : retirez les commentaires TODO et ajoutez vos contraintes.Trois contraintes sur un entier n : 1. n est pair (n % 2 == 0) 2. n > 10 3. n < 8
Indice : ces contraintes sont conjointement insatisfiables. Utilisez assert_and_track avec 3 etiquettes Bool, puis affichez le unsat_core. Lequel des trois le solveur pointe-t-il (en pratique, le noyau minimal peut contenir 2 des 3 etiquettes) ?
Étape 1 : ecrivez la parite n % 2 == 0 en arithmetique entiere Z3 (pensez a n - 2*(n/2) == 0 ou n % 2).
# Exercice 2 : UNSAT + noyau (etudiant)
s_ex2 = Solver()
# n = Int('n') # TODO etudiant
# e1, e2, e3 = Bools('e1 e2 e3') # TODO etudiant : etiquettes
# s_ex2.assert_and_track(n % 2 == 0, e1) # TODO etudiant : parite (ajuster la formule si besoin)
# s_ex2.assert_and_track(..., e2) # TODO etudiant : n > 10
# s_ex2.assert_and_track(..., e3) # TODO etudiant : n < 8
# TODO etudiant : s_ex2.check() + s_ex2.unsat_core()
print("Exercice 2 a completer : retirez les commentaires TODO et ajoutez vos contraintes + extraction du noyau.")Exercice 2 a completer : retirez les commentaires TODO et ajoutez vos contraintes + extraction du noyau.Reprenez le modèle de coloration (section 4) et repondez a la question : la carte d’Australie est-elle 2-coloriable ? (i.e. existe-t-il une coloration valide avec seulement 2 couleurs ?)
Indice : c’est une question de decision. Changez le domaine {0,1,2} en {0,1} et relancez check. Le résultat (sat ou unsat) est la reponse. Si unsat, cela prouve que 2 couleurs ne suffisent pas (il en faut au moins 3).
Étape 1 : copiez la cellule de l’exemple 3, reduisez le domaine, et interpretez le verdict du solveur.
# Exercice 3 : la carte d'Australie est-elle 2-coloriable ? (etudiant)
s_ex3 = Solver()
# c = {e: Int(e) for e in ['WA','NT','SA','Q','NSW','V']} # TODO etudiant
# TODO etudiant : domanee a {0,1} (2 couleurs) au lieu de {0,1,2}
# TODO etudiant : re-ajouter les 9 contraintes d'adjacence (c[a] != c[b])
# TODO etudiant : s_ex3.check() et interpreter sat/unsat
print("Exercice 3 a completer : retirez les commentaires TODO, reduisez le domaine a 2 couleurs et interpretez le verdict.")Exercice 3 a completer : retirez les commentaires TODO, reduisez le domaine a 2 couleurs et interpretez le verdict.| Concept | Cote C# (Z3.Linq) | Cote Python (z3-py) |
|---|---|---|
| Style | Declaratif (LINQ Where/from) |
Imperatif-symbolique (Solver.add) |
| Specification | Arbres d’expressions compiles | Appels s.add explicites |
| Avantage | Lisibilite proche du pseudo-code | Acces complet (tactiques, Optimize, théories) |
| Insatisfiabilite | theorem.Solve() leve / retourne |
check() == unsat + unsat_core() |
Ce qu’il faut retenir : - Les deux styles sont equivalents en expressivite sur les problemes de satisfaction ; le choix est une question de lisibilite vs contrôle. - Le noyau d’insatisfiabilite (unsat_core) est l’outil de debuggage essentiel : il localise les contraintes fautives dans un modèle. - Le paradigme declaratif prend tout son sens sur les problemes combinatoires (coloration, planning, allocation) : on declare la structure, le solveur resout. La taille de l’instance n’affecte que les performances, jamais la structure du code.
Pour aller plus loin : - Z3-Python-06 — Optimisation avancee : Optimize, maximize/minimize, quand la satisfaction devient optimisation sous objectifs. - Z3 C# (Z3.Linq) : la serie soeur declarative, pour comparer les idiomes dans leur contexte natif. - La documentation z3-solver (pyz3) pour l’API complete.