You are asking about the algorithmic complexity of verifying a SAT solution with m clauses. Obviously if n is fixed and small, you can verify any solution in O(1) time-- just use a lookup table! So, let's assume that n is fixed but too large for a lookup table. Your CNF formula can be written as a 3-SAT problem so any clause can be checked in constant time.
Assuming no redundant clauses, you have to visit every clause so you won't be able to do better than O(m).
As for how to actually check solutions, the way you do it is you'd assign values to the variables representing the hash input. Then all other variables in your CNF would be solved through propagation for a valid input (and propagate to a conflicting state for an invalid input). A SAT solver does this by keeping track of which literals remain that can satisfy each clause and when only one literal remains due to the others being assigned the other way, the one literal that remains must be in the solution (see "watched literals").
Knowing there is a solution is as hard (in a complexity theoretical sense) as finding one. If you can tell a formula is unsat, you can use that to find a solution: just assign each variable a value and if at any step that makes the problem UNSAT, invert your assignment. This takes X steps where X is the number of variables. So if you had a polynomial UNSAT finder for x variables, you'd have a polynomial time solution finder that's x times slower and so still polynomial time (just one degree higher).
