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$?

  • 6
    $\begingroup$ 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? $\endgroup$ Jan 22, 2022 at 13:01

2 Answers 2


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<j\leq n$. 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?

  • $\begingroup$ 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. $\endgroup$
    – Craig
    Jan 22, 2022 at 18:45
  • $\begingroup$ 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 :) $\endgroup$ Jan 22, 2022 at 20:51
  • $\begingroup$ 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 $\endgroup$
    – Craig
    Jan 22, 2022 at 21:11
  • $\begingroup$ 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$. $\endgroup$ Jan 22, 2022 at 23:41
  • $\begingroup$ 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 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)$. $\endgroup$
    – Neal Young
    Jan 24, 2022 at 23:44

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

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

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

  3. And $\psi(x, y, z)$ has $6+n'=n$ variables and $14+n \le T$ clauses.

  4. 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<n$. 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.)


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.