How to use an old SAT solver to discover a new one, as is done in The Golden Ticket? In Lance Fortnow's book The Golden Ticket, he mentions that once you have a polynomial-time algorithm for an NP-complete problem, you can use it to find a faster algorithm. Can you tell me how that is done? And once that is done, you can use the new algorithm to discover an even faster one ad infinitum, till a fixed point. Below is the exact quote from the book:


  "So what do you ask a genie who will grant you only one wish?" said
  the adviser.
  
  "I have no idea," replied Steve.
  
  "You ask for a genie who will grant all your wishes."
  
  The proverbial light bulb went off in Steve's head. He knew there must
  be some better algorithm for solving clique problems out there
  somewhere, but he couldn't figure it out on his own. But he had the
  genie, the Tsinghua code, which could search an exponential number of
  possibilities quickly. So he wrote up a program that used the
  Tsinghua routines to search for a better algorithm for NP problems.
  He got permission to use the computing resources of the National
  Center for Supercomputing Applications (NCSA), based at the University
  of Illinois. After weeks of processing time his work paid off a little
  bit, finding a new algorithm that had a 5 percent improvement over the
  Tsinghua code--good enough for a research paper but not enough to make
  a real impact.
  
  His adviser simply said, "Try again using the new code."
  
  So Steve used his new code to find an even faster algorithm for NP
  problems. A few weeks later he had a 20 percent improvement.
  
  But his adviser was not impressed. "Try it again."
  
  Steve replied, "Why don't I just set up the computer to automatically
  keep trying with the new code it finds?"
  
  The adviser gave that look, the look that told a student he had
  achieved enlightenment, or at least had realized the obvious.
  
  Steve went back to his office and started the tricky process of
  writing code that searches for faster code, and then used this faster
  code to find even faster code and continue this process until it could
  find no further improvement.


Now focus on SAT. MiniSAT is a fast SAT solver, though not to the point of being polynomial-time. 


  How to use MiniSAT to mechanically discover a new SAT solver?
Actually, probably you can't use a SAT solver to find another SAT solver, unless something surprising happens.

If P = NP, then you can.  If P = NP, then the polynomial hierarchy collapses (i.e., P = PH), so there is a polynomial-time algorithm for every problem in PH.  The problem of asking whether there is a faster SAT solving algorithm is essentially a $\Sigma_2$ problem, which is part of the polynomial hierarchy; if the polynomial hierarchy collapses, there's a polynomial-time algorithm for every problem in PH and thus for every problem in $\Sigma_2$.  Thus you can in polynomial time search for a better SAT solver, if P = NP.

But most researchers expect that P is not equal to NP, so this statement is most likely moot and unlikely to be helpful in practice.

If P is not equal to NP, then this reasoning doesn't work.  In fact, many researchers expect that $\Sigma_2$ is even harder than NP (there are problems in $\Sigma_2$ that are harder than any problem in NP), so it would be surprising if there was a simple reduction to express the problem "find me a faster SAT solver" as an instance of SAT.  In particular, SAT solvers can solve SAT, or any other problem in NP -- but in any case, only problems in NP.  If (as we suspect) $\Sigma_2$ is harder than NP, then SAT solvers can't solve problems in $\Sigma_2$.

Of course, we don't actually know.  It's always possible that the conventional wisdom is wrong, and that tomorrow we discover that P is actually equal to NP.  That would be a great surprise, but we can't completely rule it out.

The Golden Ticket is trying to give a deeper understanding of why complexity theorists consider the P vs NP problem so important and so fundamental.  Part of that involves exploring counterfactual worlds and counterfactual assumptions that we suspect are probably false, to see what their consequences would be.



Or, to explain it a different way:

The problem is that finding a better SAT solver is a $\exists \forall $ kind of statement.  The statement is of the form $\exists A \forall x . P(A,x)$, where $P(A,x)$ is the statement that $A$ is fast and correctly solves the SAT instance $x$.  Those kinds of statements can't be solved with a SAT solver.  SAT solvers can solve problems of the form $\exists x. Q(x)$.  However, $\exists \forall$ statements are harder than $\exists$ statements.  This is basically the difference between $\Sigma_2$ and NP.