One assignment must satisfy the whole formula
For (p∨q)∧(¬p∨r), setting p and r true satisfies the formula regardless of q. Finding separate, incompatible assignments for individual clauses is insufficient: every occurrence of a variable shares one value. Satisfiability requires one successful assignment, whereas tautology requires all assignments.
A proposed assignment can be checked by evaluating the formula. Exhaustive enumeration also eventually terminates for finite propositional input, making SAT decidable. Potentially expensive search is distinct from the absence of any always-terminating decision algorithm.
Verification and completeness
SAT belongs to NP because a satisfying assignment has polynomial length and can be verified in polynomial time relative to the formula encoding. The Cook–Levin theorem also gives a polynomial-time reduction from every NP language to SAT, preserving yes-instances exactly. Both membership and hardness establish completeness.
One proof represents a verification computation as a circuit, introduces variables for gate values, constrains each local operation with clauses, and requires a true output. Auxiliary variables record intermediate results; the construction need not already know whether an accepting certificate exists.
Worst cases and structured instances
NP-completeness does not prove exponential time for every instance or make practical solvers useless. A polynomial-time algorithm for general SAT would imply P=NP, an unresolved question in the cited course. Encoding, constraint structure and search strategy affect concrete performance.
2-SAT and propositional Horn formulas admit polynomial-time methods, while general 3-SAT is already NP-complete. Applications also depend on faithful modeling: a satisfying assignment establishes consistency of encoded constraints, not every requirement left outside the model.