We consider Total Functional $\NP$ ($\TFNP$) search problems. Such problems are based on combinatorial principles that guarantee, through locally checkable conditions, that a solution to the problem exists in an exponentially-large domain, and have the property that any solution has a polynomial-size witness that can be verified in polynomial time. ... more >>>

Johnson, Papadimitriou and Yannakakis introduce the class $\PLS$ consisting of optimization problems for which efficient local- search heuristics exist. We formulate a type-2 problem $\iter$ that characterizes $\PLS$ in style of Beame et al., and prove a criterion for type-2 problems to be nonreducible to $\iter$. As a corollary, we ... more >>>

We present a new framework for the study of search problems and their definability in bounded arithmetic. We identify two notions of complexity of search problems: verification complexity and computational complexity. Notions of exact solvability and exact reducibility are developed, and exact $\Sigma^b_i$-definability of search problems in bounded arithmetic is ... more >>>