I am searching for a program to convert 3sat to clique problem.

I tried following links



But it is not converting 3sat problem.

Is there any algorithm to convert 3sat to clique ?

  • $\begingroup$ If you're looking for a (polynomial-time) algorithm to convert an instance of 3-SAT to an instance of the decision version of CLIQUE (given a graph, decide whether there is a clique with $k$ vertices), then there is an easy polynomial-time reduction which I can sketch in an answer. If you're looking for an already-made implementation then I'm not aware of one (although it is straightforward to write from the reduction). $\endgroup$
    – Steven
    Commented Sep 26, 2023 at 13:03
  • $\begingroup$ I know implementation but I want a code which do the reduction. please can you provide me code? $\endgroup$
    – user
    Commented Sep 26, 2023 at 15:18

1 Answer 1


Let 3-SAT formula $\phi$ be $C_1 \wedge C_2 \wedge \dots \wedge C_m$, where $C_i$ is a clause consisting of the disjunction of three literals: $(\ell_i^1 \vee \ell_i^2 \vee \ell_i^3)$.

We can create an auxiliary graph $G$ as follows:

  • For each clause $C_i$ create three vertices $\ell_i^1, \ell_i^2, \ell_i^3$, i.e., one for each literal. And add all edges between them.
  • Add an edge between each pair of complementary literals. I.e., if $\ell_i^h$ and $\ell_j^k$ refer to the same variable but one literal is positive and the other is negated, then add the edge $(\ell_i^h, \ell_j^k)$.

Let $\overline{G}$ be the complement of $G$ (i.e., $\overline{G}$ has the same vertex set as $G$ and it contains an edge $e$ if and only if $e$ is not in $G$).

Claim: The 3-SAT formula $\phi$ is satisfiable if and only if $\overline{G}$ contains a clique of size $m$.

Proof ($\Longrightarrow$): Consider a truth assignment that satisfies $\phi$ and, for each clause $C_i$ choose a literal $\ell^*_i$ that is true according to such an assignment. Notice that the set $L = \{\ell^*_i \mid i=1,\dots,m\}$ contains exactly one literal per clause (by definition) and does not contain any pair of complementary literals (since they cannot both be true). Then $L$ is an independent set of size $m$ of $G$, which means that the subgraph induced by $L$ must be a clique of size $m$ in to complement $\overline{G}$ of $G$.

Proof ($\Longleftarrow$): Let $L$ be the vertices of a of size $m$ in $\overline{G}$ and notice that $L$ must be an independent set in $G$. Since no independent set of $G$ can contain two literals from the same clause (all literals from the same clause have an edge between them), and since there are exactly $m$ clauses, $L$ contains exactly one literal $\ell_i^*$ from each clause $C_i$. Moreover, this set of literals cannot contain any pair of complementary literals. Then you can find a satisfying assignment for $\phi$ by setting the variables according to the values of the literals in $L$. The "leftover" variables (if any) that do not correspond to any literal in $L$ can be set arbitrarily.

Here is the pseudocode of a possible implementation:

- the number m of triplets
- a list L of m triples. The generic j-th element of the i-th triple, denoted by L[i][j], contains either the index k>=1 of a variable to encode the positive literal on the k-th variable, or -k to encode the negated literal

Output: the list of edges of the graph resulting from the above reduction. The vertices of the graph are integers from 1 to 3m. The j-th literal of the i-th clause is vertex (i-1)*3+j.

For i = 1,2,...,m-1:
   For i' = i+1, i+2,....,m:
      For j = 1,2,3:
         For j' = 1,2,3:
            If L[i][j] != -L[i'][j']:
                Output the edge ((i-1)*3 + j, (i'-1)*3 + j')
  • $\begingroup$ thanks for the answer but is there any online code for the reduction ? $\endgroup$
    – user
    Commented Sep 26, 2023 at 15:00
  • $\begingroup$ As I said I'm not aware of any readily made implementation. However it should be quite simple to implement the above reduction. You just need to add edges of a graph expect those between two literals that are complementary or belong to the same clause. $\endgroup$
    – Steven
    Commented Sep 26, 2023 at 17:02
  • $\begingroup$ I've added the pseudocode of a possible implementation. $\endgroup$
    – Steven
    Commented Sep 26, 2023 at 17:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.