*P=NP but the proof will be nonconstructive and have a large constant.*

Large constant could happen.

If by nonconstructive they mean not practical, then yes, that could happen.

The following does not quite show it can't happen but it does give one pause: an old result of Levin's shows that there is a program you could write NOW such that if P=NP then this program decides SAT

**except for a finite number of formulas**(all of which are NOT in SAT) and can be proven to work in poly time (I will later give three pointers to proofs). The

**finite number of formulas**is why the people above may still be right. But only a finite number- seems like a weak kind of nonconstructive.

Since I am teaching crypto I wondered about Factoring. An old result of Gasarch (I proved it this morning -- I am sure it is already known) shows that there is a program you could write NOW such that if Factoring is in P then this program factors a number ALWAYS (none of this

**finite exception**crap) and can be proven to work in poly time. Even so, the algorithm is insane. If someone thought that factoring in P might be nonconstructive, my construction disproves it in such an absurd way that the notion that factoring could be in P nonconstructively should be taken seriously but not literally. There should be a way to say formally:

*I believe that FACTORING is in P but any poly-time algorithm is insane (not even looking at the constants) and hence could never be implemented.*

Not sure how to define insane.

Three pointers:

Stack Exchange TCS: here

Wikipedia: here

My slides (also include factoring result): here

**Question:**Can the SAT result be improved to be an algorithm that is ALWAYS right? Is there a way to show that it can't be (unless, say P=NP).

**Question**: What can be said about Graph Isomphism in this context? The proof for SAT is easily adpated to this case (all we used about SAT was that it was self-reducible). But can we get our GI algorithm to never make a mistake?

Are you user2925716?

ReplyDeleteHuh! No!

ReplyDeleteI bet P!=NP and furthermore the proof will be trivial. :-)

I think that Q1 is equivalent to proving P=NP:

ReplyDeleteP=NP is equivalent to Exists P -> polytime(P) AND forall x . P(x) = SAT(x)

So what we are trying to prove is that for a particular concrete A :

Exists P -> polytime(P) AND forall x . P(x) = SAT(x) -> polytime(A) AND forall x . A(x) = SAT(x)

Which is equivalent to prove:

NOT [ polytime(A) AND forall x . A(x) = SAT(x) ] OR Exists P -> polytime(P) AND forall x . P(x) = SAT(x)

but we want [ polytime(A) AND forall x . A(x) = SAT(x) ] = True (Q1) so we must prove P=NP

Typo:

Delete... Exists P -> polytime(P) .... should be

... Exists P . polytime(P) ... (. read as "such that")

Why do you say that "X -> Y" would be equivalent to "NOT Y OR X"?

DeleteMy mistake! it's equivalent to NOT x OR y :-)

DeleteIt's equivalent to prove

P <> NP OR [polytime (A) and A=SAT]

I don't understand the "(all of which are NOT in SAT)" part. Whenever the program fails, it claims that the given formula is not satisfiable. (Otherwise it provides a valid witness, and hence doesn't fail.) I don't understand why you claim that such a formula would be NOT in SAT. Isn't it the other way around?

ReplyDeleteIn factorization you can use the polynomial time prime algorithm to detect the bad answers and correct them searching exaustively for their factors (and if factoring is in P you need to do this only on a finite number of "bad algorithms" that behaved well on smaller numbers). In a similar fashion

ReplyDelete***under the assumption (much? stronger than P=NP) that Frege (or Extended Frege) systems are polynomially bounded proof systems***

then the following algorithm solves SAT correctly and runs in polynomial time:

Given a formula x, find the smallest i < log log |x| such that M_i outputs a satisfying assignment on all satisfiable formulas y of length |y| < log log |x| or a valid Frege unsatisfiability proof on all unsatisfiable formulas (in both cases running at most for |y|^|M_i| steps). Then run M_i on x for at most |x|^|M_i| steps; check (in polynomial time) the satisfying assignment or the correctness of then Frege unsatisfiability proof; if the assigment or the proof are not correct (or there is no M_i that satisfies the above condition) then check exhaustively (exponentially) whether x is in SAT or not.

If I understand your assumption correctly, the poly boundedness of a proof system for tautologies only implies NP=CoNP (There is an oracle A such that P\neq NP, but NP=CoNP with respect to A, hence it seems that the poly boundedness does not imply P=NP if we assume relativizable proofs.)

DeleteYou're right; it works if we add also the P=NP assumption.

DeleteI don't understand the claim about the finite number of exceptions:

ReplyDelete- Any algorithm deciding SAT could also be used to output a satisfying assignment when the instance is satisfiable. So it seems that the only way to fail would be to claim an instance is unsatisfiable when in fact it is.

- If the algorithm has a finite number of instances where it is wrong, couldn't those be hard-coded into the algorithm? Or would that count as non-constructive?

> So it seems that the only way to fail would be to claim an instance is unsatisfiable when in fact it is

DeleteYes.

> ... Or would that count as non-constructive?

Yes. It would be constructive if you explicitly write those hard-coded instances (or, alternatively, you could give the explicit x_0 such that for all instances >= x_0 the algorithm solves it correctly "without patches")

... More on the first point:

Delete- if the algorithm (that behaves well on small instances) outputs a satisfying assignment then you can check it (and "patch" it if is not valid)

- if it outputs "unsatisfiable" then you must "trust" it (otherwise you'll patch it infinitely many times)

So the explicit algorithm can output "unsatisfiable" on some satisfiable instances (finitely many if P=NP).

Another (trivial) assumption + algorithm is the following:

ReplyDelete* Assume that if P=NP we can build a polynomial time algorithm for SAT which is provably correct (in PA or ZFC)

Let M1,M2,... be a standard TM enumeration;

P1,P2,... a standard PA proof enumeration;

. On input x (a boolean formula):

. for i = 1 to |x| do

... for j = 1 to i do

..... if Pi is a valid proof that Mj solves SAT in polynomial time

....... then simulate Mj(x) and accept/reject according to it

. If no proof is found solve SAT(x) using an exhaustive search