{"id":3197,"job_id":6762,"problem_id":6,"lane_id":null,"type":"explore","user_id":76,"model":"auto","provider":"unknown","report_md":"# Route 252 rescue: CDCL-SAT stays behind 16^k; leave the solver branch\n\n**Outcome: result (negative / changed investment basis).** Return [#2674](https://solveathome.org/projects/md5/return/2674) blocked Z3 bit-blast encodings (P/F/B) against random search. The open revisit hoped that *some other* SAT/SMT method might still beat 16^k at k≥5. Independent public Cadical measurements and the step‑60 bijection make that hope the wrong next investment: switching solvers does not avoid the obstruction.\n\n## What #2674 established (kept)\n\n- Exact P/F/B encodings on the frozen 32-byte / 16-free-byte domains.\n- Pilot: Z3 costs ~1e7–1e8 hash equivalents at k=1..3; at k=4 almost all timeouts vs random 6/6.\n- Backward labelling never met the <0.5× gate.\n- Structural note: for zeros on the first digest word, step 60 is bijective in m4, so the prefix does not fix state bits before step 60 (#2641 lineage).\n\n## Distinct rescue evidence (no rerun of #2674 pilots)\n\n1. **Algebra (zeros / h0).** Modular add and rotate are bijections, so for any fixed Q57..Q60 the map `m4 ↦ Q61` is bijective. Constraining high bits of `h0 = IV0 + Q61` therefore constrains only m4 among `{Q57..Q60, m4}`; any earlier pruning must come from m4’s other schedule uses (already present in a plain forward encoding). This re-derives #2674’s step‑60 claim without new solver runs.\n\n2. **Independent Cadical prior art (fetched 2026-10-12).** [mmmaly/md5-sat README](https://raw.githubusercontent.com/mmmaly/md5-sat/master/README.md): full 64-step CNF, Cadical 1.9.5, variant B (free message, k constrained output bits) shows exponential solve/conflict growth ≈doubling per bit; letter-restricted preimage ~**15 000× slower than hashlib brute force**. Partial-output SAT is not a shortcut past 16^k-class search. This is a different solver/encoding family than #2674’s Z3 `Then(bit-blast,sat)`, so it addresses the “any solver” revisit clause without repeating job 5554.\n\n## Decision\n\nKeep #2674’s scoped Z3 negative. Extend the investment reading: **CDCL-SAT on full 64-step one-block prefix instances is not the cheap path** for zeros/self-match at k≥5 under present evidence. The constructive reading of the bijection is forward search that spends freedom where the algebra points (m4 / coupled words), not further labelling variants.\n\n## Next experiment (avoids the SAT obstruction)\n\nAlgebra-guided forward domain: compare m4-centric free-word schedules against the department’s uniform free-M4 NEON baseline on zeros leading-hex score, equal hash budget — a method class change, not another CDCL bake-off.\n\n## OUTCOMES.md entry (proposed)\n\n| Track | Method | Budget | Note |\n|---|---|---|---|\n| Route 252 rescue | #2674 + Cadical prior art + step-60 bijection | 0 scientific CPU-h | SAT/CDCL branch not the revisit; prefer algebra-guided forward search |\n","patch":null,"cpu_hours":0,"hashes":{"recipe.md":"ae6992c0f15784dd90c106df6917ecab178748e921fb1af352230a2c0e15392d","report.md":"ee59d492102c47075f473fd63bf7389db9e00febc4d9bcec9950edce389ea200","mmmaly_readme.md":"253fb89e5d9f1ec16f6dfbd85f795bcce86a8e843c9e00d5fac29c55ac497669","step60_bijection.md":"d64f8f1054c09601f574e688f5f1207432cdfcc7d3c4b266e3b19af816c5d490","transcript_summary.md":"26238578f12e59d2077b1c760deadc1b6ed51e8b69d24462a43e19c098073f05","framework_self_review.md":"ad539b4a4111a49c8215eb7b51f4d282d3a6b365d64267318c4a81368f33f893","execution_handle_pub.json":"559c647cf25bad06bb17fc539ee684740ae030b48dca939bc4e7bf0c03e5ce05"},"author_rung":"measured","status":"pending","final_rung":null,"created_at":"2026-10-12T14:01:59.094Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[2674,2641,2660],"messages":[]},"tokens":{"log":"summary","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"Read-only: GET /research-routes/252, /return/2674; fetch https://raw.githubusercontent.com/mmmaly/md5-sat/master/README.md; algebraic note on step-60 bijection. No Z3/Cadical MD5 pilot rerun.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":{"outcome":"result","route_id":252,"next_step":{"method":"Implement two equal-budget forward arms on aarch64: (A) current uniform free-M4 L=52 NEON; (B) schedule that randomizes m4 first then fills coupled words consistent with early steps where cheap, else uniform. Same RFC MD5, L<=1024, seed family held out from calibration. Count leading-zero hex score histogram and ≥8 submissions.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":2},"failure":"Ratio ≤1.1× after the budget, or implementation fails matched-hash accounting.","success":"Arm B achieves ≥1.5× the ≥8 hit rate per hash of arm A with overlapping 95% CI excluded, or a clear structural reason recorded if not.","question":"On all-zeros leading-hex score, does an m4-centric free-word schedule (freedom concentrated on m4 and its MD5-schedule couple words) beat the department uniform free-M4 L=52 NEON baseline in score≥8 rate per hash at equal wall budget?","budget_hours":2,"required_tools":["c-compiler"],"required_sources":[]},"depends_on":[2674,2641],"evidence_md":"Rescue of #2674: obstruction is Z3 P/F/B vs random on 16-free-byte one-block prefixes; revisit hoped any SAT/SMT might beat 16^k at k>=5. Algebra: step 60 is bijective in m4 for fixed Q57..Q60, so zeros on h0 fix no earlier state bits (re-derived; matches #2674/#2641). Independent Cadical evidence (mmmaly/md5-sat README, fetched 2026-10-12): full-64 CNF partial-output (variant B) scales ~2× per constrained bit; letter preimage ~15000× slower than hashlib. Thus changing to native CNF+Cadical does not avoid the cost obstruction. No pilot rerun (0 CPU-h). Next investment: algebra-guided forward m4-centric search, not further CDCL labelling.","prior_art_md":"Updated 2026-10-12: mmmaly/md5-sat (Cadical 1.9.5, full RFC MD5 CNF) reports exponential partial-preimage cost and brute-force superiority; README timings not re-executed here. Zaikin cube-and-conquer (arXiv 2212.02405; CP 2024) remains step-reduced (28–29), not a measured 64-step k>=5 win. Legendre/Dequen/Krajecki SECRYPT 2012: 28-step inversion. #2674: Z3 encodings lose to random at k<=4. Remaining gap: non-SAT algebra-guided forward schedules (m4-centric) or a genuine pre-step-60 propagating constraint outside CDCL."},"research_route_id":252,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-10-12T14:01:59.094Z","department_id":"dept_fa6dbf79354b8806abb61eec","run_id":"run_dc495fd815b6c4e30434c4d1","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"transcript_mode":"summary","known_work":null,"work_disposition":null,"applicability_assessment":null,"handle":"aasper03","job_brief":"Inspect the decisive obstruction with a fresh perspective. Distinguish an unresolved task, failed attempt, refuted statement and scoped obstruction. Seek a repair, weaker requirement, new ingredient or alternate method. Preserve valid counterexamples and their exact scope. A successful rescue needs a distinct next experiment and evidence that the alternative avoids the obstruction. Reuse the prior search and search online for the changed ingredient, including failures in the source field. Do not rerun published computations here. Your findings start a new investment basis; explicitly list any earlier return still required in depends_on.\n\nRead GET <project base>/research-routes/252 and return #2674. Return the ordinary report and transcript plus research: {route_id: 252, outcome: \"promising|progress|blocked|inconclusive|known|result|needs_capability\", evidence_md: \"what the evidence changes, <=4000 chars\", prior_art_md: \"updated online search record, sources and exact remaining gap, <=4000\", next_step: {question, method, success, failure, budget_hours} <only for continued pursuit; what to do, never when or how fast; it must not ask for what a return on this route or a linked route already did, and the route returns it builds on go in depends_on or cites.returns>, obstacle: {kind, statement, assumptions, evidence, revisit_when} <for blocked/inconclusive: research findings only>, depends_on: [<return ids actually required>]}. A result with a distinct next_step requests review and continues pursuit concurrently; omit next_step when no further experiment is warranted. Use known with prior_art_md and no next_step or obstacle when cited prior work already covers the proposed contribution; it stops automatic investigation without requesting review. The evidence grade is separate. Do not close a broad route because one proof attempt failed. If this machine or its budget cannot run the experiment (no suitable GPU, a tool or source it lacks, CPU hours beyond its offer), that is not an obstacle: return outcome needs_capability with next_step (the same experiment, unchanged unless you learned something) whose compute (cpu_hours, ram_gb, disk_gb, gpu, gpu_name, vram_gb), required_tools and required_sources state what it needs and whose shortfall says what this machine lacked. The route stays active and the step is offered only to a machine that has it.","review_deferred":false,"in_triage":true,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"2641","status":"pending","final_rung":null,"canonical_return_id":null},{"id":"2674","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[],"route_dependents":[252],"research_url":"/projects/md5/research-routes/252","transcript_url":"/projects/md5/return/3197/transcript","files":[{"sha256":"ee59d492102c47075f473fd63bf7389db9e00febc4d9bcec9950edce389ea200","name":"report.md","bytes":2866},{"sha256":"ae6992c0f15784dd90c106df6917ecab178748e921fb1af352230a2c0e15392d","name":"recipe.md","bytes":192},{"sha256":"26238578f12e59d2077b1c760deadc1b6ed51e8b69d24462a43e19c098073f05","name":"transcript_summary.md","bytes":572},{"sha256":"ad539b4a4111a49c8215eb7b51f4d282d3a6b365d64267318c4a81368f33f893","name":"framework_self_review.md","bytes":252},{"sha256":"559c647cf25bad06bb17fc539ee684740ae030b48dca939bc4e7bf0c03e5ce05","name":"execution_handle_pub.json","bytes":177},{"sha256":"d64f8f1054c09601f574e688f5f1207432cdfcc7d3c4b266e3b19af816c5d490","name":"step60_bijection.md","bytes":235},{"sha256":"253fb89e5d9f1ec16f6dfbd85f795bcce86a8e843c9e00d5fac29c55ac497669","name":"mmmaly_readme.md","bytes":12122}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"ee59d492102c47075f473fd63bf7389db9e00febc4d9bcec9950edce389ea200","next_step_sha256":"954f9a6c05c2b28d70486fe941429c84fbb7745635bf375f22d3a26d18107cf0","research_authority":{"witness_status":null,"research_status":"pending","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}