How efficient are DPLL-based SAT-solvers on satisfiable instances of PHP? We know that DPLL based SAT-solvers fail to answer correctly on unsatisfiable instances of $\mathrm{PHP}$ (pigeon hole principle), e.g. on "there is a injective mapping from $n+1$ to $n$":

$$\mathrm{PHP^{n+1}_{n}} := \left(\bigwedge_{i\in[n+1]} \ \bigvee_{j\in[n]} \ p_{i,j}\right) \wedge \left(\bigwedge_{i\neq i'\in[n+1]} \ \bigwedge_{j\in[n]} \ (\lnot p_{i,j} \vee \lnot p_{i',j})\right)$$

I am looking for results about how they perform on satisfiable instances of $\mathrm{PHP}$, e.g. on "there is a injective mapping from $n$ to $n$". 

Do they find a satisfying assignment quickly on such instances?
On satisfiable instances of $PHP$, DPLL based SAT solvers will furnish a satisfying assignment in linear time.

To see why, observe how the CNF encoding of an unsatisfiable instance of $PHP$ with $n$ holes and $n + 1$ pigeons is sintactically identical to an instance of $k = n$ Graph Coloring, where the input graph is a clique of $n + 1$ vertices. 

Similarly, the CNF encoding of a satisfiable instance of $PHP$ with $n$ holes and $n$ pigeons is sintactically identical to an instance of $k = n$ Graph Coloring, where the input graph is a clique of $n$ vertices.

Now, coloring a clique of $n$ vertices with $n$ colors is straightforward: scan the vertices, and assign to each of them one of the remaining colors (already assigned colors are automatically ruled out by the clique-ness of the graph, using unit propagation). Whatever of the remaining colors you choose, it will be good and will lead you to a satisfying assignment.

From the DPLL solver point of view: each time it will try to guess the boolean value of a variable $v_i$, such value will be right (whatever it is), because there will certainly be a satisfying assignment in which variable $v_i$ has the guessed value. Unit propagation will do the rest of the job, by guiding the solver along the satisfying path (in other words: by preventing it to guess wrong values).

The search then proceeds one variable after the other, linearly, each time making the correct guess.