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?