Definition of SAT Problem
In computational complexity, we usually think of SAT as a decision problem: given a CNF, decide whether there is a truth assignment that satisfies it. There is also a search version of SAT: given a CNF, either find a satisfying assignment, or state that the formula is unsatisfiable. SAT solvers consider a third version: given a CNF, either find a satisfying assignment, or a proof that the formula is unsatisfiable.

There are several relations between the various versions. First, if you solve the decision version, you can also solve the search version. The idea is to find the lexicographically smallest satisfying assignment. Assuming that the variables are $x_1,\ldots,x_n$, we first substitute $x_1=0$ and check whether the resulting formula is still satisfiable. If so, we continue on to $x_2$. Otherwise, we substitute $x_1 = 1$ (the formula must remain satisfiable) and continue on to $x_2$. After $n-1$ more such steps we uncover a satisfying assignment.

Another relation is that if you can solve the search version that you can also solve the SAT solver version. The idea is that if the algorithm for the search version states that the CNF is unsatisfiable, then the transcript of the algorithm serves as proof that the CNF is indeed unsatisfiable. So these two versions are essentially equivalent.