Is there a public document related to this proposal? Better yet, its security analysis that led to it being discarded?
Most SAT instances are surprisingly easy to solve, hence the "unreasonable" effectiveness of SAT solvers.
The construction of known-hard SAT instances is really building a new kind of crypto primitive out of SAT, and TBH using this kind of primitive versus more well known PoWs has little value to the network, is harder to analyse and is a lot more work for developers.
I mean its useful from a research pov, you'd be building a money-based CTF for solving certain theoretically hard types of SAT instances, but you are basically sacrificing the stability (such as there is...) of the currency to do so.
A really basic security analysis is "here is this thing which is pretty simple to implement and we are very confident it works" versus "here is this new thing that provides no extra intrinsic value, is more complicated, and we're not sure about". I am not sure there was ever a "security proof" that it was a bad idea because none was really required.