1---2id: H173title: SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits4axis: C5kind: sha2566statement: For fixed free message bits k, CaDiCaL/Kissat time grows roughly exponentially with the step count s, becoming7 infeasible (300 s) at s ≈ s_k; SMT (Z3 bit-vectors) is slower than SAT on the same cells.8motivation: C2 (SAT/SMT understanding of reduced-round constraints).9assumptions: Tseitin encoding, ripple-carry adders.10expected_contribution: Scaling figure and table across 11 step counts × 7 free-bit counts × 2 solvers.11related_work:12- mironov2006applications13- nejati2017adaptive14- alamgir2024sha25615- biere2024cadical16- demoura2008z317possible_counterexamples: Sub-exponential growth (would be surprising and would need explanation).18verification_strategy: experiments/reduced_round_sha256/preimage_sat.py on M3U96b19computational_budget: ≈ 3 node-hours20status: running21classification: pending22evidence: []23verdict: pending24---2526# H17 — SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits2728For fixed free message bits k, CaDiCaL/Kissat time grows roughly exponentially with the step count s, becoming infeasible (300 s) at s ≈ s_k; SMT (Z3 bit-vectors) is slower than SAT on the same cells.29