<p>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$.</p>

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

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

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

<hr>

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

CC BY-SA 3.0
2015-12-07T06:20:12.710Z
2016-12-10T23:39:06.313Z
2016-12-10T23:39:06.313Z
D.W.
<p>I am interested in reducing $k$-Clique to SAT without making the instance much larger.</p>

<p>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 <em>cubic</em> size.
However, $k$-Clique is in P for every fixed $k$ so there "ought" to be an efficient reduction at least for fixed $k$.</p>

<p>One way to build the reduction is by <a href="https://cstheory.stackexchange.com/a/617">using the SAT variables as a characteristic vector</a>, 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 <em>quadratic</em> 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.</p>

<p>Let's try to do better than $O(n^2)$.</p>

<p>The generic reduction of <a href="http://dx.doi.org/10.1016/0020-0190(88)90152-4">Cook</a>/<a href="http://dx.doi.org/10.1145/322047.322060">Schnorr</a>/<a href="http://dx.doi.org/10.1145/322123.322138">Pippenger/Fischer</a> 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 <em>quasilinear</em> 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.</p>

<blockquote>
  <p>Is there a better reduction known from Clique to SAT?</p>
</blockquote>

<p>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 <a href="http://dx.doi.org/10.1016/j.jcss.2010.06.007">Fortnow/Santhanam</a> and <a href="http://dx.doi.org/10.1145/2629620">Dell/van Melkebeek</a> but the overheads seem too large for these results to imply anything specific.</p>

<p>(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.)</p>

CC BY-SA 3.0
2015-12-04T19:56:43.127Z
See a somewhat-related question http://mathoverflow.net/q/224898/440 on MathOverflow, in which the small size of a quantified Boolean formula for $k$-clique translates directly into the slow convergence rate of the 0-1 law for random graphs. The question already contains a formula of quadratic size; the accepted answer gives a linear-size formula that implies the existence of a $k$-clique, but that might be false even when a clique exists.
David Eppstein
CC BY-SA 3.0
2015-12-05T06:12:21.017Z
Do you want a reduction that runs in log space as well? Because as you point out, $k$-clique can be solved in polynomial time for constant $k$, so a polynomial time reduction can actually check for a $k$-clique and then output a *constant* sized SAT instance.
Joe Bebel
CC BY-SA 3.0
2015-12-05T21:35:02.840Z
@JoeBebel: with $k\log n$ space it is even possible to output a SAT instance with $k\log n$ variables, the solutions to which are all the locations of $k$-cliques in the graph.  For each potential clique, one outputs a clause forbidding that $k$-clique if it is not present.  This captures the solutions precisely, a one-one reduction, so answers Kaveh's question, but just as with your suggestion, solving the instance before deciding on how to reduce it seems like a cheat too far.
András Salamon
<cc.complexity-theory><sat><reductions><clique>
Improving Cook's generic reduction for Clique to SAT?
András Salamon
# Improving Cook's generic reduction for Clique to SAT?

(Asked by: username_0 on 2015-12-04)

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](https://cstheory.stackexchange.com/a/617), 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](http://dx.doi.org/10.1016/0020-0190(88)90152-4)/[Schnorr](http://dx.doi.org/10.1145/322047.322060)/[Pippenger/Fischer](http://dx.doi.org/10.1145/322123.322138) 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](http://dx.doi.org/10.1016/j.jcss.2010.06.007) and [Dell/van Melkebeek](http://dx.doi.org/10.1145/2629620) 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.)

**Tags:** cc.complexity-theory, sat, reductions, clique

> **Comments:**
> **username_1**: See a somewhat-related question http://mathoverflow.net/q/224898/440 on MathOverflow, in which the small size of a quantified Boolean formula for $k$-clique translates directly into the slow convergence rate of the 0-1 law for random graphs. The question already contains a formula of quadratic size; the accepted answer gives a linear-size formula that implies the existence of a $k$-clique, but that might be false even when a clique exists.  
> **username_2**: Do you want a reduction that runs in log space as well? Because as you point out, $k$-clique can be solved in polynomial time for constant $k$, so a polynomial time reduction can actually check for a $k$-clique and then output a *constant* sized SAT instance.  
> **username_0**: @JoeBebel: with $k\log n$ space it is even possible to output a SAT instance with $k\log n$ variables, the solutions to which are all the locations of $k$-cliques in the graph.  For each potential clique, one outputs a clause forbidding that $k$-clique if it is not present.  This captures the solutions precisely, a one-one reduction, so answers Kaveh's question, but just as with your suggestion, solving the instance before deciding on how to reduce it seems like a cheat too far.  

---

## 1 answers

### Answer by username_3 on 2015-12-07. Score: 10 | Accepted answer

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.


---

