9
$\begingroup$

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.

Improve this question
$\endgroup$
  • 3
    $\begingroup$ 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? $\endgroup$ – holf Mar 29 '17 at 14:52
  • $\begingroup$ Thank you very much for the comment. That sounds right. :) I will edit the question based on your comment. $\endgroup$ – Michael Wehar Mar 29 '17 at 15:13
  • 3
    $\begingroup$ The best known reduction to CNF-SAT is Tseytin transformation. $\endgroup$ – qsp Mar 29 '17 at 17:28
  • $\begingroup$ @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? $\endgroup$ – Michael Wehar Mar 29 '17 at 18:38
  • 4
    $\begingroup$ 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... $\endgroup$ – Ryan Williams Mar 30 '17 at 1:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.