# 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.

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?

• @ZiruiWang - Finding an algorithm from a fixed set of candidate algorithms is typically a $\Sigma_2$/$Pi_2$ problem rather than an NP-complete problem. The author could have meant that (they can be solved by nested SAT solvers). Alternatively, the author could have mean to optimize certain parameters of existing algorithms. – DCTLib Jun 2 '16 at 9:04
• The set of algorithms is infinite. You will only be able to find an algorithm using a SAT solver if your fix the search space. The search space will then be the space of candidate algorithms. Nesting SAT solvers to find new algorithms is described in this paper: link.springer.com/article/10.1007%2Fs10009-012-0249-7 – DCTLib Jun 2 '16 at 10:27
• "Finding an algorithm" is essentially synthesis. It is in Sigma_2, because we want to check (1) if there exists an implementation such that (2) for all inputs, the implementation works correctly. The part after the (2) is essentially a co-NP problem. You could call it nested as whenever the one SAT solver finds a solution, the other SAT solver is used to check it. When this is not the case, clauses are added to the first one. The first SAT solver thus repeats its work until the second is fine with the solution. So a SAT solver is called in a SAT procedure. – DCTLib Jun 2 '16 at 12:15
• @DCTLib The assumption is that P = NP, so PH collapses and everything simplifies to P. – Zirui Wang Jun 2 '16 at 13:19
• @DCTLib, lots of great comments there. Want to write a full answer? – D.W. Jun 2 '16 at 14:20

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.

• Why can't a SAT solver solve a $\Sigma_2$ statement? It's still exponential-time. The difficulty lies in the encoding. – Zirui Wang Jun 2 '16 at 19:49
• @ZiruiWang, I edited the fourth paragraph of my answer to explain why more explicitly. SAT solvers can't solve all exponential-time problems (unless NP = EXPTIME, which we suspect is not the case). – D.W. Jun 2 '16 at 19:51
• @ZiruiWang You can probably encode many problems as SAT, but they might not be polynomial in length. SAT hits hard cases for polynomial input, so running it on an exponentially-sized input is probably not going to work. – jmite Jun 2 '16 at 19:55