Degenerate Conditional Clauses for CDCL Hash Cryptanalysis

Standard Conflict-Driven Clause Learning (CDCL) solvers can struggle on dense XOR-heavy encodings in SHA-256 differential instances, traditionally motivating solvers with Gaussian elimination such as CryptoMiniSat. We identify a Boolean Constraint Propagation (BCP) blind spot in standard Conjunctive Normal Form (CNF) encodings of SHA-256 nonlinear functions Ch and Maj. To resolve this, we introduce degenerate conditional differential equivalence clauses that explicitly encode differential propagations otherwise missed by BCP. The current reproducible Docker AE artifact yields 18-step free-start speedups of 19.87x on CaDiCaL 3.0.0, 30.72x on Kissat 4.0.4, and 8.84x on CryptoMiniSat 5.8.0. These runs show 89-98% conflict reductions. A separate legacy single-instance CaDiCaL 1.9.5 run on a harder 18-step path reports 267.9x, but we keep this legacy family separate from the Docker AE claim and do not treat it as a pooled benchmark. Across measured path families, speedup grows with baseline difficulty, with a break-even threshold around 52s. At 20 steps, the measured long-run CaDiCaL path shows 29.2x speedup and 94% conflict reduction, while a higher-difficulty path family shows greater-than-135x lower-bound speedups for pure CDCL solvers from timeout evidence. White-box statistics reveal the mechanism: 53-58% fewer conflicts and 43-45% fewer restarts at 18 steps, with BCP throughput increasing from 12-13% at 18 steps to approximately 3x at 20 steps as instances grow harder. These findings, together with negative results for carry-chain and Sigma0/Sigma1 clauses, provide evidence-backed guidelines for CNF optimization in symmetric cryptanalysis.