Improving Cook's generic reduction for Clique to SAT?

Question

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.)

Answer 1

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 < 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.