How to use an old SAT solver to discover a new one, as is done in The Golden Ticket?
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.