Fix(Z3,PythonNet): Sudoku-12, Search-10 et SocialChoice-04 sous Linux et macOS (hors flotte)

[jsboige]

Hors flotte : PR de la session cloud d'agnosticisme du mainteneur (branche claude/*, exemption #17713, rôle décrit dans docs/reference/agent-cloud-agnosticisme.md). Pas de tag Grain:, pas de lane. See #17654, sous l'EPIC de parité Linux #10643. Suite de #18774 (ponts PythonNet de GameTheory) et de #18955 (Z3NativeLoader.cs de Z3-API), toutes deux mergées.

Summary

• Trois notebooks C# hors de la série Z3-API chargent Microsoft.Z3 depuis NuGet : Sudoku-12, Search-10 et SocialChoice-04. Ce paquet ne contient la bibliothèque native de Z3 que pour Windows x64 et macOS Intel.
• Search-10 et SocialChoice-04 ont aussi un pont PythonNet vers le moteur de leur jumeau Python (automata-lib, PySAT), qui ne cherche CPython qu'à des chemins Windows.
• Mesuré sur un clone vierge Linux, versions de main, PYTHONNET_PYDLL non définie. Le second arrêt est mesuré en contournant le premier par l'environnement (LD_LIBRARY_PATH vers une libz3, ou PYTHONNET_PYDLL + PYTHONPATH) :

Notebook	Premier arrêt	Second arrêt
Sudoku-12	DllNotFoundException: Unable to load shared library 'libz3' au premier solveur	—
Search-10	FileNotFoundException: Aucun CPython avec automata-lib trouvé (pont, tranche 3)	DllNotFoundException ... 'libz3' (§4)
SocialChoice-04	DllNotFoundException ... 'libz3' (§7)	DllNotFoundException: Could not load C:\Users\…\Python313\python313.dll (pont PySAT, §8)

• Après correction, les trois s'exécutent de bout en bout sous Linux. Les résultats calculés sont ceux de la base : modèles, verdicts SAT/UNSAT, optimum du carré latin (192), vecteurs de tests d'automata-lib, verdicts PySAT. Seules les durées changent (voir le diagnostic).

Changes

• Z3 : la cellule qui restaure Microsoft.Z3 charge Z3NativeLoader.cs de la série Z3-API par un #load à chemin relatif explicite, puis appelle Z3NativeLoader.Register(typeof(Context).Assembly) avant le premier appel à Z3.
  • Sudoku-12, cellule 1 ; Search-10, cellule 20 ; SocialChoice-04, cellule 27.
  • C'est la forme de SvgChartHelper.cs (Probas/Infer/), que GameTheory et ML chargent déjà depuis une autre série.
  • Sous Windows et macOS Intel, Register ne fait rien ; ailleurs, il charge la libz3 désignée par Z3_LIBRARY_PATH, sinon celle du paquet Python z3-solver, sinon celle du système (voir l'en-tête du fichier).
• Ponts PythonNet : même repli que Fix(GameTheory): ponts PythonNet de GT-06, GT-07, GT-13 et GT-17 sous Linux et macOS (hors flotte) #18774.
  • La recherche existante est conservée telle quelle : PYTHONNET_PYDLL, puis le CPython Windows préconfiguré.
  • Quand elle ne désigne aucun fichier existant, InitPythonFromInterpreter(module) lance le premier interpréteur, python3 puis python, qui importe le module (automata pour Search-10, pysat pour SocialChoice-04), et en reprend la bibliothèque partagée, le préfixe et le sys.path.
  • Search-10 levait une exception quand aucun candidat n'existait : elle est remplacée par ce repli.
• Prose :
  • Sudoku-12, cellule 0 : la section « Configuration de l'environnement », vide jusqu'ici, dit ce que fait la cellule suivante sous Linux et macOS Apple Silicon ;
  • Search-10, cellule 0 (prérequis du pont) et cellule 19 (installation de Microsoft.Z3) ;
  • SocialChoice-04, cellule 26 (Z3, §7) et cellule 36 (recette du pont, §8) ;
  • Sudoku-12, cellule 25 (lecture du banc d'essai) : voir le diagnostic.

Registre de parité jumelle : les trois notebooks appartiennent chacun à une paire. Chacune reçoit une attestation --update --by claude-cloud:hors-flotte, posée après les strips outillés.

Le diff compte 6 fichiers : les 3 notebooks et les 3 attestations.

Diagnostic dérive

Comparaison cellule par cellule entre la base (flotte, Windows) et cette tête (clone vierge Linux), sur le texte des sorties, CRLF normalisés, bandeau JavaScript de .NET Interactive masqué. Exécution sous dotnet-interactive 1.0.712001, le canon depuis le 02/10 (#18766) : language_info.version reste 13.0 dans les trois notebooks.

Notebook	Cellules code	Sorties identiques	Écarts
Sudoku-12	19	16	cellules 0 et 1 : en-têtes NuGet (Installing → Installed Packages) et bandeau JavaScript ; cellule 11 : durées du banc d'essai, et la dernière mise à jour de l'affichage de progression
Search-10	15	12	cellule 0 : bandeau ; cellules 5 et 6 : en-têtes NuGet et version de CPython
SocialChoice-04	15	9	cellule 0 : bandeau ; cellules 8, 9, 10, 12 et 13 : durées, en-têtes NuGet et version de CPython

• (a) env/kernel : emplacement de libz3 et de la bibliothèque CPython, objet de la PR. S'y ajoutent la version de CPython (3.13 sous Windows, 3.11 ici), les en-têtes NuGet et le bandeau de .NET Interactive. Verdict CAUSE_FIXED.
• (e) non déterministe, machine : durées des bancs d'essai (Sudoku-12, cellule 11 ; SocialChoice-04, cellules 8 à 13). Verdict CAUSE_INTRINSIC.
  • Tous les verdicts sont identiques à la base. C'est vrai aussi de la grille d'Arrow par Z3 (SAT à 2 alternatives, UNSAT à 3 et à 4 × 2 électeurs) et de l'abandon mesuré à 4 alternatives × 3 électeurs (budget de 15 s dépassé des deux côtés).
  • La prose de SocialChoice-04 ne cite aucune durée figée ; ses tendances (Z3 croît fortement avec la grille, DPLL bat Z3 sur le cas 3 × 2) tiennent sur la tête.
• (b) prose antérieure à la base : Sudoku-12, cellule 25.
  • La lecture du banc d'essai affirmait que la substitution est la plus rapide en Easy et Medium, que l'entier est 3ᵉ en Easy, et que les vecteurs de bits sont « ~1,5× à 2× » plus rapides dès les grilles faciles. Elle donnait aussi « 3 à 5× » sur Hard.
  • Les sorties de la base la contredisaient déjà. En Easy, l'entier est 2ᵉ (174,1 ms contre 156,9 pour les vecteurs de bits simples). En Medium, le plus rapide est l'encodage par vecteurs de bits simple. Sur Hard, le rapport est de 2,2 à 2,9×. check_stale_claims.py le signale sur la base (cellule 25, « 1,5 »).
  • Sur la tête, l'entier est même le plus rapide en Easy (102,1 ms, contre 148,4 à 179,6 ms pour les vecteurs de bits), et le rapport sur Hard est de 2,3 à 3,0×. Une exécution préparatoire, sous dotnet-interactive 1.0.617701, donnait 120,0 ms et 2,5 à 2,75×.
  • La phrase réécrite ne garde que ce qui tient sur ces trois exécutions : sur les grilles faciles, aucun encodage ne domine et leur ordre change ; sur les grilles difficiles, l'entier est de l'ordre de 2 à 3× plus lent que chaque encodage par vecteurs de bits.
  • Verdict CAUSE_FIXED : la cause, un classement figé dans une prose qui interprète des durées, est retirée.
• Aucune sortie n'a été touchée à la main.

Exécution committée : Z3_LIBRARY_PATH pointant vers la libz3.so du wheel officiel z3-solver==4.12.2.0, la version du package NuGet, celle que la base affiche ; automata-lib 9.2.0 et python-sat dans un environnement virtuel CPython 3.11, PYTHONNET_PYDLL non définie, donc par le repli.

Verdict SOTA : SOTA-OK. Les vrais moteurs (Z3, automata-lib, les solveurs CDCL de PySAT) s'exécutent ; rien n'est substitué. Organe-first :

1. Série propriétaire. Le chargement de libz3 est un organe de la série Z3-API.
2. Invocation de l'organe réel. Les trois notebooks consomment Z3NativeLoader.cs par #load au lieu de le recopier.
3. Export dans la série source. Il n'y a rien à exporter : le fichier est déjà autonome.
4. Témoin négatif. C'est le DllNotFoundException mesuré sur main.
5. Vérification indépendante. Les jumeaux Python, avec leur z3-solver, automata-lib et PySAT natifs, donnent les mêmes verdicts.

La fonction InitPythonFromInterpreter est la copie déjà présente dans GT-06, GT-07, GT-13 et GT-17 (#18774). La proposition d'un fichier partagé, décrite dans #18774, reste à l'arbitrage du mainteneur.

Review Checklist

• 1. Scope : chargement de libz3 et repli des ponts PythonNet hors Windows dans trois notebooks ; prose des prérequis et des recettes ; une lecture de banc d'essai de Sudoku-12 qui citait un classement que les sorties ne portaient pas ; attestations de parité.
• 2. Post-fix validation, relancée après le dernier commit :
  • validate_pr_notebooks.py : PASS ;
  • check_output_failure_text.py : 0 regressed ;
  • check_output_collapse.py et check_source_collapse.py : 0 flagged ;
  • check_kernel_drift.py : 0 regression ;
  • check_papermill_ratchet.py : 0 regression (BLOCK_ADDED sur les trois : la base n'avait pas de bloc papermill) ;
  • check_prose_quantitative_claims.py --diff ... --strict : OK ;
  • scripts/check_docs_links.py --check : 0 nouveau lien cassé ;
  • check_cell_source_parses.py --target-py 3.12 --pr-diff : 0 finding ;
  • detect_bare_cross_dir_load.py --check : 0 sur les trois notebooks (les #load portent un chemin relatif explicite) ;
  • check_twin_parity.py --per-pair --check : INTRO=0 ;
  • check_twin_parity.py --verify-recorded-sha : les trois paires de la PR sont OK. Les MISMATCH listés concernent d'autres paires et sont antérieurs à la PR ;
  • check_stale_claims.py : 0 sur les trois (la base en avait 1 sur Sudoku-12, la phrase réécrite) ;
  • check_factual_mislabel.py : 0 sur Sudoku-12 et Search-10 ; 1 sur SocialChoice-04 (cellule 16, « 216 variables »), identique sur la base ;
  • scripts/check_markdown_claims_output.py : Sudoku-12 passe de 1 finding à CLEAN ; Search-10, 4 des deux côtés, tous des numéros de version (9.2.0, 3.1.0, 4.12.2) ; SocialChoice-04, 7 → 8, tous des numéros de version (3.1.0, 3.13, 4.12.2), le huitième venant de z3-solver==4.12.2.0 dans la phrase ajoutée ;
  • check_split_reading_cells.py : clean ; check_interp_positioning.py : 0 ; strip_machine_paths.py --scan : 0 ;
  • check_machine_dep_timing.py : mêmes résultats sur la base et sur la tête (Sudoku-12 : le budget de 3 s par grille, une constante du banc d'essai).
• 3. Pedagogical coherence : exercices et stubs inchangés. Les cellules de restauration de Microsoft.Z3 gagnent deux lignes ; les ponts gardent leur logique.
• 4. Real execution : notebook_tools.py execute <nb> --kernel .net-csharp sous Linux (dotnet-interactive 1.0.712001, le canon depuis le 02/10, [P0] .NET 11 EPIC #18695 -- aligner le pin dotnet-interactive (po-2026 mesure 1.0.712001 != canon 1.0.617701) #18766) : exec_count 1 à 19, 1 à 15 et 1 à 15, 0 erreur. Puis strip_probe_banner.py --apply et scrub_papermill_paths.py --apply.
• 5. Regression check : sous Windows, la recherche de CPython et ses chemins sont inchangés, et Register retourne sans rien faire ; macOS Intel suit le même chemin pour Z3. Ces cas découlent du code et n'ont pas été exécutés ici : seule la branche Linux l'a été.

Anti-regression

• Pas de Lean/Coq touché.
• Aucun test désactivé.
• Code retiré : seule l'exception de Search-10 (« Aucun CPython avec automata-lib trouvé ») disparaît. Le repli la remplace, et il lève à son tour une exception explicite quand aucun interpréteur n'importe automata.

Notebook-specific

• Aucun raise NotImplementedError / assert False / 1/0 introduit.
• Toutes les cellules code ont execution_count et des sorties cohérentes.
• Seuls les notebooks dont une cellule source a changé sont committés (C.3).

Test plan

Sur un poste Linux ou macOS Apple Silicon, avec .NET 10, dotnet-interactive 1.0.712001, et un environnement Python où pip install z3-solver==4.12.2.0 automata-lib python-sat a été exécuté, python3 désignant son interpréteur :

python scripts/notebook_tools/notebook_tools.py execute MyIA.AI.Notebooks/GameTheory/SocialChoice/04-Computational-Aggregation-SAT-Z3-Csharp.ipynb --kernel .net-csharp

La grille d'Arrow (§7) doit conclure UNSAT à 3 alternatives, et les trois solveurs CDCL du §8 UNSAT (Arrow verifie). Sur main, le notebook s'arrête au §7 sur DllNotFoundException ... 'libz3'. Même essai pour Sudoku-12 et Search-10.

Environnement de mesure : conteneur Linux x64, 4 threads, clone vierge, hors flotte.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VuVMY5fhzd5cQhzHiyvjka

---

Generated by Claude Code

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 3
• Code cells validated: 49
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	15.2s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	14.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.5s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.3s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	25.6s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	17.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.5s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	9.1s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

⚠️ Factual-mislabel review needed: a markdown cell states an entity count or tuple formula that CONTRADICTS the committed stream of the code cell it describes (typically copied from a twin notebook with different data). Advisory, NOT a merge gate — triage against the JSON artifact.

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[jsboige]

Sur la tête ef31a5f69, 94 des 95 checks sont verts (dernière tentative par nom). Le seul rouge est le PR gate, en DWELL : le plancher de 120 min depuis le commit de 14:39:28Z, qui s'écoule à 17:07Z.

Ce n'est pas un défaut de la PR, et il n'y a rien à corriger : un nouveau push remettrait le plancher à zéro. Je ne pousse donc rien.

Une fois le plancher écoulé, je rejouerai la jambe moi-même, comme sur #18955 :

gh run rerun 37130511180 --job 111224509860

---

Generated by Claude Code

[clusterManager-Myia]

VERDICT: LGTM

[Hermes] po-2026 — review CoursIA #19000 @ ef31a5f (+2865/-780, 6 fichiers, P4 >1000 lignes).

Vérifications programmatiques au head :

• 3 notebooks extraits intégralement et lus via vue structurelle : Sudoku-12 (19 cellules code, exec 1->19, 0 erreur), Search-10 (15, 1->15, 0), SocialChoice-04 (15, 1->15, 0). Les claims du body (« exec_count 1 à 19, 1 à 15 et 1 à 15 ») sont exacts au compteur près.
• Organe-first vérifié dans les sources : les 3 notebooks portent #load "../SymbolicAI/SMT/Z3-API/Z3NativeLoader.cs" (chemin relatif explicite, pas de recopie) + Z3NativeLoader.Register(typeof(Context).Assembly) en tête (Sudoku-12 cellule 1, confirmé).
• Ponts PythonNet : repli InitPythonFromInterpreter présent avec sonde python3->python (import du module + sysconfig -> dll/home/path) et exception explicite si aucun interpréteur n'importe le module — conforme #18774.
• Claims quantitatifs croisés avec les outputs committés : optimum du carré latin 192 (Sudoku-12 cell 27) ; Arrow SAT@2 alternatives / UNSAT@3 / UNSAT@4x2 / abandon 4x3 budget 15 s (SC-04 cells 18/34) ; les 3 solveurs CDCL « UNSAT (Arrow verifie) » (cell 37). Tout est présent dans les sorties.
• Lecture du banc d'essai réécrite (Sudoku-12 cell 25) tenue par les sorties : Int le plus rapide en Easy (102,1 ms mesuré), 2,3-3,0x sur Hard (572,8 vs 191,3-250,7), vecteurs de bits sous la seconde sur top95, 3/3 Success partout. La prose ne cite plus le classement figé que la base contredisait déjà — le CAUSE_FIXED du diagnostic est réel, pas cosmétique.
• Aucun chemin machine Windows (C:\Users\...) dans les sources ni les outputs des 3 notebooks (0 fuite).
• P5 re-compté : « Le diff compte 6 fichiers : les 3 notebooks et les 3 attestations » = 6 mesurés, attestations twin au format attendu (by: claude-cloud:hors-flotte, shas python/csharp + content).
• Checks au head : tout vert sauf PR gate = jambe DWELL pure (minuteur 120 min, « rien à corriger dans le code ») — non-bloquant documenté. Security scan du diff : 0.

Réserves mineures (n'invalident pas) :

• Les branches Windows / macOS Apple Silicon « découlent du code » sans exécution ici (assumé dans le body, point 5 de la checklist) — la flotte corroborera au prochain cycle d'exécution Windows.
• InitPythonFromInterpreter dupliqué dans désormais 6 notebooks — renvoi explicite à l'arbitrage #18774 pour le fichier partagé, déjà documenté.

[Hermes hermes-pr-review, cycle :16 03/10, host f6be46d1b7a3, sig=20919085]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19000
head: ef31a5f
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c24ec4873f1f41331c02f7f981a0a9349d05ecfc2c170103ee2087dfff181c52
diff-files: 6
diff-additions: 2865
diff-deletions: 780
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

note: Dossier c415 sur PR #19000 (Fix(Z3,PythonNet): Sudoku-12, Search-10 et SocialChoice-04 sous Linux et macOS (hors flotte)). Tierce attestation depuis myia-po-2026:CoursIA-3 (PR porteuse cloud-mainteneur, exemption #17713). DEEP/notebook-csharp, 6 fichiers (3 .ipynb C# + 3 .yaml twin_pairs.d/), +2865/-780 = +2085 net. PR gate SUCCESS strict (commits/ef31a5f69a/check-runs, conclusion=success @17:11:17Z). Hermes APPROVED LGTM @16:30:16Z (review CoursIA-3 par po-2026, 6 fichiers, P4 >1000 lignes, verifications programmatiques au head : 3 notebooks extraits integralement et lus, validation des chemins de libz3/CPython par LD_LIBRARY_PATH et PYTHONNET_PYDLL). 94/95 checks verts (dernier rouge etait DWELL leve par supersession). B.0 OK (rc=0, 0 nit non leve, 1 commentaire non evalue = [INFO] jsboige 14:58:10Z sur DWELL plancher 120 min -- non bloquant, releve depuis). scope: pass (6 fichiers sous MyIA.AI.Notebooks/ et scripts/notebook_tools/twin_pairs.d/, PAS sous .claude/, .github/, ni CLAUDE.md). domain: pass (substance : fix parite Linux/macOS via libz3/CPython pour 3 notebooks C# chargeant Microsoft.Z3 NuGet et 2 ponts PythonNet, conformite EPIC parite Linux #10643, suite #18774 et #18955 deja mergees). Cible READY : substance fix parite Linux/macOS attestee par cloud-mainteneur + Hermes LGTM, pas de nit non leve, PR gate SUCCESS strict. Note composite §A : +2865/-780 depasse seuil 3000 lignes en volume brut, MAIS Hermes LGTM motivé couvre la nature single-feature du fix (3 notebooks + 3 YAML config = 1 feature parite Linux/macOS, pas 4+ features distinctes). Tell c384 (c384, 06:37Z) accepte les PRs hors flotte exemption #17713. Eligible auto-merge LIGHT/DEEP ai-01 (DEEP normalement refuse par merge_ready auto, mais c'est cloud-mainteneur).