Algoritmos construtivamente eficientes, sem correção e prova de eficiência

Estou procurando exemplos naturais de algoritmos eficientes (isto é, em tempo polinomial) st

1. sua correção e eficiência podem ser comprovadas construtivamente (por exemplo, na ou na ), mas$PRA$$HA$
2. nenhuma prova usando apenas conceitos eficientes é conhecida (ou seja, não sabemos como provar sua correção e eficiência na ou ).S 1 $TV^0$$S^1_2$

Eu mesmo posso fazer exemplos artificiais. No entanto, quero exemplos naturais interessantes, ou seja, algoritmos estudados por eles mesmos, não criados apenas para responder a este tipo de perguntas.

Essa é a mesma idéia que a resposta de Andrej, mas com mais detalhes.

KRAJICEK e Pudlak [ LNCS 960, 1995, pp. 210-220 ] demonstraram que, se é uma Σ b 1 -property que define primos no modelo padrão e S 1 2 ⊢ ¬ P ( x ) → ( ∃ y 1 , y 2 ) ( 1 < y 1 , y 2 < x ∧ x = y 1 y 2$P(x)$$\Sigma^b_1$

$$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 < y_1, y_2 < x \land x = y_1y_2)$$ existe um algoritmo de fatoração de tempo polinomial. Isso fornece vários exemplos, já que qualquer algoritmo NP para teste de primalidade produz basicamente uma fórmula . Em particular, o teste de primalidade AKS fornece essa fórmula (quando reformulado adequadamente no idioma de S 1 2 ). O artigo de Krajicek e Pudlak fornece mais exemplos relacionados a criptografia desse tipo, mas antecede a AKS e os avanços relacionados em alguns anos.$\Sigma^b_1$$S^1_2$

$\mathrm{TC}^0$$\mathit{VTC}^0$

$\mathit{TV}^0$$\mathit{VTC}^0$$\mathrm{TC}^0$

$\left(\frac an\right)$

$p$$\left(\frac ap\right)=1$$a$$p$

$S^1_2$

Outra classe de exemplos é dada por algoritmos de teste de irredutibilidade e fatoração para polinômios (principalmente sobre campos finitos e sobre os racionais). Invariavelmente, eles se baseiam no pequeno teorema de Fermat ou em suas generalizações (entre outros) e, como tal, não são conhecidos por serem formalizáveis ​​em uma teoria apropriada da aritmética limitada. Normalmente, esses algoritmos são randomizados, mas para exemplos determinísticos de tempo polinomial, pode-se fazer o teste de irredutibilidade de Rabin ou o algoritmo de raiz quadrada de Tonelli-Shanks (formulado para que um não retorno quadrático seja necessário como parte da entrada).

O teste de primalidade da AKS parece ser um bom candidato para se acreditar na Wikipedia.

No entanto, eu esperava que esse exemplo fosse difícil de encontrar. As provas existentes serão redigidas para que obviamente não sejam feitas na aritmética limitada, mas provavelmente serão "adaptáveis" à aritmética limitada com mais ou menos esforço (geralmente mais).