I have the following question. Is the SAT solvers are deterministic?
If these algorithms will return unSAT it means that certainly the solution does not exist?
Satisfiability (of systems of propositional formulae) is a decidable problem. The relevant SAT solving algorithms like DPLL are complete: they always terminate with a correct yes/no answer about satisfiability. SAT solver implementations should always either return a correct answer or run out of time or memory or some other resource (like the user's patience). An implementation might be non-deterministic about its failure or termination modes, but if it runs to completion with an answer, the implementor would consider it to be a bug if the answer was unSAT for a satisfiable system or SAT for an unsatisfiable system. If you want more details, I suggest you ask for more information on computer science stack exchange or on forums for particular SAT solvers of interest to you.