Disjunction Clauses: A finite collection of literals connected by disjunction $\lor$ (Most Common);
Conjunction Clauses: A finite collection of literals connected by conjunction $\land$ (Less Common);
Conjunctive Normal Form (CNF): Conjunction of disjunction clauses;
I-B. Boolean Satisfiability Problem (SAT)
General SAT:
Input: A CNF; (To check: whether the boolean formula has to be a CNF)
Output: Whether there exists an interpretation satisfying this CNF.
$k$-SAT:
Constraints: Each clause in the input CNF contains $k$ literals.
Cook-Levin Theorem:
SAT is NP-complete.
2-SAT:
A 2-literal clause $x\lor y$ is equivalent to the conjunction of implications $x \rightarrow \bar{y} \lor y \rightarrow \bar{x}$. Therefore, a 2-SAT CNF can be reprensted by a directed graph. Therefore, the 2-SAT problem is equivalent to check whether there exists a path $x \rightsquigarrow \bar{x}$ and $\bar{x} \rightsquigarrow x$ for all the literals $x$. We finally have 2-SAT <= Reachability and 2-SAT is in P.
II. Proof (k-SAT <= 3-SAT)
3-literal clauses are non-trivial and can not be represented by implications. As metioned above, Any $k$-SAT can be reduced to 3-SAT. In the following part, we are going to prove that $k$-literal clause can be transformed to 3-literal clause [2]. All the details can be found in the reference [2].
$C^{\prime}$ is not equivalent to for arbitrary interpretations of $z$'s. However, we can prove that: $C$ can be satisfied if and only if if $C^{\prime}$ can be satisfied.
Conclusions:
We can not only prove that $k$-SAT<=3-SAT. We can also prove that SAT <= 3-SAT. The reverse direction 3-SAT <= SAT is trivial.
SciCodePhy
commented
2 months ago
Reduce k-SAT to 3-SAT (Version-I)
I. Definitions and Background
I-A. Boolean Algebras
I-B. Boolean Satisfiability Problem (SAT)
General SAT:
$k$-SAT:
Cook-Levin Theorem:
2-SAT:
A 2-literal clause $x\lor y$ is equivalent to the conjunction of implications $x \rightarrow \bar{y} \lor y \rightarrow \bar{x}$. Therefore, a 2-SAT CNF can be reprensted by a directed graph. Therefore, the 2-SAT problem is equivalent to check whether there exists a path $x \rightsquigarrow \bar{x}$ and $\bar{x} \rightsquigarrow x$ for all the literals $x$. We finally have 2-SAT <= Reachability and 2-SAT is in P.
II. Proof (k-SAT <= 3-SAT)
3-literal clauses are non-trivial and can not be represented by implications. As metioned above, Any $k$-SAT can be reduced to 3-SAT. In the following part, we are going to prove that $k$-literal clause can be transformed to 3-literal clause [2]. All the details can be found in the reference [2].
Given an arbitrary literal $l$, we have:
$$ l = \left(l \vee z_1 \vee z_2\right)\land \left(l \vee \overline{z_1} \vee z_2\right) \land \left(l \vee z_1 \vee \overline{z_2}\right) \land \left(\ell \vee \overline{z_1} \vee \overline{z_2}\right), $$
where $z_1$ and $z_2$ are two dummy variables.
$$ l_1\lor l_2 = \left(l_1 \vee l_2 \vee z_1\right) \land \left(l_1 \vee l_2 \vee \overline{z_1}\right) $$
where similarly $z_1$ is a dummy variable.
For $C =l_1 \lor l_2 \cdots l_k$, we can introduce $k-3$ dummy variables to generate a new CNF:
$$ C^{\prime}=\left( l_1 \lor l_2 \lor z_1 \right) \land \left( l_3 \lor \bar{z_1} \lor z_2 \right) \land \left( l_4 \lor \bar{z_2} \lor z_3 \right) \land \cdots \land \left( lm \lor \bar{z{m-2}} \lor z{m-1} \right) \land \cdots \land \left( l{k-2} \lor \bar{z{k-4}} \lor z{k-3} \right) \land \left( l{k-1} \lor l{k} \lor \bar{ z_{k-3} } \right) $$
$C^{\prime}$ is not equivalent to for arbitrary interpretations of $z$'s. However, we can prove that: $C$ can be satisfied if and only if if $C^{\prime}$ can be satisfied.
Conclusions:
We can not only prove that $k$-SAT<=3-SAT. We can also prove that SAT <= 3-SAT. The reverse direction 3-SAT <= SAT is trivial.
III. References
Core References:
Other References: