<p><strong>Problems</strong></p>

<blockquote>
  <ul>
  <li>Let SAT denote the following problem:</li>
  </ul>
  
  <p>Given a boolean formula, does there exist a satisfying assignment?</p>
  
  <ul>
  <li>Let CNF-SAT denote the following problem:</li>
  </ul>
  
  <p>Given a boolean formula in conjunctive normal form, does there exist a
  satisfying assignment?</p>
</blockquote>

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

<p><strong>Parameters</strong></p>

<p>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).</p>

<p><strong>Question</strong></p>

<blockquote>
  <p>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)$.</p>
  
  <p>What are the best known bounds on $v(n,m)$ and $l(n,m)$?</p>
</blockquote>

<p>As pointed out by qsp in the comments below, <a href="https://en.wikipedia.org/wiki/Tseytin_transformation" rel="noreferrer">Tseytin transformation</a> 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)$?</p>

<p><strong>Revised Question</strong></p>

<blockquote>
  <p>Does there exist a polynomial time reduction with functions $f(n)$ and $g(m)$ such that:</p>
  
  <ul>
  <li><p>$l(n,m) = \mathrm{poly}(m)$</p></li>
  <li><p>$v(n,m) = f(n) \cdot g(m)$</p></li>
  <li><p>$g(m) = o(m)$</p></li>
  </ul>
</blockquote>

<p>Any relevant references are greatly appreciated!  Thank you.</p>

CC BY-SA 3.0
2017-03-29T14:52:22.277Z
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
CC BY-SA 3.0
2017-03-29T15:13:32.420Z
Thank you very much for the comment.  That sounds right.  :)  I will edit the question based on your comment.
Michael Wehar
CC BY-SA 3.0
2017-03-29T17:28:10.357Z
The best known reduction to CNF-SAT is Tseytin transformation.
sean
CC BY-SA 3.0
2017-03-29T18:38:22.633Z
@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?
Michael Wehar
CC BY-SA 3.0
2017-03-30T01:32:54.983Z
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...
Ryan Williams
CC BY-SA 3.0
2017-03-30T06:12:59.507Z
@RyanWilliams Thank you!  I really appreciate the comment.  :)  I was wondering, can we do any better if we bound the non-determinism.  For example, if the multitape TM runs for $t(n)$ time and only uses $n$ non-deterministic bits, could we reduce it to a CNF-SAT instance with $O(n)$ variables and $O(t(n)^{1 + \varepsilon})$ clauses?  For this approach to work, maybe we would also need to bound the space so that the TM runs for $t(n)$ time only using $n$ space and $n$ bits of non-determinism?  Or, maybe this just isn't possible given existing techniques.  Any thoughts are welcomed.
Michael Wehar
CC BY-SA 3.0
2017-03-30T14:56:35.413Z
Sorry that my previous comment (deleted) was a little overly optimistic in the result.  Although it's just a small step to finding a better reduction to CNF-SAT, for every $k$, I have a reduction that reduces a SAT instance with $n$ variables and $m$ literal occurrences to a SAT instance of weft $k+1$ with $n$ variables and $2^{k \cdot m^{\frac{1}{k}}}$ literal occurrences.
Michael Wehar
<cc.complexity-theory><np-hardness><sat><reductions><parameterized-complexity>
What are the best known reductions from SAT to CNF-SAT?
Michael Wehar
# What are the best known reductions from SAT to CNF-SAT?

(Asked by: username_0 on 2017-03-29)

**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](https://en.wikipedia.org/wiki/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.

**Tags:** cc.complexity-theory, np-hardness, sat, reductions, parameterized-complexity

> **Comments:**
> **username_1**: 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?  
> **username_0**: Thank you very much for the comment.  That sounds right.  :)  I will edit the question based on your comment.  
> **username_2**: The best known reduction to CNF-SAT is Tseytin transformation.  
> **username_0**: @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?  
> **username_3**: 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...  
> **username_0**: @RyanWilliams Thank you!  I really appreciate the comment.  :)  I was wondering, can we do any better if we bound the non-determinism.  For example, if the multitape TM runs for $t(n)$ time and only uses $n$ non-deterministic bits, could we reduce it to a CNF-SAT instance with $O(n)$ variables and $O(t(n)^{1 + \varepsilon})$ clauses?  For this approach to work, maybe we would also need to bound the space so that the TM runs for $t(n)$ time only using $n$ space and $n$ bits of non-determinism?  Or, maybe this just isn't possible given existing techniques.  Any thoughts are welcomed.  
> **username_0**: Sorry that my previous comment (deleted) was a little overly optimistic in the result.  Although it's just a small step to finding a better reduction to CNF-SAT, for every $k$, I have a reduction that reduces a SAT instance with $n$ variables and $m$ literal occurrences to a SAT instance of weft $k+1$ with $n$ variables and $2^{k \cdot m^{\frac{1}{k}}}$ literal occurrences.  

---

## 0 answers

