<p><strong>Theorem 1.</strong> <em>For all <span class="math-container">$n\ge 6$</span> and <span class="math-container">$T$</span> with <span class="math-container">$n+14\le T \le 7{n\choose 3}$</span>, there is a satisfiable 3-SAT formula on <span class="math-container">$n$</span> variables with <span class="math-container">$T$</span> clauses in which all clauses are redundant.</em></p>
<p>Before we give the proof, note that <span class="math-container">$7{n\choose 3}$</span> is an upper bound on the number of clauses in <em>any</em> satisfiable 3-CNF formula.  In the case <span class="math-container">$T=7{n\choose 3}$</span> the theorem implies that the formula on <span class="math-container">$n$</span> variables obtained by anding together all 3-CNF clauses containing at least one positive literal is uniquely satisfied by setting all variables true, and all of its clauses are redundant.</p>
<p><em>Proof of Theorem 1.</em></p>
<ol>
<li><p>Let <span class="math-container">$\mu(x_1, x_2, x_3)$</span> be the 3-CNF formula with 3 variables that contains all 3-CNF clauses except <span class="math-container">$\overline x_1 \vee \overline x_2 \vee \overline x_3$</span>.  Then <span class="math-container">$\mu(x_1, x_2, x_3)$</span> is uniquely satisfied by setting all variables true. The formula <span class="math-container">$\mu$</span> has seven clauses.</p>
</li>
<li><p>Now for <span class="math-container">$x=(x_1, x_2, x_3)$</span> and <span class="math-container">$z=(z_1, z_2, \ldots, z_{n'})$</span>
define
<span class="math-container">$$\alpha(x, z) = (z_1 \vee \overline{x_1} \vee \overline{x_2})\wedge (z_2 \vee \overline{x_1} \vee \overline{x_2})
\wedge \cdots \wedge (z_{n'} \vee \overline{x_1} \vee \overline{x_2})$$</span>
and
<span class="math-container">$$\beta(x, z) = \mu(x) \wedge \alpha(x, z).$$</span></p>
</li>
<li><p>Note that <span class="math-container">$\beta(x, z)$</span> is uniquely satisfied by setting all its variables true.</p>
</li>
<li><p><em>Case 1.</em> First consider the case that <span class="math-container">$T \ge 14 + 2n$</span>.</p>
</li>
<li><p>For <span class="math-container">$x=(x_1, x_2, x_3)$</span>, <span class="math-container">$y=(y_1, y_2, y_3)$</span>, and
<span class="math-container">$z=(z_1, \ldots, z_{n'})$</span> where <span class="math-container">$n'=n-6$</span>, define
<span class="math-container">$$\phi(x, y, z)
= \beta(x, y) \wedge \beta(y, x) \wedge \alpha(x, z) \wedge \alpha(y, z).$$</span></p>
</li>
<li><p>By inspection the clauses in <span class="math-container">$\phi(x, y, z)$</span> are all distinct. By Step 3 above <span class="math-container">$\phi(x, y, z)$</span> is uniquely satisfied by setting all variables true.</p>
</li>
<li><p>Every clause in <span class="math-container">$\phi(x, y, z)$</span> is redundant.  (Indeed, for any three of the four subformulas in the definition of <span class="math-container">$\phi$</span> to be satisfied, all variables in <span class="math-container">$(x, y, z)$</span> must be true.  This follows from the same reasoning as for Step 3.)</p>
</li>
<li><p>Then <span class="math-container">$\phi(x, y, z)$</span> has <span class="math-container">$6+n'=n$</span> variables and <span class="math-container">$14+2n \le T$</span> clauses.</p>
</li>
<li><p>Now pad <span class="math-container">$\phi$</span> by adding <span class="math-container">$T-14-2n$</span> clauses of the form <span class="math-container">$(u\vee v\vee w)$</span> where <span class="math-container">$u$</span>, <span class="math-container">$v$</span>, and <span class="math-container">$w$</span> are any of the <span class="math-container">$2n$</span> literals and at least one literal is positive.  There are <span class="math-container">$7{n \choose 3}$</span> such clauses, <span class="math-container">$14+2n$</span> of which already occur in <span class="math-container">$\phi$</span> --- avoid those.  All added clauses are redundant.  This concludes the proof for Case 1.</p>
</li>
<li><p><em>Case 2.</em> Now consider the remaining case: <span class="math-container">$n + 14\le T &lt; 14+2n$</span>.</p>
</li>
<li><p>For <span class="math-container">$x=(x_1, x_2, x_3)$</span>, <span class="math-container">$y=(y_1, y_2, y_3)$</span>, and
<span class="math-container">$z=(z_1, \ldots, z_{n'})$</span> where <span class="math-container">$n'=n-6$</span>, define
<span class="math-container">$\psi(x, y, z)$</span> to be the &quot;and&quot; of the following two subformulae:</p>
</li>
</ol>
<p><span class="math-container">$$\beta(x, y) \wedge \beta(y, x)$$</span>
<span class="math-container">$$(x_1 \vee z_1 \vee z_2) \wedge(x_1 \vee z_2 \vee z_3) \wedge \cdots \wedge (x_1 \vee z_{n'-1} \vee z_{n'}) \wedge (x_1 \vee z_{n'} \vee z_1).$$</span></p>
<ol start="12">
<li><p>By inspection the clauses in <span class="math-container">$\psi(x, y, z)$</span> are all distinct. The satisfying assignments to <span class="math-container">$\phi(x, y, z)$</span> are those that set variables in <span class="math-container">$x$</span> and <span class="math-container">$y$</span> true, and variables in <span class="math-container">$z$</span> arbitrarily.</p>
</li>
<li><p>Every clause in <span class="math-container">$\psi(x, y, z)$</span> is redundant. (The reasoning is as in Case 1, except that here the assignment to <span class="math-container">$z$</span> is unconstrained and remains unconstrained upon removal of any clause.)</p>
</li>
<li><p>And <span class="math-container">$\psi(x, y, z)$</span> has <span class="math-container">$6+n'=n$</span> variables and <span class="math-container">$14+n \le T$</span> clauses.</p>
</li>
<li><p>Now pad <span class="math-container">$\psi$</span> by adding <span class="math-container">$T-14-n &lt; n$</span> new clauses of the form <span class="math-container">$(x_1 \vee \overline{z_i}\vee \overline{z_{i+1}})$</span> where <span class="math-container">$i&lt;n$</span>. All added clauses are redundant.  This concludes the proof for Case 2.
<span class="math-container">$~~~\Box$</span></p>
</li>
</ol>
<p>Note that we could weaken the assumption <span class="math-container">$T \ge n+14$</span> to something like <span class="math-container">$T \ge n/2+14$</span> if we are allowed to use variables that occur only once.  (But in that case the notion of redundancy is unclear, because deleting the sole clause that contains a given variable removes the variable from the formula.)</p>

CC BY-SA 4.0
2022-01-23T16:11:44.607Z
2022-01-24T23:28:38.597Z
2022-01-24T23:28:38.597Z
Neal Young
<p>I interpret the question as: given <span class="math-container">$n$</span> and <span class="math-container">$T$</span>, what is the maximum number of redundant clauses a satisfiable <span class="math-container">$n$</span>-variable formula on <span class="math-container">$T$</span> clauses can have?
For the purposes of this question, I find it helpful to phrase this as:
Find (lower bounds on) <span class="math-container">$f(n,m)$</span> such that an <span class="math-container">$n$</span>-variable <span class="math-container">$m$</span>-clause formula may imply <span class="math-container">$f(n,m)$</span> clauses (that may or may not be in the formula). I answer the question by giving, in two constructions, my &quot;best attempt&quot; formulas, which try to keep <span class="math-container">$m$</span> as small as possible, but make <span class="math-container">$f$</span> as large as possible. I find that <span class="math-container">$f(n,\mathcal O(n))=\Theta(n^3)$</span>, i.e., only a linear number of clauses suffices to obtain the maximum possible number of implied clauses. A consequence is that, in the extreme case, all clauses except a <span class="math-container">$\mathcal O(\frac{1}{n^2})$</span> fraction is redundant.
This non-redundant part that you are after, is usually called the <em>unsatisfiable core</em> when the formula is unsatisfiable, which will yield you many results if you search the literature.</p>
<ol>
<li><p><span class="math-container">$f(n,2(n-2))\geq 3\binom{n-1}{2}=\Omega(n^2)$</span>. <strong>Construction</strong>: consider the formula with clauses <span class="math-container">$(x_1\vee x_2\vee x_i)$</span> and <span class="math-container">$(\neg x_1\vee x_2\vee x_i)$</span> for <span class="math-container">$i=3\ldots n$</span>. This implies all clauses <span class="math-container">$(x_2\vee x_i)$</span>, so it also implies the clause <span class="math-container">$(x_2\vee \pm x_i\vee \pm x_j)$</span>, except not the clause <span class="math-container">$(x_2\vee \neg x_i\vee \neg x_j)$</span>, for each <span class="math-container">$(i,j)$</span> with <span class="math-container">$1\leq i&lt;j\leq n$</span>. There are <span class="math-container">$3\binom{n-1}2$</span> such clauses.</p>
</li>
<li><p><span class="math-container">$f(n, \frac{7}{3}n)= 7\binom n3=\Omega(n^3)$</span>. <strong>Construction</strong>: consider the formula with the <span class="math-container">$7$</span> clauses <span class="math-container">$(\pm x_{i}\vee \pm x_{i+1}\vee \pm x_{i+2})$</span> except the all-negative clause <span class="math-container">$(\neg x_i\vee \neg x_{i+1}\vee \neg x_{i+2})$</span>, for <span class="math-container">$i=1,4,7,\ldots,n-2$</span>. This formula implies all literals <span class="math-container">$x_i=1$</span>, so it has exactly one satisfying assignment, <span class="math-container">$x=(1,\ldots, 1)$</span>. It therefeore also implies all clauses that have at least one positive literal in it, of which there are <span class="math-container">$7\binom n3$</span>. A consequence: for <span class="math-container">$\alpha\leq \frac{7}{3}$</span>, we have <span class="math-container">$f(n,\alpha n)=\Omega(n^{\frac{9}{7}\alpha})$</span>, which is better than Construction 1, since we get <span class="math-container">$f(n,2n)=\Omega(n^{2\frac{4}{7}})$</span>.</p>
</li>
</ol>
<p>Does <span class="math-container">$f$</span> have a phase transition between <span class="math-container">$m=2n$</span> and <span class="math-container">$m=2\frac{1}{3}n$</span>, where it goes from <span class="math-container">$f=\Omega(n^{2\frac{4}{7}})$</span> to <span class="math-container">$f=\Omega(n^3)$</span>? Are these constructions optimal? I hope that someone can answer who is more familiar with the literature.</p>
<hr />
<p>The flipside of your question (my previous interpretation): given a satisfiable formula on <span class="math-container">$n$</span> variables and <span class="math-container">$T$</span> clauses, when may I conclude, based only on <span class="math-container">$n$</span> and <span class="math-container">$T$</span>, that at least some number of the clauses are redundant?</p>
<p>I find this a difficult combinatorial question. Perhaps the literature contains the answer; I hope somebody can add it here.</p>
<p>Here is a lower bound. Consider the formula with all <span class="math-container">$T=\binom n3$</span> all-positive clauses. This is a redundancy-free formula, since removing, e.g., the clause <span class="math-container">$(x_1\vee x_2\vee x_3)$</span> now allows the satisfying assignment <span class="math-container">$x=(0,0,0,1,\ldots, 1)$</span> (the definition of redundant was that removing it preserved the set of satisfying assignments). All the other clauses behave similarly. Is this the largest redundancy-free formula?</p>

CC BY-SA 4.0
2022-01-22T18:45:53.743Z
I suppose my question was slightly different, in that I was asking if there is a way to know the maximum possible number of redundant clauses, for a given $n,T$, whereas you have answered a very related interesting question, as to if one can ever be certain about the existence of redundancies. So I suppose you've answered the lower bound! The motivation for my question, is essentially that I have an unconventional solver which is hindered by redundant clauses, and so I am looking to analyze the worst case running time for that solver.
Craig
CC BY-SA 4.0
2022-01-22T20:51:25.743Z
Ah, I see. Actually, I find my misunderstanding quite amusing! Let me try to answer your real question, if I have it correct: Given $n$ and $T$, what is the maximum number of redundant clauses any formula can have? For *unsatisfiable* formulas, the answer is clearly $8\binom n3-8$, namely the formula containing all the clauses is unsat, but you only need $8$ clauses to make an unsat formula (I think this is what you meant with the $T-n^3$ bound). I'll think about your question, and update my answer if I figure it out :)
Lieuwe Vinkhuijzen
CC BY-SA 4.0
2022-01-22T21:11:04.963Z
Yes that is what I meant, and is why the question is really only interesting for satisfiable instances. If you are able to think up an answer I would appreciate it immensely! I'll be thinking too
Craig
CC BY-SA 4.0
2022-01-22T23:41:44.913Z
I have added some constructions which go some way towards answering your question, if I have interpreted it correctly this time. I hope you find them helpful; I also hope that you find the framing helpful. I cannot prove that these constructions are optimal, and there are surely many other constructions for other values of $m=\alpha n$.
Lieuwe Vinkhuijzen
CC BY-SA 4.0
2022-01-24T23:44:36.980Z
Regarding Lieuwe's question about phase transition, I think that the formula $\beta(x, z)$ (where $x=(x_1,x_2, x_3)$ and $z=(z_1, \ldots, z_{n-3})$) from [my answer](https://cstheory.stackexchange.com/a/51019/8237) has $n+4$ clauses and is uniquely satisfiable by setting all variables true.  I think this implies $f(n, n+4) = 7{n\choose 3}$.  By generalizing this argument I think one can show $f(n, n/3+k) = \Omega(k^3)$ for any $k$.  Any 3-CNF formula with $n$ variables has at least $n/3$ clauses, so any phase transition would have to be around $m\approx n/3 + o(n)$.
Neal Young
CC BY-SA 4.0
2022-01-22T13:03:53.737Z
2022-01-23T15:31:07.893Z
2022-01-23T15:31:07.893Z
Lieuwe Vinkhuijzen
<p>For a non-empty <span class="math-container">$3-SAT$</span> with <span class="math-container">$n\geq3$</span> variables and <span class="math-container">$T\geq1$</span> non-identical non-degenerate clauses <span class="math-container">$C_i$</span>:
<span class="math-container">$$S=C_1 \wedge \ldots \wedge C_T$$</span>
where a non-degenerate clause is one containing <span class="math-container">$3$</span> unique literals (no clauses like <span class="math-container">$a\vee a\vee b$</span>, etc.)</p>
<p>It is clear that there are <span class="math-container">$2^3 \cdot \binom{n}{3}\geq T$</span> possible <span class="math-container">$C_i$</span> to choose from. Additionally when <span class="math-container">$n=3$</span> there are no possible redundant clauses.</p>
<p>This is not true for <span class="math-container">$n=4$</span>, here is an example:
<span class="math-container">$$\begin{split}
&amp;(x_4\vee x_2\vee x_3)\wedge(\overline{x}_4\vee x_2\vee x_3)\wedge(x_1\vee x_4\vee x_3)\wedge(x_1\vee \overline{x}_4\vee x_3)\\
\wedge&amp;(x_1\vee x_2\vee x_4)\wedge(x_1\vee x_2\vee \overline{x}_4)\wedge(x_1\vee x_2\vee x_3)
\end{split}
$$</span>
The last clause here is redundant, since removing it from the <span class="math-container">$SAT$</span> instance would have no effect on the satisfying assignments.</p>
<p>For an unsatisfiable instance, clearly the upper bound on redundant clauses is: <span class="math-container">$T-2^3$</span></p>
<p>Given these constraints, does anyone see a path towards figuring out the maximum number of possible redundant clauses in a satisfiable instance, for a given <span class="math-container">$n$</span> and <span class="math-container">$T$</span>?</p>

CC BY-SA 4.0
2022-01-22T13:01:03.930Z
Neat question. You can improve the question by defining, what *exactly* do you mean by redundant? Do you mean that the set of satisfying assignments is preserved when that clause is removed, or something else? Do you mean to ask about the clauses *that are in the formula* or do you mean clauses that *are implied* by the formula, but do not necessarily appear in the formula?
Lieuwe Vinkhuijzen
<sat><upper-bounds>
Is there an Upper Bound on Number of Redundant Clauses in a satisfiable $3-SAT$?
Craig
# Is there an Upper Bound on Number of Redundant Clauses in a satisfiable $3-SAT$?

(Asked by: username_0 on 2022-01-22)

For a non-empty $3-SAT$ with $n\geq3$ variables and $T\geq1$ non-identical non-degenerate clauses $C\_i$:
$$S=C\_1 \wedge \ldots \wedge C\_T$$
where a non-degenerate clause is one containing $3$ unique literals (no clauses like $a\vee a\vee b$, etc.)

It is clear that there are $2^3 \cdot \binom{n}{3}\geq T$ possible $C\_i$ to choose from. Additionally when $n=3$ there are no possible redundant clauses.

This is not true for $n=4$, here is an example:
$$\begin{split}
&(x\_4\vee x\_2\vee x\_3)\wedge(\overline{x}\_4\vee x\_2\vee x\_3)\wedge(x\_1\vee x\_4\vee x\_3)\wedge(x\_1\vee \overline{x}\_4\vee x\_3)\\
\wedge&(x\_1\vee x\_2\vee x\_4)\wedge(x\_1\vee x\_2\vee \overline{x}\_4)\wedge(x\_1\vee x\_2\vee x\_3)
\end{split}
$$
The last clause here is redundant, since removing it from the $SAT$ instance would have no effect on the satisfying assignments.

For an unsatisfiable instance, clearly the upper bound on redundant clauses is: $T-2^3$

Given these constraints, does anyone see a path towards figuring out the maximum number of possible redundant clauses in a satisfiable instance, for a given $n$ and $T$?

**Tags:** sat, upper-bounds

> **Comments:**
> **username_1**: Neat question. You can improve the question by defining, what *exactly* do you mean by redundant? Do you mean that the set of satisfying assignments is preserved when that clause is removed, or something else? Do you mean to ask about the clauses *that are in the formula* or do you mean clauses that *are implied* by the formula, but do not necessarily appear in the formula?  

---

## 2 answers

### Answer by username_1 on 2022-01-22. Score: 7 | Accepted answer

I interpret the question as: given $n$ and $T$, what is the maximum number of redundant clauses a satisfiable $n$-variable formula on $T$ clauses can have?
For the purposes of this question, I find it helpful to phrase this as:
Find (lower bounds on) $f(n,m)$ such that an $n$-variable $m$-clause formula may imply $f(n,m)$ clauses (that may or may not be in the formula). I answer the question by giving, in two constructions, my "best attempt" formulas, which try to keep $m$ as small as possible, but make $f$ as large as possible. I find that $f(n,\mathcal O(n))=\Theta(n^3)$, i.e., only a linear number of clauses suffices to obtain the maximum possible number of implied clauses. A consequence is that, in the extreme case, all clauses except a $\mathcal O(\frac{1}{n^2})$ fraction is redundant.
This non-redundant part that you are after, is usually called the *unsatisfiable core* when the formula is unsatisfiable, which will yield you many results if you search the literature.

1. $f(n,2(n-2))\geq 3\binom{n-1}{2}=\Omega(n^2)$. **Construction**: consider the formula with clauses $(x\_1\vee x\_2\vee x\_i)$ and $(\neg x\_1\vee x\_2\vee x\_i)$ for $i=3\ldots n$. This implies all clauses $(x\_2\vee x\_i)$, so it also implies the clause $(x\_2\vee \pm x\_i\vee \pm x\_j)$, except not the clause $(x\_2\vee \neg x\_i\vee \neg x\_j)$, for each $(i,j)$ with $1\leq i. There are $3\binom{n-1}2$ such clauses.
2. $f(n, \frac{7}{3}n)= 7\binom n3=\Omega(n^3)$. **Construction**: consider the formula with the $7$ clauses $(\pm x\_{i}\vee \pm x\_{i+1}\vee \pm x\_{i+2})$ except the all-negative clause $(\neg x\_i\vee \neg x\_{i+1}\vee \neg x\_{i+2})$, for $i=1,4,7,\ldots,n-2$. This formula implies all literals $x\_i=1$, so it has exactly one satisfying assignment, $x=(1,\ldots, 1)$. It therefeore also implies all clauses that have at least one positive literal in it, of which there are $7\binom n3$. A consequence: for $\alpha\leq \frac{7}{3}$, we have $f(n,\alpha n)=\Omega(n^{\frac{9}{7}\alpha})$, which is better than Construction 1, since we get $f(n,2n)=\Omega(n^{2\frac{4}{7}})$.

Does $f$ have a phase transition between $m=2n$ and $m=2\frac{1}{3}n$, where it goes from $f=\Omega(n^{2\frac{4}{7}})$ to $f=\Omega(n^3)$? Are these constructions optimal? I hope that someone can answer who is more familiar with the literature.

---

The flipside of your question (my previous interpretation): given a satisfiable formula on $n$ variables and $T$ clauses, when may I conclude, based only on $n$ and $T$, that at least some number of the clauses are redundant?

I find this a difficult combinatorial question. Perhaps the literature contains the answer; I hope somebody can add it here.

Here is a lower bound. Consider the formula with all $T=\binom n3$ all-positive clauses. This is a redundancy-free formula, since removing, e.g., the clause $(x\_1\vee x\_2\vee x\_3)$ now allows the satisfying assignment $x=(0,0,0,1,\ldots, 1)$ (the definition of redundant was that removing it preserved the set of satisfying assignments). All the other clauses behave similarly. Is this the largest redundancy-free formula?

> **Comments:**
> **username_0**: I suppose my question was slightly different, in that I was asking if there is a way to know the maximum possible number of redundant clauses, for a given $n,T$, whereas you have answered a very related interesting question, as to if one can ever be certain about the existence of redundancies. So I suppose you've answered the lower bound! The motivation for my question, is essentially that I have an unconventional solver which is hindered by redundant clauses, and so I am looking to analyze the worst case running time for that solver.  
> **username_1**: Ah, I see. Actually, I find my misunderstanding quite amusing! Let me try to answer your real question, if I have it correct: Given $n$ and $T$, what is the maximum number of redundant clauses any formula can have? For *unsatisfiable* formulas, the answer is clearly $8\binom n3-8$, namely the formula containing all the clauses is unsat, but you only need $8$ clauses to make an unsat formula (I think this is what you meant with the $T-n^3$ bound). I'll think about your question, and update my answer if I figure it out :)  
> **username_0**: Yes that is what I meant, and is why the question is really only interesting for satisfiable instances. If you are able to think up an answer I would appreciate it immensely! I'll be thinking too  
> **username_1**: I have added some constructions which go some way towards answering your question, if I have interpreted it correctly this time. I hope you find them helpful; I also hope that you find the framing helpful. I cannot prove that these constructions are optimal, and there are surely many other constructions for other values of $m=\alpha n$.  
> **username_2**: Regarding Lieuwe's question about phase transition, I think that the formula $\beta(x, z)$ (where $x=(x_1,x_2, x_3)$ and $z=(z_1, \ldots, z_{n-3})$) from [my answer](https://cstheory.stackexchange.com/a/51019/8237) has $n+4$ clauses and is uniquely satisfiable by setting all variables true.  I think this implies $f(n, n+4) = 7{n\choose 3}$.  By generalizing this argument I think one can show $f(n, n/3+k) = \Omega(k^3)$ for any $k$.  Any 3-CNF formula with $n$ variables has at least $n/3$ clauses, so any phase transition would have to be around $m\approx n/3 + o(n)$.  

---

### Answer by username_2 on 2022-01-23. Score: 7

**Theorem 1.** *For all $n\ge 6$ and $T$ with $n+14\le T \le 7{n\choose 3}$, there is a satisfiable 3-SAT formula on $n$ variables with $T$ clauses in which all clauses are redundant.*

Before we give the proof, note that $7{n\choose 3}$ is an upper bound on the number of clauses in *any* satisfiable 3-CNF formula. In the case $T=7{n\choose 3}$ the theorem implies that the formula on $n$ variables obtained by anding together all 3-CNF clauses containing at least one positive literal is uniquely satisfied by setting all variables true, and all of its clauses are redundant.

*Proof of Theorem 1.*

1. Let $\mu(x\_1, x\_2, x\_3)$ be the 3-CNF formula with 3 variables that contains all 3-CNF clauses except $\overline x\_1 \vee \overline x\_2 \vee \overline x\_3$. Then $\mu(x\_1, x\_2, x\_3)$ is uniquely satisfied by setting all variables true. The formula $\mu$ has seven clauses.
2. Now for $x=(x\_1, x\_2, x\_3)$ and $z=(z\_1, z\_2, \ldots, z\_{n'})$
   define
   $$\alpha(x, z) = (z\_1 \vee \overline{x\_1} \vee \overline{x\_2})\wedge (z\_2 \vee \overline{x\_1} \vee \overline{x\_2})
   \wedge \cdots \wedge (z\_{n'} \vee \overline{x\_1} \vee \overline{x\_2})$$
   and
   $$\beta(x, z) = \mu(x) \wedge \alpha(x, z).$$
3. Note that $\beta(x, z)$ is uniquely satisfied by setting all its variables true.
4. *Case 1.* First consider the case that $T \ge 14 + 2n$.
5. For $x=(x\_1, x\_2, x\_3)$, $y=(y\_1, y\_2, y\_3)$, and
   $z=(z\_1, \ldots, z\_{n'})$ where $n'=n-6$, define
   $$\phi(x, y, z)
   = \beta(x, y) \wedge \beta(y, x) \wedge \alpha(x, z) \wedge \alpha(y, z).$$
6. By inspection the clauses in $\phi(x, y, z)$ are all distinct. By Step 3 above $\phi(x, y, z)$ is uniquely satisfied by setting all variables true.
7. Every clause in $\phi(x, y, z)$ is redundant. (Indeed, for any three of the four subformulas in the definition of $\phi$ to be satisfied, all variables in $(x, y, z)$ must be true. This follows from the same reasoning as for Step 3.)
8. Then $\phi(x, y, z)$ has $6+n'=n$ variables and $14+2n \le T$ clauses.
9. Now pad $\phi$ by adding $T-14-2n$ clauses of the form $(u\vee v\vee w)$ where $u$, $v$, and $w$ are any of the $2n$ literals and at least one literal is positive. There are $7{n \choose 3}$ such clauses, $14+2n$ of which already occur in $\phi$ --- avoid those. All added clauses are redundant. This concludes the proof for Case 1.
10. *Case 2.* Now consider the remaining case: $n + 14\le T < 14+2n$.
11. For $x=(x\_1, x\_2, x\_3)$, $y=(y\_1, y\_2, y\_3)$, and
    $z=(z\_1, \ldots, z\_{n'})$ where $n'=n-6$, define
    $\psi(x, y, z)$ to be the "and" of the following two subformulae:

$$\beta(x, y) \wedge \beta(y, x)$$
$$(x\_1 \vee z\_1 \vee z\_2) \wedge(x\_1 \vee z\_2 \vee z\_3) \wedge \cdots \wedge (x\_1 \vee z\_{n'-1} \vee z\_{n'}) \wedge (x\_1 \vee z\_{n'} \vee z\_1).$$

12. By inspection the clauses in $\psi(x, y, z)$ are all distinct. The satisfying assignments to $\phi(x, y, z)$ are those that set variables in $x$ and $y$ true, and variables in $z$ arbitrarily.
13. Every clause in $\psi(x, y, z)$ is redundant. (The reasoning is as in Case 1, except that here the assignment to $z$ is unconstrained and remains unconstrained upon removal of any clause.)
14. And $\psi(x, y, z)$ has $6+n'=n$ variables and $14+n \le T$ clauses.
15. Now pad $\psi$ by adding $T-14-n < n$ new clauses of the form $(x\_1 \vee \overline{z\_i}\vee \overline{z\_{i+1}})$ where $i. All added clauses are redundant. This concludes the proof for Case 2.
    $~~~\Box$

Note that we could weaken the assumption $T \ge n+14$ to something like $T \ge n/2+14$ if we are allowed to use variables that occur only once. (But in that case the notion of redundancy is unclear, because deleting the sole clause that contains a given variable removes the variable from the formula.)


---

