{\huge Practically P=NP?}

Solving is believing \vspace{.5in}

Boris Konev and Alexei Lisitsa are both researchers at the University of Liverpool, who work in Logic and Computation. They have recently made important progress on the Erd\H{o}s Discrepancy Problem using computer tools from logic. Unlike the approach of a PolyMath project on the problem, their proof comes from a single program that ran for just over 6 hours, a program administered only by them, but mostly not written by them.

Today Ken and I wish to talk about their paper and two consequences of it.

Their paper can be read at two levels. On the surface the paper is about the famous discrepancy conjecture of Paul Erd\H{o}s, which we have talked about before. I will state the precise conjecture in a moment, but suffice it to say that previously the best lower bound for a certain ``constant'' $latex {\gimel}&fg=000000$ was $latex {1}&fg=000000$ and they moved it to $latex {2}&fg=000000$. Since Erd\H{o}s conjectured that a finite $latex {\gimel}&fg=000000$ must not exist, that is it is unbounded, this is a long way from solving the problem. Yet it is the first nontrivial result of any kind on this famous problem.

Note, I am experimenting with using Hebrew letters to denote constants that aren't. The logical wording of Erd\H{o}s' conjecture is that for any $latex {f\colon \mathbb{N}^+ \rightarrow \{-1,+1\}}&fg=000000$ and $latex {C > 0}&fg=000000$ there are integers $latex {k}&fg=000000$ and a $latex {d}&fg=000000$ so that

$latex \displaystyle \left| \sum_{i=1}^{k} f(id) \right| > C. &fg=000000$

$latex \displaystyle f(d), f(2d), f(3d), \dots &fg=000000$

Theorem 1 {\huge

$latex \displaystyle \gimel > 2. &fg=000000$

}

Unbespeakable Proofs?

The abstract of their paper includes a word that I and probably most fellow Americans would blip on:

For the particular case of $latex {C = 1}&fg=000000$ a human proof of the conjecture exists; for $latex {C = 2}&fg=000000$ a bespoke computer program had generated sequences of length 1124 of discrepancy 2, but the status of the conjecture remained open even for such a small bound.

Looking in my English-English/English-English dictionary, I find the phrase ``bespoke tailor,'' but nothing to do with bespoke programs. Of course Ken from his long time in England knew the word means ``by commission'' or ``custom-made,'' as in custom-tailored. Well custom tailors have dwindled even more on this side of the Pond. The first consequence I see in their paper is that this may start happening for hand-made proofs and programs too.

Note their paper is entitled ``A SAT Attack on the Erd\H{o}s Discrepancy Conjecture.'' That's right, SAT as in complexity, or really SAT as in solver. What they did was ``meta'': they coded their requirements for a proof of $latex {\gimel > 2}&fg=000000$ up as a SAT problem. They really use both the ``SAT'' and ``UNSAT'' sides of what the solver gives:

• First they construct a long finite sequence of discrepancy 2, meaning that 2 is the maximum of all finite sums $latex {f(d) + f(2d) + \cdots f(kd)}&fg=000000$ in it.
• Then they show that no longer such sequence can be found.

The latter, the UNSAT proof, is what's not checkable by hand. It prints to a 13-gigabyte file. Ken reckons his nearing-200-gigabytes of chess analysis data at 2 kilobytes to a ``page,'' so by that measure their proof fills 6.5 million pages. As several news articles point out, this dwarfs the 15,000 pages of the classification of finite simple groups, and even tops the estimated 10 gigabytes of the entire printed content of Wikipedia in English.

Such a length seems unspeakable. If the authors required us to verify a custom-tailored program on top of that, we'd agree. However, they dress for success with a mail-order wardrobe of SAT solvers. Hence their proof is unbespeakable. Once you take the measurements they need---their logical requirements and SAT encoding---you can order the computation from any suitable e-tailer for SAT. As our friend Gil Kalai is quoted as saying:

``I'm not concerned by the fact that no human mathematician can check this, because we can check it with other computer approaches.''

A Word on How They Do It

That $latex {\gimel \geq 1}&fg=000000$ is obvious: just consider any odd subsequence. Human proofs had been made for $latex {\gimel > 1}&fg=000000$. For the more liberal notion that allows arithmetical progressions to begin at any number $latex {b}&fg=000000$, summing

$latex \displaystyle f(b + d), f(b + 2d), f(b + 3d), \dots, &fg=000000$

If $latex {\gimel = \aleph_0}&fg=000000$, then a logical compactness argument gives the following consequence:

For any $latex {C > 0}&fg=000000$ there is an $latex {n_C > 0}&fg=000000$ such that for all $latex {n \geq n_C}&fg=000000$, every sequence of length $latex {n}&fg=000000$ contains a finite $latex {0}&fg=000000$-anchored progression whose sum (or its negative) exceeds $latex {C}&fg=000000$.

Thus if Erd\H{o}s' conjecture is true, then this defines a function $latex {g}&fg=000000$ from $latex {C}&fg=000000$ to the greatest $latex {n_C}&fg=000000$. Computing $latex {g(2)}&fg=000000$ exactly was Konev and Lisitsa's first goal. Their program first found a sequence of length $latex {1160}&fg=000000$ that had $latex {C=2}&fg=000000$. The previous best had been a sequence of length 1124. This used a SAT solver to find a set of boolean values so that encoded a sequence with $latex {C=2}&fg=000000$. The virtue of the SAT side of the solvers is that if they return a answer, then it can be easily checked by others. A sequence of length 1160 can certainly be checked by others with a tiny program that runs in seconds on their phone.

The much more difficult part came when they increased the length to 1161. Showing that there is no sequence---that no sequence enables each of its $latex {0}&fg=000000$-anchored progressions to have its sum in $latex {[-2,+2]}&fg=000000$---requires a SAT solver that returns a proof of UNSAT. This is much harder in general, but it worked in this case. The certificate of UNSAT is much larger than the 1160 sequence, and it requires the many gigabytes of memory. Thus checking it independently becomes much harder.

Konev and Lisitsa have a separate page on the details of their encoding, helping others to check their work. And also to appreciate it, because it needs some cleverness. An ``obvious'' encoding requires too many variables. One of the keys in making SAT attacks of this type is in how one encodes the problem.

They are currently working on $latex {C = 3}&fg=000000$. They initially guessed $latex {n_3}&fg=000000$ would be about 13,000, but their finds from the ``SAT part'' have topped $latex {13,800}&fg=000000$. Uniform ways are known to construct sequences of any length $latex {n}&fg=000000$ whose discrepancy is $latex {O(\log n)}&fg=000000$, which is incomparably better than the $latex {O(\sqrt{n})}&fg=000000$ attained by random sequences. But getting only $latex {3}&fg=000000$ for $latex {n = 13,800}&fg=000000$ is a long way from $latex {\log n}&fg=000000$.

P=NP?

Their paper can also be read at another level, below the surface, that reflects on complexity theory. Their paper shows that there are SAT solvers capable of solving hard natural problems in reasonable time bounds. What does this say about the strong belief of most that not only is $latex {\mathsf{P} \neq \mathsf{NP}}&fg=000000$ but that the lower bounds are exponential?

I wonder sometimes if we in complexity theory are just plain wrong. Often SAT solver success is pushed off as uninteresting because the examples are ``random,'' or very sparse, or very dense, or special in some way. The key here, the key to my excitement, is that the SAT problem for the Erd\H{o}s problem is not a carefully selected one. It arises from a longstanding open problem, a problem that many have tried to dent. This seems to me to make the success by Konev and Lisitsa special.

John Lubbock once said: What we see depends mainly on what we look for. Do we in complexity theory suffer from this? As they say across the Pond, this is bang-on. According to our friends at Wikipedia Lubbock was: The Right Honourable John Lubbock, 1st Baron Avebury MP FRS DCL LLD, known as Sir John Lubbock, 4th Baronet from 1865 until 1900, was a banker, Liberal politician, philanthropist, scientist and polymath. I know he lived many years ago, but note he was a polymath: hmmm... Meanwhile I remember that another Liverpool product came across the Pond 50 years ago.

Open Problems

The main question is can we advance and prove $latex {\gimel >3}&fg=000000$? Also is there a non-computer proof that $latex {\gimel > 2}&fg=000000$? I have no problem with such proofs in general, but I certainly prefer proofs that I can understand. Tim Gowers says he like Gil has a ``relaxed'' view of such proofs, so perhaps we should too.

The real long-term question, for both of us, is what does this type of success say about our beliefs in complexity theory? Does it not shake you a tiny bit, make you a wee bit worried, that we may have made a serious error. That our ``belief'' that SAT is hard is wrong? Ken has a motive given here for trying out some \#SAT solvers, which are out there too.