Deterministic SAT solver
Core algorithms like DPLL and its refinements like CDCL are completely deterministic. 

Note that non-determinism doesn't necessarily mean that an algorithm may lead to a wrong result. For example we can distinguish between


Monte Carlo algorithms, which are randomised algorithms whose output may be incorrect with some probability.
Las Vegas algorithms, which are are randomised algorithms whose output  is always correct, but the algorithms 'gamble' with the resources used in the computation, e.g. running time on identical inputs may vary.


At the other extreme are probabilistic algorithms for solving $k$-SAT such as Sch&ouml;ning's [ 1 ] which is Monte-Carlo, and remarkably effective in practise given its utter simplicity. Interestingly Sch&ouml;ning's algorithm can be completely derandomised without losing (much of) its effectiveness [ 2 ].

In practise, industrial SAT-solvers always employ some degree of randomness, so as to 'escape' from the bad (= exponential) worst-case behaviour of DPLL-based algorithms.  MiniSat is a highly configurable and evolving piece of software. That said, MiniSat is not completely deterministic: the choice of branching variable is sometimes randomised, depending on command line options. (The default is that  2% of branching variables are chosen randomly IIRC.) Likewise, MiniSAT has the option of initialising the VSIDS scores randomly. (VSIDS is a heuristic for 'measuring' the influence a variable has.)





U. Schöning, A Probabilistic Algorithm for $k$-SAT Based on Limited
Local Search and Restart.
R. A. Moser, D. Scheder, A Full Derandomization of Sch&ouml;ning's
$k$-SAT Algorithm.