# What are the best known reductions from SAT to CNF-SAT?

Problems

• Let SAT denote the following problem:

Given a boolean formula, does there exist a satisfying assignment?

• Let CNF-SAT denote the following problem:

Given a boolean formula in conjunctive normal form, does there exist a satisfying assignment?

Note: CNF-SAT is more restrictive because it requires that the boolean formulas be in conjunctive normal form.

Parameters

Let's consider some parameters that we associate with a boolean formula. Let $n$ denote the number of variables and $m$ denotes the number of literal occurrences (or we could say the total size of the formula).

Question

Consider a polynomial time reduction that reduces a SAT instance $\phi$ with $n$ variables and $m$ literal occurrences to a CNF-SAT instance $\phi^{\prime}$ with $v(n,m)$ variables and $l(n,m)$ literal occurrences for some functions $v(n,m)$ and $l(n,m)$.

What are the best known bounds on $v(n,m)$ and $l(n,m)$?

As pointed out by qsp in the comments below, Tseytin transformation is a reduction where $v(n,m) = O(m)$ and $l(n,m) = O(m)$. However, does there exist a reduction where $v(n,m) = O(n \sqrt{m})$ and $l(n,m) = O(m^2)$? What about a reduction with $v(n,m) = O(n^2)$ and $l(n,m) = O(m^2)$?

Revised Question

Does there exist a polynomial time reduction with functions $f(n)$ and $g(m)$ such that:

• $l(n,m) = \mathrm{poly}(m)$

• $v(n,m) = f(n) \cdot g(m)$

• $g(m) = o(m)$

Any relevant references are greatly appreciated! Thank you.

• I do not see why you have a $\log(m)$. I take $m$ the size of the formula because it is easier to see this way. Isn't the usual reduction to 3-CNF linear in $m$? You introduce a fresh variable $z_v$ for each gate $v$ of your boolean formula (or circuit for this reduction) and express $z_v = z_{v_1} \oplus z_{v_2}$ with a 3-CNF if $\oplus$ is the label of $v$ and $v_1$, $v_2$ its children. With this reduction, you have a 3-CNF with $v(n,m) = O(m)$ and $l(n,m) = O(m)$. Right?
– holf
Mar 29, 2017 at 14:52
• Thank you very much for the comment. That sounds right. :) I will edit the question based on your comment. Mar 29, 2017 at 15:13
• The best known reduction to CNF-SAT is Tseytin transformation.
– sean
Mar 29, 2017 at 17:28
• @qsp Thank you very much for the comment!! Yep, that seems to be the best we can get in terms of formula size (or number of literal occurrences). But, are there any known reductions where we reduce the number of variables (say from $m$ to $n^2$), but increase the number of literal occurrences? Mar 29, 2017 at 18:38
• It seems one can reduce any $$NTIME(t(n))$$ computation on a multitape TM on an input of length $$n$$ to a CNF SAT instance on $$O(t(n))$$ variables and $$O(t(n)^{1+\varepsilon})$$ clauses each of width $$O(\log t(n))$$. For any $\varepsilon > 0$\$. That should say something about reductions to formulas... Mar 30, 2017 at 1:32