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: running26classification: pending27evidence: []28verdict: pending29---3031# H18 — Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records3233With 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.34