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: evaluated classification: known_reproduced evidence:
- results/reduced_round_sha256/summary.json
- results/reduced_round_sha256/collision_sat.json verdict: '264 cells, 119 collisions verified. r = 4, 6, 8: UNSAT in all variants/solvers/seeds (72 runs) — no collision within the words an 8-step compression reads. r = 10–16: 0-conflict collisions differing in exactly 9 consecutive words (a terminal 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, Alamgir et al. 2024), 31 (Li et al. 2024), 39 SFS.'
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.