I am running into some memory concerns, mostly due to all the parallelization. The fewer variables in these equations the better 
http://jheusser.github.io/2013/02/03/satcoin.html
SAT solvers tried, didn't work. But I'd still like to see a set of 256 monster logic formula with 2048 bit inputs for the SHA256 round function.