Guess I am wrong anyway in my interpretation of his proof. Feels too much like: P doesn't equal NP since sat-solving is hard, which reverses an arrow.

Still, I don't see how he lifts phase transitions: He needs to show that

*all*possible sat-solvers have phase-transition behavior on (specific) sat instances, and I just don't see how one can generalize that from the behavior of a few current DPLL based solvers. (Got bored, read some of the arguments against his construction, starts to make some sense, again.)

A distinguished author comments on the proof at the CACM. It didn't pass scrutiny, both on the use of finite model theory -which I don't understand- and -if I read it correctly- the author has similar doubts on whether a characterization of an NP problem as being hard on phase transition boundaries of some sort is actually a characterization of an NP problem.

The latter interests me. To most people in the field, it feels natural, therefor it must be true. I don't know, I guess one of the results of his failed attempt might actually be that people start looking into whether such an assumption is actually correct. I.e., does the feeling hold up to mathematical rigor?

(Hmm, I wonder whether I got the second part of his argument right. Should look in to it. Read a bit further, of course his constructions are way more elaborate than my weak simplification of his approach. He starts of by assuming P=NP, and tries to derive a contradiction, no idea at the moment. I find it strange that he actually can derive a contradiction. He poses specific clauses, and derives that determining a solution is impossible, though he assumes a P=NP algorithm?)