algorithm for checking satisfiability

Question

In order to prove that SAT is in NP, I need to come up with a polynomial time verfier (an algorithm). The Cooks Levin Theorem uses a non-deterministic Turing machine but that's not what I am looking for.

The idea of the algorithm could be that we put in the values and calculate the answer. Then, we check whether the answer is 1 or not. However, I am unable to understand how I could write a psuedocode for the 'putting in values' part and then show that it's polynomial for sure.

if x = 1:
 accept
else:
 reject

This could be in O(1). But what about the remaining part?

Answer 1

Here is how I would do it:

Algo: Verifier for DNF-SAT problem given as array of closures and a possible mapping of literals to booleans
Input:
Array of closures: [$C_1$,$C_2$,...,$C_m$]
where $C_j \subseteq \{x_1,...,x_n,\neg x_1, ... \neg x_n\}$
(Certificate) Array $M$ where $M_i$ is the boolean value of literal $x_i$
Output: true or false

for $i = 1$ to $m$:
  value = true
  for literal in $C_i$:
    if literal == $x_i$:
      value = value or $M[i]$:
    else if literal == $\neg x_i$:
      value = value or (not $M[i]$)
  if not value:
    return false
return true 

Note: the math notation is indented and commonly used in pseudocode sadly cs stackexchange doesn't support it