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.