Let $k,n \in \mathbb{N}$, where $k$ can be thought of as being fixed constant. For each $1 \leq \ell \leq k$ and $1 \leq i \leq n$ we have a proposition symbol $p_{(\ell,i)}$ (so in total we have $nk$-proposition symbols). Consider the following propositional formula $$\bigvee_{n_1 + \dots + n_k = n} \ \bigwedge_{1 \leq \ell \leq k} \ p_{(\ell,n_\ell)}$$ of size $O(kn^{k-1})$. Is there an equivalent propositional formula which is essentially shorter (say, of length $n^{(k/2)}$)?

EDIT: Even though the original question now has a perfectly valid answer, I would still like to know whether one could do better than $O(n^{\log(k)})$. For example, is $O(n^{100})$ possible? If you know how one could achieve a bound of this shape, you could send me an email about it directly (or just post it as an answer, if you prefer).

  • 1
    $\begingroup$ Would you accept a formula that uses additional symbols and is equisatisfiable to your formula? $\endgroup$
    – D.W.
    Nov 30, 2022 at 9:23
  • $\begingroup$ @D.W. Good question. I'm only looking for shorter formulas that are equivalent with my formula (motivation comes from formula size lower bounds, not SAT-encoding related things). $\endgroup$ Nov 30, 2022 at 9:41

1 Answer 1


How about this?

$$\bigvee_{1 \le u \le n} \left( \bigvee_{n_1+\dots+n_{k/2}=u} \bigwedge_{1 \le \ell \le k/2} p_{\ell,n_\ell} \right) \land \left( \bigvee_{n_{k/2+1}+\dots+n_k=n-u} \bigwedge_{k/2+1 \le \ell \le n} p_{\ell,n_\ell} \right)$$

This has size $O(kn^{k/2+1})$. Of course, this can be generalized by applying the same transformation recursively.

  • 1
    $\begingroup$ I guess that if you apply this recursively you can get something like $O(kn^{\log(k)})$? $\endgroup$ Nov 30, 2022 at 10:01

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.