patternModerate
Reduction 3SAT and CLIQUE
Viewed 0 times
andreductionclique3sat
Problem
Hello everyone this is my first question ever and I apologize if I ask in the wrong manner causing this post to be either closed or deleted. I'm learning Reductions and my professor has asked us to write a paper on reductions (3SAT)
When doing the Reduction from the Clique Problem to 3SAT, I understand that we make clauses and every clause contains 3 literals (hence, 3SAT) but my problem comes when choosing what literals and why they choose them. How do I know which literals to choose? So I know that in every clause I'll have x1, x2 and x3, but how do I choose their assignment order? In one clause I have (x1 or x2 or x3) and in another I have (x1 or not x2 or not x3). How were these chosen?
Also, it seems they don't begin with a graph in mind already. What if I'm given a graph to begin with, how would I convert it into x1, x2, x3? If for clause I have 3 vertices, how would I assign them their respected boolean expression? Thank you very much
When doing the Reduction from the Clique Problem to 3SAT, I understand that we make clauses and every clause contains 3 literals (hence, 3SAT) but my problem comes when choosing what literals and why they choose them. How do I know which literals to choose? So I know that in every clause I'll have x1, x2 and x3, but how do I choose their assignment order? In one clause I have (x1 or x2 or x3) and in another I have (x1 or not x2 or not x3). How were these chosen?
Also, it seems they don't begin with a graph in mind already. What if I'm given a graph to begin with, how would I convert it into x1, x2, x3? If for clause I have 3 vertices, how would I assign them their respected boolean expression? Thank you very much
Solution
Here is one possible way to reduce Clique to SAT (you can then further reduce it to 3SAT). This type of reduction is often used in (propositional) proof complexity, an area of complexity theory.
Given a graph $G = (V,E)$ and a number $k$, we will have variables $x_{iv}$ for every $1 \leq i \leq k$ and every $v \in V$. You should think of $x_{iv}$ as stating that $v$ is the $i$th vertex in the clique. We want to encode the following constraints:
-
For each $i$, there is an $i$th vertex in the clique: $\bigvee_{v \in V} x_{iv}$.
-
For each $i,j$, the $i$th vertex is different from the $j$th vertex: for each $v \in V$, $\lnot x_{iv} \lor \lnot x_{jv}$.
-
For each non-edge $(u,v) \notin E$, $u,v$ cannot both belong to the clique: for each $i,j$, $\lnot x_{iu} \lor \lnot x_{jv}$.
You can think of the second constraint as a special case of the third one.
If we take all these clauses together, we get a CNF which states that "the $x_{iv}$ encode a $k$-clique in $G$". This CNF is satisfiable iff $G$ contains a $k$-clique.
If you want to get a 3CNF, all you need to do is to convert the constraints of the first kind into 3-clauses. There is a standard way to do this: if the vertices are $v_1,\ldots,v_n$, we replace $\bigvee_{v \in V} x_{iv}$ with
$$
x_{iv_1} \lor x_{iv_2} \lor y_{iv_2} \\
\lnot y_{iv_2} \lor x_{iv_3} \lor y_{iv_3} \\
\lnot y_{iv_3} \lor x_{iv_4} \lor y_{iv_4} \\
\ldots \\
\lnot y_{iv_{n-2}} \lor x_{iv_{n-1}} \lor x_{iv_n}
$$
Here the $y_{iv}$ are new variables. This set of clauses is equivalent to the original clause $x_{iv_1} \lor x_{iv_2} \lor \cdots \lor x_{iv_n}$.
Given a graph $G = (V,E)$ and a number $k$, we will have variables $x_{iv}$ for every $1 \leq i \leq k$ and every $v \in V$. You should think of $x_{iv}$ as stating that $v$ is the $i$th vertex in the clique. We want to encode the following constraints:
-
For each $i$, there is an $i$th vertex in the clique: $\bigvee_{v \in V} x_{iv}$.
-
For each $i,j$, the $i$th vertex is different from the $j$th vertex: for each $v \in V$, $\lnot x_{iv} \lor \lnot x_{jv}$.
-
For each non-edge $(u,v) \notin E$, $u,v$ cannot both belong to the clique: for each $i,j$, $\lnot x_{iu} \lor \lnot x_{jv}$.
You can think of the second constraint as a special case of the third one.
If we take all these clauses together, we get a CNF which states that "the $x_{iv}$ encode a $k$-clique in $G$". This CNF is satisfiable iff $G$ contains a $k$-clique.
If you want to get a 3CNF, all you need to do is to convert the constraints of the first kind into 3-clauses. There is a standard way to do this: if the vertices are $v_1,\ldots,v_n$, we replace $\bigvee_{v \in V} x_{iv}$ with
$$
x_{iv_1} \lor x_{iv_2} \lor y_{iv_2} \\
\lnot y_{iv_2} \lor x_{iv_3} \lor y_{iv_3} \\
\lnot y_{iv_3} \lor x_{iv_4} \lor y_{iv_4} \\
\ldots \\
\lnot y_{iv_{n-2}} \lor x_{iv_{n-1}} \lor x_{iv_n}
$$
Here the $y_{iv}$ are new variables. This set of clauses is equivalent to the original clause $x_{iv_1} \lor x_{iv_2} \lor \cdots \lor x_{iv_n}$.
Context
StackExchange Computer Science Q#70531, answer score: 12
Revisions (0)
No revisions yet.