1---2id: H183title: Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records4axis: C5kind: sha2566statement: With a 600 s budget, CaDiCaL finds collisions (standard IV) for s ≤ s_c steps and semi-free-start collisions for7 s ≤ s_sfs, while the literature records are 31 steps (practical collision, Li et al. ASIACRYPT 2024; 37-step theoretical,8 2026) and 39 steps (semi-free-start); automated generic search reproduces the easy regime only.9motivation: C4 (can automated searches reproduce known reduced-round results?).10assumptions: Generic encoding, no differential characteristic guidance.11expected_contribution: Honest calibration of generic SAT against the state of the art.12related_work:13- nikolic2008collisions14- sanadhya2008new15- mendel2011finding16- mendel2013improving17- dobraunig2015analysis18- li2024first19- li2024new20- zhang2026collision21- alamgir2024sha25622possible_counterexamples: SAT reaching ≥ 24 steps unaided (would be notable).23verification_strategy: experiments/reduced_round_sha256/collision_sat.py24computational_budget: ≈ 3 node-hours25status: evaluated26classification: known_reproduced27evidence:28- results/reduced_round_sha256/summary.json29- results/reduced_round_sha256/collision_sat.json30verdict: '264 cells, 119 collisions verified. r = 4, 6, 8: UNSAT in all variants/solvers/seeds (72 runs) — no collision within31 the words an 8-step compression reads. r = 10–16: 0-conflict collisions differing in exactly 9 consecutive words (a terminal32 local collision). r = 18: 53 s standard IV, 7–10 s semi-free-start. r ≥ 20: all timeouts. Largest 18 steps vs 28 (pure SAT,33 Alamgir et al. 2024), 31 (Li et al. 2024), 39 SFS.'34---3536# H18 — Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records3738With a 600 s budget, CaDiCaL finds collisions (standard IV) for s ≤ s_c steps and semi-free-start collisions for s ≤ s_sfs, while the literature records are 31 steps (practical collision, Li et al. ASIACRYPT 2024; 37-step theoretical, 2026) and 39 steps (semi-free-start); automated generic search reproduces the easy regime only.39