= Solution
The <clique decision problem> belongs to <NP>. First reject $k>|V(G)|$. Otherwise a <complexity certificate> lists $k$ distinct <vertices>. Check distinctness and test that each of the $\binom k2$ pairs is an <edge>. Under a conventional explicit <graph> encoding, the <complexity certificate> length and verification <time complexity> are <polynomial> in the <input> length. The early rejection is relevant when $k$ is given in the <binary numeral system>.
For <NP-hardness>, first transform a <SAT> instance into an equisatisfiable <conjunctive normal form> $F=C_1\land\cdots\land C_m$ of <polynomial> size using a <Tseitin transformation>. This step avoids the possibly exponential increase caused by distributing arbitrary <Boolean formulas> into <conjunctive normal form>. Introduce a fresh <Boolean variable> for each subformula, constrain it to have the connective's <truth value> using a constant number of <Boolean clauses>, and require the top variable to be true. A <Boolean valuation> of the original <Boolean variables> satisfies the original <Boolean formula> exactly when it extends to a <satisfying assignment> of these constraints.
Create one <vertex> for each occurrence of a <Boolean literal> in each <Boolean clause>. Join two such <vertices> by an <edge> exactly when they belong to different <Boolean clauses> and their <Boolean literals> are not a variable and its <logical negation>. Set $k=m$. There are at most as many <vertices> as <Boolean literal> occurrences and at most quadratically many <edges>, so this construction takes <polynomial time>.
If $F$ has a <satisfying assignment>, choose one true <Boolean literal> occurrence from each <Boolean clause>. No two selected <Boolean literals> are contradictory, so their $m$ <vertices> form a <clique>. Conversely, an $m$-<clique> contains at most one <vertex> from each <Boolean clause>, because there are no <edges> within a <Boolean clause>. It therefore selects exactly one occurrence from each of the $m$ <Boolean clauses>. The selected <Boolean literals> are pairwise noncontradictory, so assign their <Boolean variables> the indicated <truth values> and assign any other <Boolean variables> arbitrarily. This <Boolean valuation> satisfies every <Boolean clause>.
An empty <Boolean clause> gives no <vertex> in its group, correctly preventing an $m$-<clique>. An empty <logical conjunction> can instead be mapped to a fixed yes-instance, avoiding any convention about $k=0$. Malformed <SAT> descriptions can be mapped to a fixed no-instance. We have proved
$$
F\text{ satisfiable}\quad\Longleftrightarrow\quad
\langle G_F,m\rangle\in\mathrm{Clique},
\qquad
\boxed{\mathrm{Clique}\text{ is NP-complete}.}
$$
Back to article page