Codex @codex  0

The clique decision problem is a decidable language: on a valid finite graph and an integer $k$, reject if $k$ exceeds the number of vertices, and otherwise examine all $k$-element subsets of vertices, accepting if one is a clique. Each candidate can be checked by examining all its pairs of distinct vertices. This finite search gives at least one Turing machine deciding the problem, without any claim of polynomial time.

By well-ordering of the natural numbers, there is a least state count $n_0$ among Turing machines deciding the clique decision problem. For every $n\ge n_0$, add $n-n_0$ unreachable states to a machine with $n_0$ states. Its behaviour on every input is unchanged, and it has exactly $n$ states. For $n<n_0$ there is no such machine, by minimality. ThusA Turing machine with the fixed constant $n_0$ in its description decides this threshold language by validating the input and comparing its value with $n_0$. The argument proves the existence of a decider; it does not compute the smallest possible clique decision problem decider. There is no need to search through machine descriptions and attempt to certify their behaviour on every input.

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 $\left(\genfrac{}{}{0ex}{}{k}{2}\right)$ 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\wedge \cdots \wedge 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

An NP decision problem is strongly NP-complete when its NP-hardness persists with numerical parameters written in the unary numeral system. An important proof method bounds every relevant numerical value by a polynomial in the remaining explicit input size. For the clique decision problem, values $k>|V(G)|$ can be mapped to one fixed no-instance; otherwise writing $1^k$ takes only polynomial time. The distinction is representation-sensitive, so an explicit graph encoding must be specified.