exploring which input bits effect which output bits (1, 2 or 3 at a time) might be interesting
I don't expect SHA2 to be broken by the ways discussed in this thread, but it's a good thing that someone tries it. A good result from such approach would be not analytical solution (seems impossible, but there always is a hope that equations system will collapse 
), but representation of double SHA2 better (by operations count or height) that ones currently used in ASICs. I think I know how to chop 10% (or so) off from ~120000 binary operations, but let's hope that this thread will bring some fresh ideas logred_v8.zip ready - faster computation of !a which is the most expensive operation.
ri seems to have almost exactly 2i-1 terms. So the last bit r31 will have 230 terms. I've confirmed this with ri i=0..12 and it's bang on. The Quine-McClumskey reduction sure does a number on the complexity but it's not enough.
botnet - to take this further, you need to demonstrate that one of the input bits of the sha256 compression function does not pass through the Least Significant Bit inputs of the adds.
Or show one of the compression function output bits do not depend on the Most Significant Bit outputs of the 32bit adds.
Or that chained 32-bit adds have some reductions.
Cheers