3
$\begingroup$

If I have an instance of $k$-SAT with $m$ clauses, then a trivial upper bound on the number of variables $n$ is given by $n \leq mk$. But we can only have $n = mk$ when no variable is repeated and that would be a trivial yes-case of k-SAT. I am making some running time analysis based on number of clauses, and therefore need to eliminate $n$ from my formula.

So my question is, can I make a lower upper bound on the number of variables, above which the instances will always be trivial?

I have a feeling that $\frac{1}{2}mk$ should be possible (I even think I had the argument for this in my head at some point), because $mk$ is actually an upper bound on the number of literals, not variables, but I can't be sure that all literals are present in both negated and unnegated form, and therefore can't seem to find an argument for this.

$\endgroup$
1
$\begingroup$

If you want to prove the worst-case running time of your algorithm, you probably don't need to prove that. It's probably enough that there exists instances of SAT with (say) $\frac12 mk$ variables that are NP-hard; and that can be proven.

When each variable occurs only twice in the formula, SAT can be solved in polynomial time (via resolution).

With the restriction that each variable can occur up to three times in the formula, SAT remains NP-hard. (Proof: start with an ordinary CNF formula $\varphi$. If $x_i$ appears $k$ times, introduce variables $x_{i,1},\dots,x_{i,k}$, replace the $j$th occurrence of $x_i$ with $x_{i,j}$, and add clauses for $\neg x_{i,1} \lor x_{i,2},\neg x_{i,2} \lor x_{i,3},\dots,\neg x_{i,k-1} \lor x_{i,k}, \neg x_{i,k} \lor x_{i,1}$.)

Therefore, there exists a class of instances of $k$-SAT with $m$ clauses and $\frac{1}{3} mk$ variables, such that solving those instances is NP-hard.

To answer your original question, there is no useful answer to your original question. For all $\varepsilon>0$, there exists a class of instances of $k$-SAT with $m$ clauses and $(1-\varepsilon)mk$ variables that is NP-hard. In particular, take an ordinary CNF formula $\varphi$ with $n$ variables and then just append useless clauses of the form $x_{t} \lor x_{t+1} \lor \cdots \lor x_{t+k}$; each useless clause mentions $k$ new variables that appear only in that one clause and nowhere else. The resulting formula is exactly as hard as $\varphi$, but now has a number of variables that is an arbitrarily large fraction of $mk$.

$\endgroup$
  • $\begingroup$ I do not think that you are right about the useless clauses. Every time you add a clause of the form $(x_{t} \lor x_{t} \lor \cdots \lor x_t)$ you will have introduced a new variable, but also a new clause. And as $k \geq 2$, this would make $mk - n$ bigger. Besides we could get rid of this type of clauses in time linear in the number of clauses (they are basically unit clauses after all) so it would be of more use to me to find an upper bound on the number of variables after obvious useless clauses have been eliminated. $\endgroup$ – AstridNeu Jun 27 '18 at 13:19
  • $\begingroup$ @AstridNeu, sure, but that's beside the point. Everything written in the last paragraph remains true, and that suffices to show that there is no useful result like "if there are at least $\frac12 mk$ variables then the instance is trivial" or "if there are at least $\frac23 mk$ variables then the instance is trivial" or anything else like that replacing the fraction $\frac12$ with any other fraction strictly less than 1. (I did correct one small error in my last paragraph.) I am answering the question you asked in your post. If you have a new one, you might need to post it separately. $\endgroup$ – D.W. Jun 29 '18 at 17:54
  • $\begingroup$ Yes. Now that you edited it to $k$ new variables per appended clause $mk-n$ will always remain the same, and thus I see your point. Thanks. $\endgroup$ – AstridNeu Jun 30 '18 at 5:40

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.