We present a technique for checking instances of the satisfiability (SAT) problem based on a combination of the Davis-Putnam (DP) procedure and stochastic methods. We first use the DP procedure to some extent, so as to partition and reduce the search space. If the reduction does not lead to an answer, a stochastic algorithm is then used to search each subspace. This approach is proven to be efficient for several types of SAT instances. A parallel implementation of the method is described and some experimental results are reported.