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.