id: H18 title: Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records axis: C kind: sha256 statement: With 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. motivation: C4 (can automated searches reproduce known reduced-round results?). assumptions: Generic encoding, no differential characteristic guidance. expected_contribution: Honest calibration of generic SAT against the state of the art. related_work:
- nikolic2008collisions
- sanadhya2008new
- mendel2011finding
- mendel2013improving
- dobraunig2015analysis
- li2024first
- li2024new
- zhang2026collision
- alamgir2024sha256 possible_counterexamples: SAT reaching ≥ 24 steps unaided (would be notable). verification_strategy: experiments/reduced_round_sha256/collision_sat.py computational_budget: ≈ 3 node-hours status: running classification: pending evidence: [] verdict: pending
H18 — Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records
With 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.