Actually these SAT solvers and model checkers seem like a valid niche for blockchain and a true bit protocol: as an average user of these (i.e. enough that you run it multiple times a day, but not so often that you have a full pipeline of scheduled problems to check) you can have it run on problemms of others (generating coin) and then when you are done interpreting the results of a previous run and reformulating your own problem, you can use your coin to solve your problem quicker...