A Variation of Levin Search for All Well-Defined Problems

In 1973, L.A. Levin published an algorithm that solves any inversion problem $\pi$ as quickly as the fastest algorithm $p^*$ computing a solution for $\pi$ in time bounded by $2^{l(p^*)}.t^*$, where $l(p^*)$ is the length of the binary encoding of $p^*$, and $t^*$ is the runtime of $p^*$ plus the time to verify its correctness. In 2002, M. Hutter published an algorithm that solves any well-defined problem $\pi$ as quickly as the fastest algorithm $p^*$ computing a solution for $\pi$ in time bounded by $5.t_{p}(x)+d_p.time_{t_{p}}(x)+c_p$, where $d_p=40.2^{l(p)+l(t_{p})}$ and $c_p=40.2^{l(f)+1}.O(l(f)^2)$, where $l(f)$ is the length of the binary encoding of a proof $f$ that produces a pair $(p,t_p)$, where $t_p(x)$ is a provable time bound on the runtime of the fastest program $p$ provably equivalent to $p^*$. In this paper, we rewrite Levin Search using the ideas of Hutter so that we have a new simple algorithm that solves any well-defined problem $\pi$ as quickly as the fastest algorithm $p^*$ computing a solution for $\pi$ in time bounded by $O(l(f)^2).t_p(x)$.