For full details I think the best is to read the paper I linked in the original post as the whole process of building the program is outlined in it. A short summary would be that the program must produce boolean formulae for each bit of the sha256 output in terms of boolean variables of the input. These formulae have to be in the standard DIMACS CNF format.