Moshe Vardi's talk on P v/s NP

Just attended a very interesting talk by Moshe Vardi on P v/s NP. Thought of summarizing it:
- He introduced the concept P (solvable in polynomial time) v/s NP (verifiable in polynomial time) and then compared them to "discovering v/s checking" a proof and which is easier. Say for some reason, P = NP, it would be as easy to discover the proof for a given problem than to read/check the proof given in textbook (as said by Scott Aaronson, everyone would be Gauss). Also gave some examples of P v/s NP problems (hamiltonian/eulerian cycles) and some history.
- Then introduced some basic concepts of finite-model theory, first order logic and k-SAT problem. Then discussed nomenclature of 'phase transition' wrt statistical physics, random k-SAT and XOR-objection on Deolalikar's paper.
- If you don't intend to read Deolalikar's paper, here is what he is trying to say: "9-SAT cannot be in P" (in which he uses Immerman's theorem and random k-SAT), which clearly is not the case if we replace disjunction by XORs (which can be solved by Gauss elimination ... still have to think about this). For more details read Lipton's blog.
- Then Vardi discusses the importance of P v/s NP:
1. If we prove P = NP, still there can be problems of size (10n)^10000 which are in P but take way too long to solve.
2. If we prove P != NP, again there can be NP problems of size n^(log log log n), which then becomes a way faster solution.
- On his closing note, Vardi cites the industry SAT solvers. Though the industry SAT solvers are capable to solve SAT instances with million variables, there are some SAT instances with few hundred variables which are extremely difficult to solve. According to Vardi, identifying those difficult cases is way more important than proving SAT is P (or not in P).

Now, let me quote few of his comments:
=> The argument is using induction to prove set of natural numbers is finite ... set of zero elements is finite, add a natural number to it and it will be finite, then add another and so on ... hence QED.
=> Are they same in theory and practice, well it depends ... in theory they are same, but in practice they are different.
=> Finite model theory ... number of variables ... arbitrary long, but STILL finite.