# 3sat to clique reduction program

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

https://www.geeksforgeeks.org/maximal-clique-problem-recursive-solution/

https://www.geeksforgeeks.org/find-all-cliques-of-size-k-in-an-undirected-graph/

But it is not converting 3sat problem.

Is there any algorithm to convert 3sat to clique ?

• 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). Commented Sep 26, 2023 at 13:03
• I know implementation but I want a code which do the reduction. please can you provide me code?
– user
Commented Sep 26, 2023 at 15:18

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:

Inputs:
- 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')


• thanks for the answer but is there any online code for the reduction ?
– user
Commented Sep 26, 2023 at 15:00
• 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. Commented Sep 26, 2023 at 17:02
• I've added the pseudocode of a possible implementation. Commented Sep 26, 2023 at 17:14