Algorithme dont le temps de fonctionnement dépend de P vs. NP

Existe-t-il un exemple connu et explicite d'un algorithme avec la propriété telle que si $P\neq NP$ alors cet algorithme ne s'exécute pas en temps polynomial et si $P=NP$ alors il s'exécute en temps polynomial?

Si vous supposez que $P=^?NP$ est prouvable en PA (ou ZFC), un exemple trivial est le suivant:

Input: N   (integer in binary format)
For I = 1 to N do
begin
  if I is a valid encoding of a proof of P = NP in PA (or ZFC)
    then halt and accept
End
Reject

Un autre exemple - moins trivial - qui ne repose sur aucune hypothèse est le suivant:

Input: x   (boolean formula)
Find the minimum i such that
  1) |M_i| < log(log(|x|))  [ M_1,M_2,... is a standard fixed TM enumeration] 
  2) and  M_i solves SAT correctly 
       on all formulas |y| < log(log(|x|))
          halting in no more than |y|^|M_i| steps
          [ checkable in polynomial time w.r.t. |x| ]
  if such i exists simulate M_i on input x 
      until it stops and accept/reject according to its output
      or until it reaches 2^|x| steps and in this case reject;
  if such i doesn't exist loop for 2^|x| steps and reject.

Si $P =NP$ l'algorithme trouvera tôt ou tard - supposons sur l'entrée $x_0$ - trouver l'index du temps polynomial de Turing (ou une version rembourrée de celui-ci) $M_{SAT}$ qui résout SAT en $O( |x| ^ { |M_{SAT}| })$ et pour toutes les entrées supérieures à $x_0$ continuera de le simuler et s'arrêtera en temps polynomial (notez que l'étape 2 peut également être vérifiée en temps polynomial). En d'autres termes, si $P = NP$ l'algorithme résout SAT en temps polynomial sur tout sauf un nombre fini d'instances.

Si $P \neq NP$ l'algorithme s'exécute en temps exponentiel.