id: H17 title: SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits axis: C kind: sha256 statement: For 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. motivation: C2 (SAT/SMT understanding of reduced-round constraints). assumptions: Tseitin encoding, ripple-carry adders. expected_contribution: Scaling figure and table across 11 step counts × 7 free-bit counts × 2 solvers. related_work:
- mironov2006applications
- nejati2017adaptive
- alamgir2024sha256
- biere2024cadical
- demoura2008z3 possible_counterexamples: Sub-exponential growth (would be surprising and would need explanation). verification_strategy: experiments/reduced_round_sha256/preimage_sat.py on M3U96b computational_budget: ≈ 3 node-hours status: evaluated classification: empirical_observation evidence:
- results/reduced_round_sha256/summary.json
- results/reduced_round_sha256/preimage_sat_scaling.json verdict: '572 cells, all SAT answers re-hashed. r ≤ 16: solved by propagation (0 conflicts, ≤ 0.03 s) for any k. r ≥ 20: only k = 16 solved (CaDiCaL 6.4 s at r = 20, 87 s at r = 32, 262 s at r = 64 for 2/3 seeds); every k ≥ 24 cell times out at 300 s; Z3 2–4 orders of magnitude slower and times out at r ≥ 16. Generic SAT is slower than 2^16 brute force once the expansion matters.'
H17 — SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits
For 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.