 Clique decision problem

Given an explicitly represented finite simple graph $G$ and a nonnegative integer $k$, decide whether $G$ contains a clique of size $k$. The problem is NP-complete. A polynomial-time many-one reduction from SAT first obtains conjunctive normal form by a Tseitin transformation, makes one vertex per Boolean literal occurrence, and joins noncontradictory occurrences from different Boolean clauses. A clique as large as the Boolean clause count is equivalent to a satisfying assignment.