# Concrete family of propositional formulas

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

• Would you accept a formula that uses additional symbols and is equisatisfiable to your formula?
– D.W.
Nov 30, 2022 at 9:23
• @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). Nov 30, 2022 at 9:41

$$\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.
• I guess that if you apply this recursively you can get something like $O(kn^{\log(k)})$? Nov 30, 2022 at 10:01