  This paper provides a characterization of call-by-value solvability using
call-by-value multi types. Our work is based on Accattoli and Paolini's
characterization of call-by-value solvable terms as those terminating with
respect to the solving strategy of the value substitution calculus, a
refinement of Plotkin's call-by-value $\lambda$-calculus. Here we show that the
solving strategy terminates on a term $t$ if and only if $t$ is typable in a
certain way in the multi type system induced by Ehrhard's call-by-value
relational semantics. Moreover, we show how to extract from the type system
exact bounds on the length of the solving evaluation and on the size of its
normal form, adapting de Carvalho's technique for call-by-name.
