Stream: Coq users

Topic: Possible polynomial NP-complete solution


view this post on Zulip Victor Porton (Apr 09 2021 at 20:01):

I proved a theorem and then "Linux guessed from it an efficient NP-complete algorithm" :-) and my computer broke, so I write in this chat instead of a normal communication. That was a joke, next there is a serious theorem:

view this post on Zulip Victor Porton (Apr 09 2021 at 20:09):

I've proved that my algorithm is NP-complete under assumption that P=NP. bit.ly/2Q5Xv2V0 Formalize it!

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:09):

I get a 404 for the bit.ly link :-(

view this post on Zulip Victor Porton (Apr 09 2021 at 20:11):

https://math.portonvictor.org/2021/04/08/my-algorithm-that-is-np-complete-in-the-case-if-pnp/

view this post on Zulip Victor Porton (Apr 09 2021 at 20:13):

It is simpler than you can imagine: proving provability of invertibility of an algorithm is clearly an NP-complete problem. To solve it I just enumerate and run parallel all algorithms.

view this post on Zulip Victor Porton (Apr 09 2021 at 20:14):

Previous message had two typos, corrected.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:29):

I skimmed the paper, and I'm confused on the part about enumerating all algorithms—wouldn't this require that the set of all possible algorithms be countably infinite?

view this post on Zulip Victor Porton (Apr 09 2021 at 20:32):

The set of all algorithms is obviously countably infinite.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:35):

Oh yeah, ignore me :-P

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:36):

In that case, I guess my next question is: Can you interleave an infinite number of algorithms? (Wouldn't it take an infinite amount of time to finish e.g. the first step?)

view this post on Zulip Victor Porton (Apr 09 2021 at 20:36):

https://www.google.com/search?q=markov+algorithms is simple to implement

view this post on Zulip Victor Porton (Apr 09 2021 at 20:37):

Loop N algorithms adding one more algorithm after each loop.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:39):

Oh yeah, I remember that now (sorry, I don't remember much of the details from when I learned about complexity)

view this post on Zulip Victor Porton (Apr 09 2021 at 20:39):

0 0 1 0 1 2 0 1 2 3...

view this post on Zulip Victor Porton (Apr 09 2021 at 20:43):

So will somebody formalize my proof soon?

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:45):

Just checked out the references in the paper and they pose a question that I'm also stuck on: For the algorithm to be in polynomial time, I assume each individual A_n also does. Is that requirement explicitly mentioned in the paper?

view this post on Zulip Victor Porton (Apr 09 2021 at 20:46):

No, it's enough that just one "good" A is polynomial

view this post on Zulip Victor Porton (Apr 09 2021 at 20:47):

Just one of An finishes normally, the rest are terminated in the middle.

view this post on Zulip Victor Porton (Apr 09 2021 at 20:51):

BTW, my first solution attempt used (without me noticing that I have no definition) fractional number of algorithm steps. Then I was doing a sum of infinite number of steps being finite. That's not defined, but I think, it can be defined with some new concepts. But my new algorithm is simpler.

view this post on Zulip Victor Porton (Apr 09 2021 at 20:52):

An is even not required to halt.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:52):

Okay I lied, I do have another question: How do we know when we've found the "correct" A_n? (More explicitly, does A_n return "yes"/"no", or does it return an actual proof of that fact? I think the latter, but I want to make sure I'm understanding it right.)

view this post on Zulip Victor Porton (Apr 09 2021 at 20:54):

An "should" return a proof (or not a proof, in which case we ignore the result). Most results will be "garbage".

view this post on Zulip Victor Porton (Apr 09 2021 at 20:56):

It returns a proof in some formal system like first-order predicate calculus. Maybe for coq implementation, it's easier to use a lambda calculus.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:57):

Makes sense. In that case, how do we know that a polynomial A exists? If A returns a proof of the correctness of an algorithm A', I don't think that A' being polynomial necessarily implies A is polynomial (cause proofs can get really big).

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:58):

(Again, please pardon any errors I am making, will make, and/or have been making; I'm only a simple undergrad :-P)

view this post on Zulip Victor Porton (Apr 09 2021 at 20:59):

So, the proof idea is that it searches for the first polynomial NP-complete algorithm and it produces the result. But it may terminate earlier if we find another algorithm that isn't polynomial or NP-complete but solves the problem for a particular input data.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 20:59):

But doesn't each algorithm we run during the interleaving step actually return a proof, rather than just "yes"/"no"?

view this post on Zulip Victor Porton (Apr 09 2021 at 21:00):

We assume existence of some NP-complete (polynomial) algorithm by the conditions of my theorem.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:02):

I thought NP-complete only says "there exists a polynomial-time verifier" but not necessarily that the verifier returns a proof?

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:03):

(in which case you have to know a priori which verifier is the right one)

view this post on Zulip Victor Porton (Apr 09 2021 at 21:03):

On your first question. Proof size is polynomial because in our assumptions run time of the entire algorithm is polynomial

view this post on Zulip Victor Porton (Apr 09 2021 at 21:04):

I use proofs as certificates. I specially specialized the problem for all certificates to be proofs.

view this post on Zulip Victor Porton (Apr 09 2021 at 21:05):

An returns a proof. Verifier returns like yes/no

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:09):

Is it valid to constrain the certificates like that? I was under the impression that NP-completeness only means 1) there exists some polynomial-length certificate as well as 2) some polynomial-time algorithm to check it (in which case the certificate itself doesn't need to be a proof)

view this post on Zulip Victor Porton (Apr 09 2021 at 21:10):

Any finite object can be used as a certificate. Proofs are finite objects. So nothing invalid.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:17):

"A certificate can be a proof" doesn't necessarily imply that "All certificates are proofs" though, unless I'm getting lost somewhere

view this post on Zulip Victor Porton (Apr 09 2021 at 21:18):

In general not all certificates are proofs. But in my article all certificates that I mention are proofs.

view this post on Zulip Victor Porton (Apr 09 2021 at 21:20):

In other words, I replaced the problem of finding an NP-complete algorithm with equivalent problem of finding an NP-complete algorithm with proofs as certificates.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:22):

Couldn't it be true though that, for some NP-complete problem, no polynomial-length proof exists (instead, only a polynomial-length/-time certificate/certifier combination)?

view this post on Zulip Victor Porton (Apr 09 2021 at 21:23):

I'm not quite sure. I think, you are right. But there is no need to consider all NP-complete problems (I consider just one).

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:25):

Oh I see: Is it correct to say, then, that this decision algorithm only works for NP-complete problems which we know beforehand to have polynomial-length proofs?

view this post on Zulip Victor Porton (Apr 09 2021 at 21:26):

No. My algorithm always solves my problem. The only question if it's polynomial. I proved it's polynomial if p=np.

view this post on Zulip Victor Porton (Apr 09 2021 at 21:29):

I consider only one NP-complete problem

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:31):

So is the overall statement, then, that there exists at least one NP-complete problem for which this algorithm is correct?

view this post on Zulip Victor Porton (Apr 09 2021 at 21:32):

Yes, and moreover I proved it's polynomial if p=np

view this post on Zulip Victor Porton (Apr 09 2021 at 21:33):

You are a Christian. I have a theological theory: the mind of Jesus is an NP complete algorithm

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:35):

Victor Porton said:

Yes, and moreover I proved it's polynomial if p=np

Is P=NP even required for the overall algorithm to be polynomial, then? Couldn't the algorithm just search through all possible proofs even if P<>NP, since a polynomial-length proof must exist by the original assumptions?

view this post on Zulip Victor Porton (Apr 09 2021 at 21:37):

If p!=np, then my algorithm isn't polynomial, as the inverse statement proves p=np

view this post on Zulip Victor Porton (Apr 09 2021 at 21:38):

P=np if and only if my algorithm is polynomial

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:39):

Suddenly I'm wondering: Doesn't the existence of this algorithm imply that the NP-complete problem we're solving isn't actually NP-complete?

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:39):

because the algorithm, as far as I can tell, never actually uses the assumption that P=NP

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:40):

meaning that we have a polynomial-time algorithm for solving this particular problem, which implies it's not actually NP-complete to begin with

view this post on Zulip Victor Porton (Apr 09 2021 at 21:40):

I don't understand your logic. But I proved (unless some error) that my problem is NP-complete. The proof is that my problem subsumed proof finding.

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:40):

Or, summarized: I think this algorithm might actually be a proof that an NP-complete problem cannot have a polynomial-length proof

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:41):

Oh yeah, I've been implicitly assuming P<>NP

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:41):

oops

view this post on Zulip Joshua Grosso (Apr 09 2021 at 21:42):

So I guess it's more a general statement, then: Any problem with a polynomial-length proof is in P.

view this post on Zulip Victor Porton (Apr 09 2021 at 21:42):

First, I don't know if my algorithm is polynomial. Second, p=np if and only if my algorithm is polynomial.

view this post on Zulip Victor Porton (Apr 09 2021 at 21:43):

It's false

view this post on Zulip Victor Porton (Apr 09 2021 at 21:43):

Correction: it's false unless p=np.

view this post on Zulip Victor Porton (Apr 09 2021 at 21:57):

Will you work on formalizing this?

view this post on Zulip Victor Porton (Apr 09 2021 at 22:00):

Looks like I almost proved p!=np. I will tweet.

view this post on Zulip Victor Porton (Apr 09 2021 at 22:02):

I cannot tweet because my pc is broken. Here is my proposed p!=np proof:

view this post on Zulip Victor Porton (Apr 09 2021 at 22:03):

Run my algorithms An in parallel not in equal time but each two times less CPU time than the previous.

view this post on Zulip Victor Porton (Apr 09 2021 at 22:05):

Ignore this, my p!=np proof idea was erroneous.

view this post on Zulip Victor Porton (Apr 10 2021 at 05:01):

I meant: your "might be actually a proof" is false.

view this post on Zulip Paolo Giarrusso (Apr 10 2021 at 07:12):

FWIW: This sounds related to Levin search https://steemit.com/steemstem/@markgritter/leonid-levin-s-universal-algorithm, and especially it sounds very similar to the extension by Hutter https://arxiv.org/pdf/cs/0206022.pdf, which in addition proves optimality.

view this post on Zulip Paolo Giarrusso (Apr 10 2021 at 07:13):

While Hutter does not discuss NP-completeness, since his algorithm is asymptotically optimal on each given problem, if P = NP it’d also be polynomial for NP problems. (EDIT: IIUC).

view this post on Zulip Victor Porton (Apr 10 2021 at 08:48):

So, my discovery isn't as big as I thought?! It was known a constructive solution for p=np if p=np? Why do I see everywhere the claim that constructivity of p=np is unknown?!

view this post on Zulip Paolo Giarrusso (Apr 10 2021 at 09:35):

Those are good questions, I am only pointing to potential related work in case that’s helpful.

Hutter does not discuss constructivity explicitly, and his proof seems a conventional proof in classical logic, not intuitionistic logic (I have no idea how hard it’d be to adapt it).

view this post on Zulip Paolo Giarrusso (Apr 10 2021 at 09:55):

If I may also ask questions, I’m also confused about something, and I was unable to resolve my confusion by reading what your PDF:

Victor Porton said:

It is simpler than you can imagine: proving provability of invertibility of an algorithm is clearly an NP-complete problem. To solve it I just enumerate and run parallel all algorithms.

Why is that NP-complete, especially in an arbitrary formal system? It’s obvious that there are verifiable certificates for this problem, but that alone doesn’t restrict the problem to NP (let alone NP-complete); the certificate-checking must be polynomial in the size of the input.

In this case, the input is algorithm A, the certificate is a proof P that A is invertible, and the certificate-checker must check the proof against the formal system, in time polynomial in the size of A.

I don’t see why the size of P should be bound by the size of A, even informally.

view this post on Zulip Victor Porton (Apr 10 2021 at 13:14):

No, the input of the algorithm, whose NP-completeness we check is X, A processes this input X. An is an intermediary data not the input data, maybe you confuse that A is an input of V. It's really so, but we don't check if V is NP-complete, so that's irrelevant.

view this post on Zulip Paolo Giarrusso (Apr 11 2021 at 10:34):

Well, I wasn't using the symbols in the paper...

view this post on Zulip Paolo Giarrusso (Apr 11 2021 at 10:35):

My point was just, it's not clear to me that "proving provability of invertibility of an algorithm is clearly an NP-complete problem"

view this post on Zulip Paolo Giarrusso (Apr 11 2021 at 10:39):

in fact, I'm skeptical that problem is in NP: I don't think the size of the certificate is polynomial in the input algorithm (nevermind the proof of completeness)

view this post on Zulip Paolo Giarrusso (Apr 11 2021 at 10:39):

See for instance the 2nd def. in https://en.wikipedia.org/wiki/NP_(complexity)#Formal_definition — the 2nd clause demands that the size of the certificate is polynomial.

view this post on Zulip Paolo Giarrusso (Apr 11 2021 at 11:17):

To be more specific, the paper says this work applies to any formal system — but it's surprising if that applies to the standard presentation of first-order logic. That logic doesn't have cut, hence proof size is blown up exponentially (see e.g. https://en.wikipedia.org/wiki/Cut-elimination_theorem#Consequences_of_the_theorem and the linked https://scholar.google.com/scholar?hl=en&q=Don%27t+Eliminate+Cut+boolos&btnG=&lr=lang_de%7Clang_en%7Clang_it).

view this post on Zulip Victor Porton (Apr 12 2021 at 10:09):

Paolo Giarrusso said:

in fact, I'm skeptical that problem is in NP: I don't think the size of the certificate is polynomial in the input algorithm (nevermind the proof of completeness)

It' spolynomial, because the NP-complete (by theorem assumption) algorithm B generates a polynomial-size certificate.

view this post on Zulip Paolo Giarrusso (Apr 12 2021 at 19:19):

Is B is producing proofs in FOL without cut? Those can't be polynomial, so maybe some assumption is unsatisfiable (maybe like https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Possible.20polynomial.20NP-complete.20solution/near/233896533, but I'm not sure if my question is on the same point)

view this post on Zulip Paolo Giarrusso (Apr 12 2021 at 19:24):

  1. On the formalism, in fact, I already struggle seeing whether at page 1 that X is an NP ⇒ R(X) actually follows: X in NP does not imply that X produces a formal proof in our chosen formal system, while R(X) does.

view this post on Zulip Paolo Giarrusso (Apr 12 2021 at 19:26):

  1. also, I'm not convinced by the definition of NP. IIUC, you say that X is NP if and only if ∀ Y, X(Y) = Z ⇒ ∃polynomial-time algorithm X' : X' (Z) = Y.. However, X in NP seems closer to ∃polynomial-time algorithm X': ∀ Y, X(Y) = Z ⇒ X' (Z) = Y., which is strictly stronger.

view this post on Zulip Paolo Giarrusso (Apr 12 2021 at 19:30):

On 1, the first problem seems that FOL certificates might be exponentially bigger than the actual certificates for NP completeness. The second is that R seems to demand X to produce not just a certificate, but a proof of correctness of itself — possibly on all inputs depending on the actual statement ("for every algorithm Y" means "∀ Y" but I can't guess where that goes, relative to all other quantifiers described informally)


Last updated: Feb 04 2023 at 22:29 UTC