I am interested in reducing $k$-Clique to SAT without making the instance much larger.
Clique is in NP so it can be reduced to SAT using logarithmic space. The straightforward Garey/Johnson textbook reduction blows up the instance to cubic size. However, $k$-Clique is in P for every fixed $k$ so there "ought" to be an efficient reduction at least for fixed $k$.
One way to build the reduction is by using the SAT variables as a characteristic vector, with a variable that is set to true indicating that the associated vertex is in the clique. This reduction is natural but creates a SAT instance of quadratic size if the graph is sparse. For a sparse graph, quadratically many clauses are required to enforce that in every pair of non-adjacent vertices at most one vertex may be in the clique.
Let's try to do better than $O(n^2)$.
The generic reduction of Cook/Schnorr/Pippenger/Fischer works by first taking a polynomially time-bounded NDTM that decides the language, simulating the NDTM by an oblivious DTM, simulating the oblivious DTM by a circuit, and then simulating the circuit by a 3-SAT instance. This creates a 3-SAT instance of size $O(t(n)\log t(n))$ if the NDTM time bound is $t(n)$. The log factor seems unavoidable due to overhead when simulating by an oblivious machine. For $k$-Clique one seems to have $t(n) = O(nk)$, which yields a 3-SAT instance of $O(nk(\log n + \log k))$ size, which is quasilinear for fixed $k$. In his 1988 paper Cook asked whether a better generic reduction exists for languages in NP, and as far as I know this is still open. However, Clique has a lot of structure so perhaps one can do better in this case.
Is there a better reduction known from Clique to SAT?
In particular, is it possible for fixed $k$ to reduce $k$-Clique to SAT while keeping the increase in instance size linear? Or can one use an existing result to argue that this is unlikely to be possible? I have tried using Fortnow/Santhanam and Dell/van Melkebeek but the overheads seem too large for these results to imply anything specific.
(I have been working with a reduction that seems to avoid the log factor, but before wasting more time on the gory details to verify its correctness, I'd like to know if such a reduction is already known, or if it is unlikely to exist.)