Improving Cook's generic reduction for Clique to SAT?
You can express $k$-clique as a SAT instance with $O(nk)$ variables and $O(nk^2)$ clauses.  For fixed $k$, this is linear in $n$.

Let $x_{iv}=1$ if $v$ is the $i$th vertex in the clique (by lexicographically sorted order).  In other words, $x_i$ is a "one-hot" encoding of the $i$th vertex in the clique (it is the characteristic vector for a set with one element).  This introduces $nk$ variables.

Now for each $(i,j)$ you can enforce that the corresponding two vertices are connected by an edge, using $n$ clauses.  e.g., one clause is $(\neg x_{iu} \lor x_{jv_1} \lor \dots \lor x_{jv_m})$ where $v_1,\dots,v_m$ are the vertices that are adjacent to vertex $u$.  You get one clause per vertex $u$.  This introduces a total of $O(nk^2)$ clauses.

For each $i$, you can enforce that $x_i$ is a vector of Hamming weight 1 and that $x_i &lt; x_{i+1}$, using $O(n)$ clauses.  This adds a total of $O(nk)$ more clauses.



It might be possible to do better by using $k \lg n$ variables to represent the vertices in the clique ($\lg n$ bits suffice to represent the $i$th vertex in the clique) and then building a circuit to check whether a set of $k$ vertices correspond to a clique.  One approach to build such a circuit might be by constructing the list of all $k(k-1)/2$ pairs of these vertices, in sorted order, then comparing that to the list of edges using the Merge procedure from Mergesort, or something like that.  It might be possible to get something like a $O((n+m+k^2) \text{poly}(\lg n))$-size circuit, which then translates to a SAT instance of the same size (where $m = $ the number of edges in the graph).  I haven't tried to work out the details to see whether it's actually possible, though.