<p>How about this?</p>
<p><span class="math-container">$$\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)$$</span></p>
<p>This has size <span class="math-container">$O(kn^{k/2+1})$</span>.  Of course, this can be generalized by applying the same transformation recursively.</p>

CC BY-SA 4.0
2022-11-30T10:01:05.710Z
I guess that if you apply this recursively you can get something like $O(kn^{\log(k)})$?
Reijo Jaakkola
CC BY-SA 4.0
2022-11-30T09:34:33.510Z
2022-11-30T09:34:33.510Z
D.W.
<p>Let <span class="math-container">$k,n \in \mathbb{N}$</span>, where <span class="math-container">$k$</span> can be thought of as being fixed constant. For each <span class="math-container">$1 \leq \ell \leq k$</span> and <span class="math-container">$1 \leq i \leq n$</span> we have a proposition symbol <span class="math-container">$p_{(\ell,i)}$</span> (so in total we have <span class="math-container">$nk$</span>-proposition symbols). Consider the following propositional formula
<span class="math-container">$$\bigvee_{n_1 + \dots + n_k = n} \ \bigwedge_{1 \leq \ell \leq k} \ p_{(\ell,n_\ell)}$$</span>
of size <span class="math-container">$O(kn^{k-1})$</span>. Is there an equivalent propositional formula which is essentially shorter (say, of length <span class="math-container">$n^{(k/2)}$</span>)?</p>
<p><strong>EDIT:</strong> Even though the original question now has a perfectly valid answer, I would still like to know whether one could do better than <span class="math-container">$O(n^{\log(k)})$</span>. For example, is <span class="math-container">$O(n^{100})$</span> 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).</p>

CC BY-SA 4.0
2022-11-30T09:23:26.247Z
Would you accept a formula that uses additional symbols and is equisatisfiable to your formula?
D.W.
CC BY-SA 4.0
2022-11-30T09:41:31.043Z
@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).
Reijo Jaakkola
<cc.complexity-theory><lo.logic>
Concrete family of propositional formulas
Reijo Jaakkola
# Concrete family of propositional formulas

(Asked by: username_0 on 2022-11-30)

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

**Tags:** cc.complexity-theory, lo.logic
> **Comments:**
> **username_1**: Would you accept a formula that uses additional symbols and is equisatisfiable to your formula?  
> **username_0**: @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).  

---

## 1 answers

### Answer by username_1 on 2022-11-30. Score: 7 | Accepted answer

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.

> **Comments:**
> **username_0**: I guess that if you apply this recursively you can get something like $O(kn^{\log(k)})$?  

---

