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: running classification: pending evidence: [] verdict: pending
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.