I did some graduate level research on P =? NP, specifically in the SAT space <https://en.wikipedia.org/wiki/Satisfiability>.
In particular, I helped design MARMOSET (Marmoset Automated Reasoner Mostly Only Solves Easy Theorems), a competitive SAT problem solver. <http://www.cs.unb.ca/research-groups/argroup/marmoset/> . (It's a cool name... I didn't come up with it :))
The conclusion I drew was:
1. P != NP because you can convert in polynomial time every SAT problem down to Horn clauses, which are P to solve, plus non-Horn clauses that cannot be converted i.e. have intractable intrinsic NP complexity whose reduction to the polynomial space requires "clairvoyance" of the quantum computation variety.
2. Nobody's really interested in a proof that P != NP.
That said, I only spent a couple years at it, and my memory may be faulty and I might change my mind if I revisited the issue. Part of me has always felt that the Horn clause reduction is a first step to isolating problems for a next step, but again — it's been a long time.
I doubt that.
P!=NP is one of them.
This is not the case. In my day job I need to worry about what happens if ECDSA is broken. One way that can happen is quantum computation -- but that has a relatively transparent development timeline we can plan for. The other way in which ECDSA could be broken is if P==NP and the discrete log problem can be transformed in polynomial time into another polynomial time algorithm. All of our customer funds could be stolen at that point, with liabilities in the hundreds of millions or billions of dollars.
That's lot of customer money on the line if that happened. My employer might need to pay BIG money for insurance against a P==NP break of ECDSA, or else risk going bankrupt if it happened. A proof of P!=NP would translate directly into cost savings, either in not getting that insurance or in drastically reducing premiums for it.
Let me clarify: Nobody appeared to be interested in funding a graduate student to prove P != NP.
That having been said, an accepted proof that P != NP would result in a Turing award and an additional $1M for solving one of the seven Millenium Prizes. This has been an open problem for decades, and it is a problem of enormous importance and visibility.
Now that is some good SAT solver name - keeping user's expectations low, I guess? Nice choice! ;)