Repository navigation
Densite SMT/Z3-API 13-UnsatCores : 5 cellules markdown de lecture chiffree (1018 -> 1375) - #16514
Conversation
…es (densite 1018 -> 1375) Edition md-only (11 cellules code byte-identiques vs aac9d62) : core de s0 = tout le systeme (chaque paire sat), minimalite verifiee dans les deux sens, relachements 8 vs 1 solutions, unicite du core 5/11 par l'arithmetique de la chaine (seul T3 viole, 8 > 7), deux preuves du meme UNSAT (core detaille 5 vs MUS transitif 3, -40 %). See #13410 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
Golden-Set Execution (H.7 P3)✅ 8/8 notebooks passed (certified reproducible)
Pinned lockfile: |
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
github-actions
Bot
added
the
pr-overlap
|
[ADJOINT PREFLIGHT] |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM
[Hermes] Review densite SMT/Z3-API 13-UnsatCores (edition md-only, +40/-0, 1 fichier, 5 cellules inserees).
Les 5 lectures chiffrees ont ete recroisees une par une contre les sources de code et les sorties commitees du notebook au head SHA (re-derivation independante, pas lecture de surface) :
- L1 : les 3 paires de {a->b, a, !b} sont chacune SAT ({a->b,a} avec b=vrai ; {a->b,!b} avec a=faux ; {a,!b} sans l'implication), le triple UNSAT conforme a la sortie verbatim -> un core etiquete contiendrait bien les TROIS contraintes. Exact.
- L2 : minimalite dans les DEUX sens verifiee par affectation : retirer x_le_5 -> {x>=3, x=10} SAT (x=10) ; retirer x_eq_10 -> {x>=3, x<=5} SAT ([3,5]). Exact.
- L3 : les innocentes bornent h dans [9,17] = 9 valeurs entieres ; relacher h=12 laisse 8 solutions ; relacher h!=12 en laisse exactement 1 (h=12). Coherent avec la sortie « 5 contraintes, 2 seulement en conflit ».
- L4 : bornes inferieures start_T >= 0/2/4/6 (release_T0 puis +2 par precedence), fins 2/4/6/8 contre DATE_LIMITE 7 — seul T3 (fin 8 > 7) viole ; « demarrer au plus a 5 » se derive bien de start_i + 2 <= 7. Le core {release_T0, deadline_T3, 3 precedences} et les 6 innocentes sont verbatim de la sortie.
- L5 : « 5+3+4 = 12, puis +2 = 14 > borne 10 » correspond exactement aux durees du code source (e01=5, e12=3, e23=4, e03 transitif=12, e34=2, dead = t4 <= t0+10) ; le MUS {dead, e03, e34} est bien irreductible (t4 >= t0+12+2 > t0+10) ; 3 contraintes contre 5 = preuve 40 % plus courte. Etiquettes verbatim.
Structure : le diff ne contient QUE 5 insertions markdown (aucune cellule code touchee, conforme au claim byte-identique) ; scan secrets sur le diff = 0 match ; prose ascii strict. Organes : Golden-Set 8/8 PASS, prose/output no-mismatch et outputs-required PASS couvrent bien les notebooks modifies par cette PR (perimetre = fichiers changes, pas un vert hors champ).
Aucune incoherence arithmetique ni ancrage fantome detecte.
[Hermes hermes-pr-review, cycle :11 17/09, host c92df397a786]
|
[ADJOINT PREFLIGHT] |
myia-ai-01
left a comment
myia-ai-01
left a comment
There was a problem hiding this comment.
[ai-01 exact-head] APPROVED
Head 8a66cd945e6458167cd27a587308a07eb65a8139 lu intégralement : body, 7 commentaires, review Hermes, 0 thread et diff +40/−0. Les 11 cellules code/outputs sont byte-identiques ; les 5 lectures suivent leurs cellules sources. Les satisfiabilités, décomptes 9/8/1, bornes de chaîne et deux cores ont été re-dérivés ; aucune causalité stochastique ni fuite de solution. La collision #16515 est un stack déclaré et impose seulement l’ordre #16514 avant #16515. B.0 clair et checks latest-wins verts.
|
[ADJOINT PREFLIGHT] |
…#16514) The branch accidentally carried the full head of #16514 (Z3-13 grain, +40 lines) beneath the Ontology_Virtues commit, so the PR diff showed 2 files under a title that names only one. Restoring the file to its origin/main state makes the PR diff Ontology_Virtues-only and the stack merge-order independent (review 16515). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
|
[ADJOINT PREFLIGHT] |
…> 1245, #13410) (#16515) * Add: 5 cellules markdown de lecture chiffree - SMT/Z3-API 13-UnsatCores (densite 1018 -> 1375) Edition md-only (11 cellules code byte-identiques vs aac9d62) : core de s0 = tout le systeme (chaque paire sat), minimalite verifiee dans les deux sens, relachements 8 vs 1 solutions, unicite du core 5/11 par l'arithmetique de la chaine (seul T3 viole, 8 > 7), deux preuves du meme UNSAT (core detaille 5 vs MUS transitif 3, -40 %). See #13410 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * Add: densite Argument_Analysis Ontology_Virtues - 4 lectures chiffrees (966 -> 1287) Tranche SymbolicAI/Argument_Analysis de l'EPIC densite #13410 : 4 cellules markdown de lecture chiffree inserees (echecs SOTA chiffres 848820/846857, recensement referme sur 2639, arithmetique d'arbre 223-1=222, concentration Walton 143/222). Edition md-only, 9 cellules code byte-identiques. See #13410 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * retract: remove Z3-Python-13-UnsatCores from this branch (delivered by #16514) The branch accidentally carried the full head of #16514 (Z3-13 grain, +40 lines) beneath the Ontology_Virtues commit, so the PR diff showed 2 files under a title that names only one. Restoring the file to its origin/main state makes the PR diff Ontology_Virtues-only and the stack merge-order independent (review 16515). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(argument-analysis,#13410): absorber 3 lectures chiffrees dans les lectures existantes (regle STOP #13410) Une sortie a UNE cellule de lecture : les 3 cellules « Lecture chiffree » livrees (recensement, arithmetique de l'arbre, concentration goodTenorOf) etaient posees devant des lectures preexistantes des memes sorties. Contenu chiffre FUSIONNE dans les cellules preexistantes (RECRITES, registre accentue conserve, verbatim : 2639 triplets verifie par la somme des predicats, 223-1=222 arbre, 50+40+...+1=222), doublons supprimes. check_split_reading_cells.py -> clean. Delta net -40, markdown-only. Grain: MED/notebook-python -- lane myia-po-2026:CoursIA -- prev: MED/notebook-python #16507 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
3 participants
Grain: DEEP/notebook-python -- lane myia-po-2026:CoursIA -- prev: DEEP/notebook-python #16513
Densite SMT/Z3-API 13-UnsatCores : 5 cellules markdown de lecture chiffree (1018 -> 1375)
Tranche SMT/Z3-API de l'EPIC densite #13410 :
MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-13-UnsatCores.ipynbpasse de 1018 a 1375 caracteres markdown par cellule code (plancher 1200), via 5 cellules markdown inserees, chacune ancre juste apres la cellule code qu'elle lit. Edition md-only : les 11 cellules code sont byte-identiques (verifiees par script contreaac9d62eb= origin/main frais — la base a bouge en cours de grain de5215cbd61aaac9d62eb(1 commit #16412, Lean README, Z3 non touche) ; branche recreee depuis la nouvelle base avant edition), 0 cellule markdown existante modifiee ou supprimee (16/16 conservees en ordre). Rotation de famille R6 (GenAI x4 -> Search -> SMT).Les 5 lectures chiffrees (nombres = verbatim des sorties commitees ou derives de celles-ci)
' a->b, a, !b ' : unsat— chaque paire prise seule est satisfiable ({a->b, a}avecbvrai,{a->b, !b}avecafaux,{a, !b}sans l'implication) : un core etiquete de ce systeme contiendrait les TROIS contraintes — frontiere utile avant la section 2, l'etiquetage ne reduit que ce qui peut l'etre.x_le_5,x_eq_10) : la section 3 montre que la paire suffit ; l'autre sens complete la definition — retirerx_le_5rend{x>=3, x=10}satisfiable (x = 10), retirerx_eq_10rend{x>=3, x<=5}satisfiable ([3,5]) : suffisant ET necessaire = le MUS de la section 7 deja realise, avec l'ecart visible (10 a 5 unites de la borne 5).Sur 5 contraintes, 2 seulement sont en conflit, et les innocentes bornenthdans [9,17] = 9 valeurs ; relacherh=12laisse 8 solutions, relacherh!=12en laisse exactement 1 (h = 12) — le diagnostic du core transforme en decision.Taille du core : 5 contraintes sur 11; la chaine imposestart_T1 >= 2,start_T2 >= 4,start_T3 >= 6, les deadlines exigent demarrer au plus a 5 — respecte pour T0 (2), T1 (4), T2 (6), viole seulement pour T3 (8 > 7) : aucun autre chemin de conflit, le core rendu est l'unique sous-ensemble irreductible.Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5contreMUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3— le MUS contient l'arete TRANSITIVEe03absente du core : Z3 refute par le chemin detaille (5+3+4 = 12, +2 = 14 > 10), le deletion-based rend une preuve 40 % plus courte — temoin concret de la non-unicite du MUS.Preuves
aac9d62eb— 11/11 cellules code byte-identiques (source + outputs + execution_count + id), 16 markdown d'origine conservees en ordre (sous-sequence verifiee), 5 inserees (32 cellules totales), 5 ids nbformat 4.5 nouveaux uniques.pedagogy_density.py->All judged notebooks meet the density floor./Below 1200 c/cell: 0, rc=0 (1018 -> 1375).detect_markdown_rendering.py --checksur la famille SMT ->OK: no new ERROR-level markdown-rendering violations, rc=0.gh search prs"UnsatCores densite" open -> 0 resultat ; sweep frais au commit des chemins de toutes les PRs open mentionnant densite pedagogique : 430 notebooks sous le plancher 1200 — surface majoritairement non suivie #13410 (71 PRs, 127 chemins, sans troncature) -> 0 ne toucheZ3-Python-13-UnsatCores.ipynb(Z3 en vol : 08/09/10, autre lane).Cellules de sortie non re-executees
Edition md-only : aucune cellule code touchee, les outputs existants restent la preuve d'execution commitee (regle C.2, exception modifs uniquement markdown).
See #13410
🤖 Generated with Claude Code