How much can we reduce the number of clauses by converting from $k$-SAT to $(k+m)$-SAT?

Question

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?

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

EDIT:

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.