tag:blogger.com,1999:blog-3722233.post3593116095045748693..comments2023-03-27T02:45:06.501-05:00Comments on Computational Complexity: If P=NP then we HAVE an alg for SAT.Lance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger14125tag:blogger.com,1999:blog-3722233.post-25774643377971321762018-11-02T16:50:55.815-05:002018-11-02T16:50:55.815-05:00Another (trivial) assumption + algorithm is the fo...Another (trivial) assumption + algorithm is the following:<br /><br />* Assume that if P=NP we can build a polynomial time algorithm for SAT which is provably correct (in PA or ZFC)<br /><br />Let M1,M2,... be a standard TM enumeration;<br />P1,P2,... a standard PA proof enumeration;<br /><br />. On input x (a boolean formula):<br />. for i = 1 to |x| do<br />... for j = 1 to i do<br />..... if Pi is a valid proof that Mj solves SAT in polynomial time<br />....... then simulate Mj(x) and accept/reject according to it<br />. If no proof is found solve SAT(x) using an exhaustive searchMarzio De Biasihttps://www.blogger.com/profile/18441670787376943932noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-38810687150805269072018-11-02T14:13:46.162-05:002018-11-02T14:13:46.162-05:00You're right; it works if we add also the P=NP...You're right; it works if we add also the P=NP assumption.Marzio De Biasihttps://www.blogger.com/profile/18441670787376943932noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-74388374840773616422018-11-01T12:56:11.937-05:002018-11-01T12:56:11.937-05:00If I understand your assumption correctly, the pol...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.) Erfan Khanikinoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-52475042134788397492018-11-01T11:23:07.672-05:002018-11-01T11:23:07.672-05:00My mistake! it's equivalent to NOT x OR y :-)...My mistake! it's equivalent to NOT x OR y :-)<br /><br />It's equivalent to prove<br /><br />P <> NP OR [polytime (A) and A=SAT]<br />Marzio De Biasihttps://www.blogger.com/profile/18441670787376943932noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-18453694619027109332018-10-31T12:38:40.705-05:002018-10-31T12:38:40.705-05:00... More on the first point:
- if the algorithm (...... More on the first point:<br /><br />- 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)<br />- if it outputs "unsatisfiable" then you must "trust" it (otherwise you'll patch it infinitely many times)<br /><br />So the explicit algorithm can output "unsatisfiable" on some satisfiable instances (finitely many if P=NP).<br /><br />Marzio De Biasihttps://www.blogger.com/profile/18441670787376943932noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-84038926811924920962018-10-31T12:29:31.222-05:002018-10-31T12:29:31.222-05:00> So it seems that the only way to fail would b...> So it seems that the only way to fail would be to claim an instance is unsatisfiable when in fact it is<br /><br />Yes.<br /><br />> ... Or would that count as non-constructive?<br /><br />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") Marzio De Biasihttps://www.blogger.com/profile/18441670787376943932noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-81910580377626549272018-10-30T20:41:08.242-05:002018-10-30T20:41:08.242-05:00I don't understand the claim about the finite ...I don't understand the claim about the finite number of exceptions:<br />- 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.<br /><br />- 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?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-11068788460748682862018-10-30T16:44:26.579-05:002018-10-30T16:44:26.579-05:00In factorization you can use the polynomial time p...In 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 <br /><br />***under the assumption (much? stronger than P=NP) that Frege (or Extended Frege) systems are polynomially bounded proof systems***<br /><br />then the following algorithm solves SAT correctly and runs in polynomial time:<br /><br />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.Marzio De Biasihttps://www.blogger.com/profile/18441670787376943932noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-63646817862288718312018-10-29T18:44:31.645-05:002018-10-29T18:44:31.645-05:00Why do you say that "X -> Y" would be...Why do you say that "X -> Y" would be equivalent to "NOT Y OR X"?Jakitohttps://www.blogger.com/profile/08235089048981338795noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-28561451399395732492018-10-29T18:37:03.405-05:002018-10-29T18:37:03.405-05:00I don't understand the "(all of which are...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?Jakitohttps://www.blogger.com/profile/08235089048981338795noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-7370808234988765072018-10-29T12:13:06.916-05:002018-10-29T12:13:06.916-05:00Typo:
... Exists P -> polytime(P) .... should ...Typo:<br /><br />... Exists P -> polytime(P) .... should be<br /><br />... Exists P . polytime(P) ... (. read as "such that")<br /><br /><br />Marzio De Biasihttps://www.blogger.com/profile/18441670787376943932noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-26988501651382174152018-10-29T08:36:12.336-05:002018-10-29T08:36:12.336-05:00I think that Q1 is equivalent to proving P=NP:
P=...I think that Q1 is equivalent to proving P=NP:<br /><br />P=NP is equivalent to Exists P -> polytime(P) AND forall x . P(x) = SAT(x)<br /><br />So what we are trying to prove is that for a particular concrete A :<br /><br />Exists P -> polytime(P) AND forall x . P(x) = SAT(x) -> polytime(A) AND forall x . A(x) = SAT(x)<br /><br />Which is equivalent to prove:<br /><br />NOT [ polytime(A) AND forall x . A(x) = SAT(x) ] OR Exists P -> polytime(P) AND forall x . P(x) = SAT(x)<br /><br />but we want [ polytime(A) AND forall x . A(x) = SAT(x) ] = True (Q1) so we must prove P=NPMarzio De Biasihttps://www.blogger.com/profile/18441670787376943932noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-695827498761785962018-10-29T06:16:42.910-05:002018-10-29T06:16:42.910-05:00Huh! No!
I bet P!=NP and furthermore the proof wil...Huh! No!<br />I bet P!=NP and furthermore the proof will be trivial. :-)<br /><br /><br />Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-27570345916068731322018-10-29T04:38:03.622-05:002018-10-29T04:38:03.622-05:00Are you user2925716?Are you user2925716?domhttps://www.blogger.com/profile/05790539025733385232noreply@blogger.com