Verifying a satisfying assignment (source code)

= Verifying a satisfying assignment
{title2=$O(n+m+L)$}

For a <CNF> input with $n$ <Boolean variables>, $m$ <Boolean clauses>, and $L$ <Boolean literal> occurrences, first check that the supplied <Boolean valuation> gives each input <Boolean variable> exactly one <truth value>. Evaluate each <Boolean literal> by lookup or <logical negation>, each <Boolean clause> by <logical disjunction>, and the <Boolean formula> by <logical conjunction>. Indexed <Boolean variables> and constant-cost lookups give an $O(n+m+L)$ operation count; with a finite <binary string> encoding the check still takes <polynomial time>. Thus a <satisfying assignment> is a <certificate in computational complexity> for <SAT>, proving that <SAT> belongs to <NP>. Finding it by exhaustive checking can require $2^n$ candidate <Boolean valuations>; this enumeration cost is not a lower bound on every possible <SAT> <algorithm>.<CS 252, Lecture 8: Constraint Satisfaction Problems (Carnegie Mellon University)>[CS 252, Lecture 8: Constraint Satisfaction Problems, p. 3, §3 opening paragraph: assignments as certificates and membership in NP]{ref}