The answer might be obvious, but I'm not a hardware guy: couldn't they use a FPGA to do the compilation itself, or at least the bin-packing part? Is there a way to code a general SAT-solver in FPGA?