If we suppose that we start with an instance of $k$-SAT, and try converting the problem to an instance of $(k+m)$-SAT, where there are $(k+m)$ literals per clause, can we guarantee a reduction in the total amount of clauses?

I realized after posting that we can't guarantee that the number of clauses can be reduced. However, I wonder if we have $n$ clauses, could we get something like $n/k + O(1)$ clauses by some "reduction" technique?

If so, how much can we guarantee the total number of clauses can be reduced by? For instance, if we start with $k$-SAT with $n_k$ clauses, what is the smallest guaranteed $n_{k+m}$, the new amount of clauses, that will result if we convert this instance to $(k+m)$-SAT?

More importantly, how do we carry out this conversion?


1 Answer 1


One type of conversion is simply the reverse of the k-sat-to-3-sat conversion:

Recall, the conversion of k-sat to "j"-sat, $j<k$:

$$\begin{eqnarray*} && (x_1 \vee x_2 ... \vee x_j \vee ... \vee x_k)\\ \rightarrow && (x_1 \vee x_2 ... x_j \vee d) \wedge (\overline d \vee x_{j+1} \vee x_{j+2} ... x_k)\\ \end{eqnarray*}$$

Here, $d$ is a dummy variable, which means something like "This clause isn't true, but another clause I know is". The other clause being the next clause that was split off of the original. The above is an example where $2j \geq k$, otherwise the 2nd split node will still be larger than $j$, and we must split that one again, in the same way.

Reversing the conversion

$(x_1 \vee x_2 ... x_j) \wedge (\overline x_j \vee x_{j+1} \vee ... x_k)$ then you can combine the clauses into:

$(x_1 \vee x_2 ... x_{j-1} \vee x_{j+1} \vee x_{j+2} \vee ... x_k)$

Notice the missing $x_j$ in this new formula.

Of course, you aren't guaranteed to find clauses like this in an arbitrary formula so the smallest guaranteed $n_{k+m}$ is equal to $n_k$.

However, on ordinary formulas, a variable and its negation will appear in the formula; otherwise you can perform pure-literal-elimination (described here). For simplicity, lets also assume that $k+m \geq 2k-2$. Then we can combine any two clauses that contain a literal in one and its negation in the other. Since every literal should have another clause with a negation, one can empirically guess that you should be able to approximately halve the number of clauses (you might get stuck with some literals and their negations in already joined clauses, and thus you will be stuck with some unjoinable clauses at the end; optimally joining clauses like this might be another interesting problem).


After reflection, I realized that $x_j$ must be free and not used elsewhere in the formula in order to collapse the two clauses that it belongs to. Therefore, these type of clauses (one containing a literal, and the other its negation, with this literal not being used elsewhere in the formula) is much rarer than I previously thought above. So the real answer is, there is no guarantee of how much we can reduce the number of clauses in the formula.

  • $\begingroup$ How did you get that conversion formula? It seems to me to be incorrect, and you can check it by truth table. $\endgroup$
    – Matt Groff
    Sep 20, 2012 at 18:24
  • $\begingroup$ Hi, I read it a long time ago but you can see it here. I might have mistyped it, or somehow made something unclear in the conversion; if so, feel free to point it out. $\endgroup$
    – Realz Slaw
    Sep 20, 2012 at 18:43
  • $\begingroup$ @MattGroff I can't seem to find my mistake, can you provide a counter example? $\endgroup$
    – Realz Slaw
    Sep 20, 2012 at 18:55
  • $\begingroup$ The counter example I checked was to start with a single clause, $(A \lor B)$. I then split this into two clauses, $(A \lor d) \land (\overline{d} \lor B)$, where $\overline{d}$ indicates "not $d$". If you check this in a truth table, they shouldn't be equal. I'll be anxiously waiting to hear if you get the same results. Also, I believe I know how we can fix this answer so that it does work, if it turns out that the original k-SAT to "j"-SAT conversion is incorrect... $\endgroup$
    – Matt Groff
    Sep 20, 2012 at 19:31
  • $\begingroup$ $$ \begin{array}{cc|c|l} A & B & A\vee B & (A\vee d)\wedge(\overline{d}\vee B)\\ 0 & 0 & 0 & 0|d=\{0,1\}\\ 0 & 1 & 1 & 1|d=\{1\}\\ 1 & 0 & 1 & 1|d=\{0\}\\ 1 & 1 & 1 & 1|d=\{1,0\}\end{array}$$ $\endgroup$
    – Realz Slaw
    Sep 20, 2012 at 21:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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