{\huge How Hard, Really, is SAT?}
A new longest computer proof makes us wonder about things from security to the Exponential Time Hypothesis \vspace{.5in}
Marijn Heule, Oliver Kullmann, and Victor Marek are experts in practical SAT solvers. They recently used this ability to solve a longstanding problem popularized by Ron Graham.
Today Ken and I want to discuss their work and ask a question about its ramifications.
The paper by them---we will call it and them HKM---is titled, ``Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer.'' The triples problem is a ``Ramsey''-like question raised years ago by Graham. Cube-and-Conquer is a method for solving large and complex SAT problems. Sandwiched between is a clever new tuning of resolution SAT methods called ``DRAT'' which we discuss in some detail.
The Pythagorean Triples Problem
Ron was interested in a problem that generalizes Schur's Theorem, due to Issai Schur. Suppose we color the numbers $latex {\{1,\dots,N\}}&fg=000000$ red and green. Can we always find $latex {a,b,c}&fg=000000$ three distinct numbers of the same color so that
$latex \displaystyle a + b = c?&fg=000000$
Schur's theorem says that provided $latex {N}&fg=000000$ is large enough this is true. Note that another way of putting this is that with $latex {S = \{a,b\}}&fg=000000$, all elements of the set $latex {\mathsf{nes}(S)}&fg=000000$ of nonempty sums from $latex {S}&fg=000000$ are the same color. Several mathematicians independently proved the extension that there are arbitrarily large sets $latex {S}&fg=000000$ with this property---indeed for any number of colors:$latex \displaystyle (\forall k)(\forall m)(\exists C)(\forall \chi: \mathbb{N} \rightarrow [k])(\exists S \subseteq [C], |S| = m)(\exists j \in [k])(\forall s \in \mathsf{nes}(S))\chi(s) = j. &fg=000000$
All the sums of course are linear. What happens if we go to higher powers $latex {p}&fg=000000$? If we simply look at $latex {p}&fg=000000$-th powers of sums from $latex {S}&fg=000000$ then we tie into the same theorem via $latex {\chi'(x) = \chi(x^p)}&fg=000000$ for all $latex {x}&fg=000000$. Taking sums of $latex {p}&fg=000000$-th powers such as $latex {a^p + b^p}&fg=000000$ is different. We can map that case into the simple sums problem with $latex {S' = \{a^p,b^p\}}&fg=000000$ in place of $latex {S = \{a,b\}}&fg=000000$, but it is not clear how to argue similarly with mapped colorings $latex {\chi'}&fg=000000$. Sets of the form $latex {S'}&fg=000000$ are special.
We can make them even more special by requiring $latex {a^p + b^p}&fg=000000$ to be a perfect $latex {p}&fg=000000$-th power too. OK, for $latex {p \geq 3}&fg=000000$ we are kidding, but the case $latex {p = 2}&fg=000000$ and $latex {m = 2}&fg=000000$ is the famous one of Pythagorean triples. Suppose we color the numbers $latex {\{1,\dots,N\}}&fg=000000$ red and green. Can we always find three distinct numbers $latex {a,b,c}&fg=000000$ of the same color so that
$latex \displaystyle a^{2} + b^{2} = c^{2}? &fg=000000$
This is the question Ron asked. In the spirit of Paul Erd\H{o}s, he offered $100 for a solution.The answer from HKM is that this extension is true. Perhaps that is not too surprising, since many problems can be generalized from from linear to non-linear cases. But what is really perhaps the most interesting part is that HKM found a proof via using SAT solvers.
The Theorem
The exact theorem HKM prove is:
Theorem 1 The set $latex {\{1,\dots,7824\}}&fg=000000$ can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for $latex {\{1,\dots,7825\}}&fg=000000$.
Note, this shows that Schur's theorem does extend from $latex {a+b=c}&fg=000000$ to $latex {a^{2}+b^{2}=c^{2}}&fg=000000$.
What is special about $latex {7,\!825}&fg=000000$? According to this list of triples up to $latex {c = 10,\!000}&fg=000000$, which is linked under ``Integer Lists'' from Douglas Butler's TSM Resources site, there are seven Pythagorean triples involving $latex {7,\!825}&fg=000000$:
$latex \displaystyle \begin{array}{rcl} 625^2 + 7800^2 &=& 7825^2\\ 1584^2 + 7663^2 &=& 7825^2\\ 2191^2 + 7512^2 &=& 7825^2\\ 2784^2 + 7313^2 &=& 7825^2\\ 4180^2 + 6615^2 &=& 7825^2\\ 4695^2 + 6260^2 &=& 7825^2\\ 5180^2 + 5865^2 &=& 7825^2 \end{array} &fg=000000$
There are five distinct entries for $latex {c = 7,\!820}&fg=000000$, various others before it, and quite a few for $latex {7,\!830}&fg=000000$ after it. Nothing, however, shouts why $latex {7,\!825}&fg=000000$ is a barrier. It seems better to think of it as a tipping point.
The Proof
There are $latex {2^{7,\!825}}&fg=000000$ colorings for the numbers up to $latex {7,\!825}&fg=000000$. This immediately stops any simple brute-force approach. What must be done is to break the immense number of cases down to a more manageable number. HKM did this by clever use of known SAT methods with at the addition of heuristics that are tailored to this question.
The previous best positive result had been a 2-coloring of $latex {[1 .. 7,\!664]}&fg=000000$ with no monochromatic triple, so HKM had a good idea of how large an $latex {N}&fg=000000$ to try. The SAT encoding is simple: use variables $latex {x_i}&fg=000000$ for $latex {2 \leq i \leq N}&fg=000000$, and for every $latex {(a,b,c)}&fg=000000$ such that $latex {a^2 + b^2 + c^2}&fg=000000$, include the clauses
$latex \displaystyle (x_a \vee x_b \vee x_c) \wedge (\bar{x}_a \vee \bar{x}_b \vee \bar{x}_c). &fg=000000$
If we give $latex {x_i = 1}&fg=000000$ the meaning that the number $latex {i}&fg=000000$ is colored green, then this says that for every Pythagorean triple, at least one member must be green and at least one must be red. 3SAT remains NP-complete for clauses of all-equal sign, as follows by tweaking the proof at the end of this post.Now with $latex {N = 7,\!825}&fg=000000$, what HKM needed to do was to prove the formula unsatisfiable. Proving satisfiability is easy when you know or guess a satisfying assignment---in this case, a coloring. The following graphic from the Nature article on their work shows a coloring for $latex {7,\!824}&fg=000000$ in which the white squares are ``don't-cares''---they can be either color:
\includegraphics[width=3.5in]{HKMsolution-7824 copy.jpg}
The top row goes 24 squares; the one after them is the sticking point. How to prove there is no consistent way to color it? Given the formula $latex {F = C_1 \wedge C_2 \wedge \cdots \wedge C_m}&fg=000000$, it may be hard to recognize that it entails a contradiction. The general idea is to add more clauses $latex {C}&fg=000000$ to make a formula $latex {F'}&fg=000000$ so that:
DRAT the RAT
Besides good guesses for $latex {N}&fg=000000$, HKM were armed with the latest knowledge on well-performing heuristics. A 2012 paper by Matti Järvisalo with Heule and Armin Biere includes an overview of resolution-related properties involving a big array of acronyms such as AT and HBC and RHT. The AT stands for ``asymmetric tautology'' and the 'R' prefix applied to a formula property $latex {P}&fg=000000$ enlarges $latex {P}&fg=000000$ by adding cases where a certain kind of resolution yields a formula with $latex {P}&fg=000000$. Combining these two yields the following definition---we paraphrase the newer paper's version informally:
Definition 2 Given a formula $latex {F}&fg=000000$ and a clause $latex {C}&fg=000000$ not in $latex {F}&fg=000000$, say $latex {C}&fg=000000$ has RAT via a literal $latex {z}&fg=000000$ in $latex {C}&fg=000000$ if for all clauses $latex {D}&fg=000000$ of $latex {F}&fg=000000$ containing $latex {\bar{z}}&fg=000000$ the following happens: when you make the other literals in $latex {C}&fg=000000$ and $latex {D}&fg=000000$ false, remove $latex {D}&fg=000000$, and simplify, you get an immediate contradiction.
We should say more about ``simplify'': Suppose $latex {z_1,\dots,z_k}&fg=000000$ are those other literals. Making them false is the same as making the formula $latex {F_0 = F \setminus \{D\} \wedge \bar{z}_1 \wedge \bar{z}_k}&fg=000000$ which has their negations as unit clauses. We simplify by removing for each $latex {i}&fg=000000$ all clauses with $latex {z_i}&fg=000000$ (those were satisfied) and deleting $latex {\bar{z}_i}&fg=000000$ from other clauses. After doing this, there may be other unit clauses, whereupon we repeat. If we get both $latex {y}&fg=000000$ and $latex {\bar{y}}&fg=000000$ for some variable $latex {y}&fg=000000$, that's the immediate contradiction we seek. What's important is that this unit resolution process, while ``logically'' inferior to full resolution, stops in polynomial time.
Now suppose $latex {F}&fg=000000$ is satisfiable and $latex {C}&fg=000000$ has RAT via $latex {z}&fg=000000$. If there is a satisfying assignment $latex {a}&fg=000000$ of $latex {F}&fg=000000$ that sets $latex {z}&fg=000000$ or one of the other literals in $latex {C}&fg=000000$ true, then $latex {F' = F \wedge C}&fg=000000$ is also satisfied. So suppose $latex {a}&fg=000000$ sets them all false. Now there must exist a clause $latex {D}&fg=000000$ in $latex {F}&fg=000000$ containing $latex {\bar{z}}&fg=000000$ such that $latex {a}&fg=000000$ sets the other literals in that clause false---if none then we could have set $latex {z}&fg=000000$ true after all. Then $latex {F_0}&fg=000000$ above is satisfied by $latex {a}&fg=000000$, but this is a contradiction of the (immediate) contradiction.
Note also that if $latex {F' = F \wedge C}&fg=000000$ is satisfiable then of course so is $latex {F}&fg=000000$. This isn't important to the unsatisfiability proof but is good to know: RAT clauses can be added freely. The trick is to find them. Definition 2 was crafted to make it polynomial-time recognizable that $latex {C}&fg=000000$ is RAT when you have it, but you still have to find it. A particularly adept choice of $latex {C}&fg=000000$ may allow simplifications that delete other clauses, yielding a technique called DRAT for ``Deletion Resolution Asymmetric Tautology'' proofs.
This is where the other ingenious heuristics---tailored for the triples problem but following a general paradigm called ``cube-and-conquer''---come in. We'll refer those details to the paper and its references, but this breakthrough should make one excited to read more about the state of the art.
Dart the Art?
The problem took ``only'' two days of computing on a supercomputer.---the Texas Advanced Computing Center. The computation generated 200 terabytes of raw text output. It is not clear to us whether even more intermediate text was generated on-the-fly as unsuccessful moves were backtracked-out, or how much. HKM say in their abstract:
\dots Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking.
As with all computer proofs we still would like a human readable proof. It is not that we do not trust the validity of the current proof, but rather that we would like to ``understand'' if possible why Ron's problem is true. Can we possibly extract from the certificate a dart of reasoning that yields a shorter explanation? It might be a numerical potential function whose values $latex {v}&fg=000000$ in this case are guessable and verifiable, such that $latex {v > t}&fg=000000$ for some threshold $latex {t}&fg=000000$ analytically implies unsatisfiability.
We also wonder why the size-$latex {N}&fg=000000$ formulas treated here should be any more difficult than ones you can get for factoring $latex {N}&fg=000000$-bit numbers. As we noted above, the all-signs-equal condition on the literals comes without loss of generality. So the degree of ease that allowed solving on a university center in two days must come from how the Pythagorean pattern gave a leg up to ``cube-and-conquer.'' For factoring there might be other legs---and the ``$latex {N}&fg=000000$'' from current security standards might yield even smaller formulas.
Last, as noted in the papers we've linked, the DART condition has universality properties with regard to resolution in general, yet builds on steps that are in polynomial-time $latex {p(n)}&fg=000000$. It was an incremental liberalization of previously used steps, and this makes us wonder whether it can be enhanced further while still yielding proofs that take up $latex {g(n)p(n)}&fg=000000$ length and time. Perhaps we can get the $latex {g(n)}&fg=000000$ part to be $latex {2^{o(n)}}&fg=000000$? That would refute some forms of the ``Exponential Time Hypothesis,'' which we last discussed here.
Open Problems
The most immediate questions raised by this wonderful work are: what about other equations, and what about allowing more colors? Does having three colors zoom the problem beyond any hope of attack by today's computers, or will the practical breakthroughs continue a virtuous cycle with advances in theory that bring more cases into the realm of feasibility? Is there an asymptotic analysis that might guide our ability to forecast this?