Practically P=NP?

Solving is believing

Cropped from source.

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ő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 (update) can be read at two levels. On the surface the paper is about the famous discrepancy conjecture of Paul Erdős, which we have talked about before. I will state the precise conjecture in a moment, it was said that previously the best lower bound for a certain “constant” ג was 1 and they moved it to 2. Since Erdős conjectured that a finite ג 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, we are experimenting with using Hebrew letters to denote constants that aren’t. The logical wording of Erdős’ conjecture is that for any and there are integers and so that

Thus this says that no matter how cleverly the sequence of and is chosen, there is a sub-sequence of the form

whose sum (or its negative) exceeds . Thus the conjecture is about a “for all” kind of negation of a , but the “” itself is the most interesting object—especially in terms of how high you can prove it. Since we really believe this object is infinite, and Georg Cantor started the use of Hebrew letters for infinities, we propose using the corresponding third letter of the Hebrew alphabet, ג (gimel), to stand for it. We also query the usage that they proved as the “” the discrepancy is greater than—why should we define a “” that is greater than itself? So we say instead that what Konev and Lisitsa proved is:

Theorem 1.

ג

Since ג is an integer this means ג , but we say “” to stay similar to the sources.

Un-Bespeakable Proofs?

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

For the particular case of a human proof of the conjecture exists; for 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ő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 ג 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 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 counts his nearly 200 gigabytes of chess analysis data as being 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 probably 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.”

Some Discrepancy Numbers

That ג is obvious: just consider any odd-length sub-sequence. For ג consider , as noted here: no sequence of length 12 has discrepancy 1.

For the more liberal notion that allows arithmetical progressions to begin at any number , summing

the discrepancy has been known since 1964 to grow as at least the fourth-root of the length of the sequence, with a multiplier of . Restricting progressions to be anchored at gives the problem its stylish threads. It is still surprising that no great progress was made for ג until recently, when the PolyMath project popularized the problem.

If ג , then a logical compactness argument gives the following consequence:

For any there is an such that for all , every sequence of length contains a finite -anchored progression whose sum (or its negative) exceeds .

Thus if Erdős’ conjecture is true, then this defines a function from to the greatest . So by this reckoning of “,” . The conjecture is open even under the restriction that the sequence be completely multiplicative: for all and . The corresponding quantities can be smaller, and a computer-generated but human-checked proof has shown that .

A Word on How They Do It

Computing exactly was Konev and Lisitsa’s first goal. Their program first found a sequence of length that had . 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 . 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 -anchored progressions to have its sum in —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 other, 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 . They initially guessed would be about 13,000, but their finds from the “SAT part” have topped 13,800. Uniform ways are known to construct sequences of any length whose discrepancy is , which is incomparably better than the attained by random sequences. But getting only for is a long way from .

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 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ő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, [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 when another Liverpool product came across the Pond 50 years ago, which some say “gave birth to a new world.”

Open Problems

The main question is can we advance and prove ג ? Also is there a non-computer proof that ג ? 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.

Update: “Un-bespeakable” programming is a good context to note this just-released demo by Stephen Wolfram himself of his Wolfram Language.

[re-cast intro slightly, added update, changed poorly designed LaTeX \gimel to HTML 1490]