Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
I am looking for natural examples of efficient algorithms (i.e. in polynomial time) s.t.
I can make artificial examples myself. However I want interesting natural examples, i.e. algorithms studied for their own sake, not created just to answer this type of questions.
This is the same idea as Andrej's answer but with more details.
Krajicek and Pudlak [LNCS 960, 1995, pp. 210-220] have shown that if $P(x)$ is a $\Sigma^b_1$-property that defines primes in the standard model and $$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 < y_1, y_2 < x \land x = y_1y_2)$$ then there is a polynomial time factoring algorithm. This gives a bunch of examples since any NP algorithm for primality testing basically yields such a $\Sigma^b_1$ formula. In particular, the AKS primality test gives such a formula (when appropriately recast in the language of $S^1_2$). The paper by Krajicek and Pudlak gives more cryptography related examples of this kind but predates AKS and related advances by a few years.
This example is a bit lower in the hierarchy than what Kaveh asks for, but it is an open problem whether the soundness of the uniform $\mathrm{TC}^0$ algorithms for integer division and iterated multiplication by Hesse, Allender, and Barrington can be proved in the corresponding theory $\mathit{VTC}^0$.
The argument is pretty elementary, and there should be no problem formalizing it in $\mathit{TV}^0$, but with respect to $\mathit{VTC}^0$ it suffers from a chicken-and-egg problem: it makes heavy use of the very functions whose $\mathrm{TC}^0$-computability is furnished by the algorithm.
For another example, the Jacobi symbol $\left(\frac an\right)$ is polynomial-time computable, but its soundness in the form
if $p$ is an odd prime and $\left(\frac ap\right)=1$, then $a$ is a quadratic residue modulo $p$
is not provable in $S^1_2$ unless factoring can be done in probabilistic polynomial time, by the arguments here.
Another class of examples is given by irreducibility testing and factorization algorithms for polynomials (primarily over finite fields and over the rationals). These invariably rely on Fermat’s little theorem or its generalizations (among others), and as such are not known to be formalizable in an appropriate theory of bounded arithmetic. Typically, these algorithms are randomized, but for deterministic polynomial-time examples, one can take Rabin’s irreducibility test or the Tonelli–Shanks square-root algorithm (formulated so that a quadratic nonresidue is required as a part of the input).
The AKS primality test seems like a good candidate if Wikipedia is to be believed.
However, I would expect such an example to be hard to find. Existing proofs are going to be phrased so that they are obviously not done in bounded arithmetic, but they will likely be "adaptable" to bounded arithmetic with more or less effort (usually more).
